Specification Editing and Discovery Assistant

Accurate safety analysis of software suffers from a lack of appropriate tools for software developers. Current automated tools require approximate analyses; fully-assured verification with formal methods is expert-intensive. A key to improvement is machine-checkable specifications for software modules. Specifications are also needed to express the intent of software. Further, to scale to wide use, engineers who are not formal methods experts must have usable tools, as automated as possible, integrated into their usual software development environments (IDEs). Our proposal, SPEEDY, is a user experience (UX) design for convenient generation, manipulation, and checking of specifications, directly in a common IDE (Eclipse). The tool's design integrates automated specification suggestion using current tools and published techniques. The tool also enables checking and debugging specifications directly in the IDE, with information presented in the context of the source code. The proposal targets C/C++ programs, particularly for embedded software development. Phase I of SPEEDY assessed current specification languages and prototyped the key UX mechanisms: we are now confident that they can be implemented in the Eclipse IDE. We also integrated several analysis tools, demonstrating that SPEEDY can obtain specification suggestions from external sources. We assessed many specification suggestion algorithms, selecting some to be implemented and evaluated on realistic software in Phase II. Phase I also prototyped the integrating specification checking tools and specification debugging features. We demonstrated SPEEDY on NASA software from the NASA open software site. The Phase II proposal presents a plan for scaling up the successful Phase I prototype in many dimensions: more language features; more sophisticated user guidance in generating and debugging specifications; more specification suggestion algorithms; scaled up to realistic program size.