U.S. - UK Cooperative Research: Formal Specification of Software Systems

该奖项将支持美国和英国计算机科学家在软件系统正式规范领域的合作研究。美国研究人员是斯蒂芬·菲卡斯博士；参与调查的英国研究人员是爱丁堡大学人工智能系的艾伦·邦迪博士和伦敦帝国理工学院计算机科学系的安东尼·芬克尔斯坦博士。构建完整一致的软件规范是现代软件工程方法论的关键。与此同时，对建设过程本身的表征仍然是一个开放的研究问题。从本质上讲，我们需要正式的规范来驱动我们的实现系统，但仍然缺乏以任何有纪律的方式构建这种规范的方法。首席研究员建议与两个英国研究小组合作，一个在爱丁堡大学，一个在伦敦帝国理工学院，努力实现规范设计模型的形式化和自动化。到目前为止，这三个小组中的每一个都专注于规范问题的不同方面：爱丁堡专注于从非正式描述到正式规范的映射。帝国理工学院专注于确定必要的规范活动，并跟踪它们之间的依赖关系；首席调查员专注于基于知识的规范分析方法。菲卡斯博士将与这两个英国小组合作，领导一项努力，将这三种方法整合成一个更通用的规范构建模型。结果将是双重的。首先，整合尝试本身将迫使其他三种当前模式变得更加精致。其次，菲卡斯计划将爱丁堡和帝国的部分模型整合到他现有的基于计算机的系统中，从而进一步扩展用于构建规范的自动化工具。

This award will support collaborative research between U.S. and British computer scientists in the area of the formal specification of software systems. The U.S. investigator is Dr. Stephen Fickas; the British researchers involved are Dr. Alan Bundy, Department of Artificial Intelligence, University of Edinburgh, and Dr. Anthony Finkelstein, Computer Science Department, Imperial College of Science and Technology, London. The construction of a complete and consistent software specification is critical to modern software engineering methodologies. At the same time, a characterization of the construction process itself remains an open research question. In essence, formal specifications to drive our implementation systems are needed, but the means of constructing such specifications in any disciplined manner are still lacking. The principal investigator proposes to collaborate with two U.K. research groups, one at the University of Edinburgh and one at Imperial College, London, in an effort to both formalize and automate a model of specification design. Up until this time, each of the three groups has focused on a different aspect of the specification problem: Edinburgh has focused on mapping from informal descriptions to formal specifications. Imperial College has focused on identifying necessary specification activities, and tracking the dependencies among them; the principal investigator has focused on knowledge-based approaches to specification analysis. Dr. Fickas, in cooperation with the two U.K. groups, will lead an effort to integrate the three approaches into a more general model of specification construction. The results will be twofold. First, the integration attempt itself will force each of other three current models to become more refined. Second, Dr. Fickas plans to incorporate parts of the Edinburgh and Imperial models into his existing computer-based system, thus providing further extensions to an automated tool for specification construction.