Description: 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.

Benefits: We envision these use cases for SPEEDY's specification discovery and manipulation features: 1) Developers creating implementation and specifications together, with continuous automated checking 2) Developers writing code to specifications previously created by experts who have designed and verified core algorithms 3) Understanding and reverse engineering existing (legacy) code 4) Code Review of code under development 5) V&V teams inspecting developed code NASA has applications across these use cases. There are four particular categories of potential users. 1) NASA developers implementing safety-critical avionics or space-flight software can use SPEEDY in use cases 1, 2 and 4 above. SPEEDY helps them introduce formal methods into their work processes without having to swim (and sink) in the details of logics, provers, and verification conditions. 2) NASA formal methods teams have the task of verifying core designs and protocols. But once designed, the result must be communicated to developers and implemented correctly. Formal specifications provide a way to enable and check this communication, and SPEEDY provides a tool in which to accomplish it easily. This is use case #2. 3) NASA V&V teams can make ready use of use cases #4 and #5. 4) NASA developers faced with old code or changing team members will welcome the capabilities of use case #3.

Our target market for the eventual SPEEDY product is safety and security-critical software development engineers and organizations. We are building on the current trend toward more logical formality in software development. The bulk of that market develops embedded software; this is the same market space that is addressed by GrammaTech's existing products. We believe there is an early-adopter segment of that market that is willing to increase the level of model checking/software verification/formal reasoning during software development. But we are sure this need will be satisfied only if there are tools that provide the right capabilities, in the developers' working environment, targeted to non-formal-methods experts. This market growth will be particularly the case for embedded (and robotic) software, as such software will be increasingly important to an ever more technological society. We will initially focus our (non-NASA) marketing efforts on current customers who manufacture avionics systems, medical devices, and other safety-critical embedded systems (e.g. automotive software) – e.g., FDA, Covidien, Lockheed-Martin, and Honeywell. A second tier of relevant customers is development groups doing security analyses, security certification, and reverse engineering for understanding or maintenance.