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

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

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.