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

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

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.