NASA has awarded a contract to GrammaTech (News - Alert), Inc., a software developer specializing in software assurance tools and cybersecurity solutions, to prototype a specification editing and discovery tool (SPEEDY) for C/C++ code analysis.
Officials with GrammaTech said that the tool, packaged as a plug-in to the Eclipse integrated development environment (IDE), will assist software developers in modular formal verification tasks.
Company officials said that SPEEDY will provide automated suggestions of specifications for given contexts, with user interface features aiding developers in generating, editing and checking specifications.
"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," said Tim Teitelbaum (News - Alert), CEO of GrammaTech.
Teitelbaum added that 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.
According to company officials, SPEEDY will support the needs of NASA's software development teams and Independent Verification and Validation (IV&V) groups.
Earlier in April, GrammaTech announced that the company has been awarded more than $8 million in research contracts.
GrammaTech performs sponsored research for many branches of the U.S. government. Over its 25-year history, government customers have included the Department of Defense (DOD), the Department of Homeland Security (DHS), the National Aeronautics and Space Administration (NASA), the National Institute of Standards and Technology (NIST) and the National Science Foundation (NSF). In the past four months, the company submitted eight proposals, six of which have been selected for funding. The remaining two are still pending.
GrammaTech’s research department undertakes the full life cycle of new ideas – from government-sponsored research, through advanced, technology-ready prototypes, into widely-adopted COTS (commercial-off-the-shelf) products. The department focuses on automatic program analysis, including both static and dynamic analysis on source code and binary machine code.
Edited by Alisen Downey