Specification Editing and Discovery Assistant

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. More »