GrammaTech, a software developer specializing in software assurance tools and cybersecurity technology, received an award from NASA to prototype a specification editing and discovery tool (SPEEDY) for C/C++ code analysis.
Packaged as a plug-in to the Eclipse integrated development environment (IDE), the tool will assist software developers in modular formal verification tasks. SPEEDY provides automated suggestions of specifications for given contexts, with user interface features aiding developers in generating, editing, and checking specifications.
SPEEDY will support the needs of NASA’s software-development teams and Independent Verification and Validation (IV&V) groups. The tool will assist NASA personnel in evaluating the safety and robustness properties of software in production, including embedded nextgeneration 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.