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.
