U.S.-France Cooperative Research: Integrating a Theorem Prover and a Specification Environment

该奖项将支持麻省理工学院的John Guttag博士和Stephen Garland博士与法国巴黎大学Recherche Information atique的Michel Bidoit博士和Christine Choppy博士在软件工程方面的合作研究。研究人员提出了一个联合项目，首先将巴黎大学南德分校正在开发的规范环境AsSegigue与麻省理工学院正在开发的定理证明系统LP相结合。然后，他们将试验使用组合系统来开发和推理规范。现在人们普遍认为，精确的规范可以在软件开发和维护中发挥有用的作用。构建系统中最令人头疼的问题涉及整体系统组织和组件集成。模块化是控制这一点的关键，而规范是实现模块化的关键。美国和法国的研究小组都采用了一种强调简洁和清晰、而不是可执行性的规范风格。为了使在不执行或实现规范的情况下测试规范成为可能，两个小组都开发了使说明者能够声明规范的逻辑属性的技术。然而，法国人的研究集中在生产和管理大规模规范所需的技术上，而麻省理工学院的团队则集中在检查规范逻辑属性声明所需的技术上。通过将这两项互补的研究工作结合起来，研究人员计划生产一种工具，可以用来开发、推理和管理大规模的软件正式规范。

This award will support collaborative research in software engineering between Drs. John Guttag and Stephen Garland, Massachusetts Institute of Technology and Drs. Michel Bidoit and Christine Choppy, Laboratoire de Recherche Informatique, University of Paris-Sud, France. The investigators propose a joint project that will first work on combining Assegigue, a specification environment under development at the University of Paris-Sud, and LP, a theorem proving system under development at MIT. They will then experiment with using the combined system to develop and reason about specifications. There is now widespread agreement that precise specifications can play a useful role in software development and maintenance. The most vexing problems in building systems deal with overall system organizations and the integration of components. Modularity is the key to controlling this, and specifications are essential for achieving modularity. Both the US and French research groups have adopted a style of specification that emphasizes brevity and clarity rather than executability. To make it possible to test specifications without executing or implementing them, both groups have developed techniques that enable specifiers to make claims about logical properties of specifications. However, whereas the French have centered their research around the technology needed to produce and manage large scale specifications, the MIT group has centered its research around the technology needed to check claims about logical properties of specification. By combining these two complementary research efforts, the investigators plan to produce a tool that can be used to develop, reason about and manage large-scale formal specifications of software.