According to Tim Teitelbaum, GrammaTech’s CEO, SPEEDY will provide automated suggestions of specifications for given contexts, with user interface features aiding developers in generating, editing and checking specifications and will operate as a plug-in to the Eclipse integrated development environment (IDE).
“SPEEDY will essentially be able to look over your shoulder, using machine-checkable specifications to automate sound verification and warn you if something isn’t right,” he said. “The user interface features, and underlying automation in SPEEDY, will facilitate the use of formal methods by all software developers, improving efficiency and accuracy of development teams.”
He said SPEEDY will be designed to support the needs of NASA’s software-development teams and Independent Verification and Validation (IV&V) groups.
The tool will be able to assist NASA personnel in evaluating the safety and robustness properties of software in production or under review, including embedded next-generation avionics and space software.
The tool will also serve as a natural companion to the heuristic bug-finding and style-checking tools GrammaTech has completed for NASA’s Jet Propulsion Laboratory (JPL) in the past.