Static Detection of Bugs in Embedded Software Using Lightweight Verification

Award Information
Agency: National Aeronautics and Space Administration
Branch: N/A
Contract: NNC08CA25C
Agency Tracking Number: 066977
Amount: $600,000.00
Phase: Phase II
Program: SBIR
Awards Year: 2008
Solicitation Year: 2006
Solicitation Topic Code: X2.03
Solicitation Number: N/A
Small Business Information
315-317 N. Aurora Street, Ithaca, NY, 14850-4201
DUNS: 603978321
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Michael McDougall
 Principal Investigator
 (607) 273-7340
 mcdougall@grammatech.com
Business Contact
 Ray Teitelbaum
Title: CEO
Phone: (607) 273-7340
Email: tt@grammatech.com
Research Institution
N/A
Abstract
Validating software is a critical step in developing high confidence systems. Typical software development practices are not acceptable in systems where failure leads to loss of life or other high costs. Software best practices for high confidence systems are often codified as coding rules. Adhering to these practices can increase software readability and predictability, thereby enhancing quality. However, adherence is limited by the lack of high-quality tools to measure adherence automatically. Checking rule conformance requires a diverse set of software analysis technologies, ranging from syntactic analysis to sophisticated inference of runtime behavior. By combining lightweight verification techniques with other scalable analysis techniques that target syntactic and other static properties, we will create a tool that flags violations for almost all the rules typically applied to high-assurance code. Our Phase I work demonstrated the feasibility of this approach. In Phase I, we developed a tool for checking compliance with rules developed for JPL flight software. The tool leveraged GrammaTech's existing technology for static analysis, including facilities for analyzing a program's abstract syntax tree, control-flow graph, and inferred runtime behavior. The prototype successfully checks a set of rules designed for high-assurance software. Our experiments show that the tool adds only minimal overhead to our CodeSonar bug-finding tool, and generates few or no spurious results that could distract or annoy users.

* Information listed above is at the time of submission. *

Agency Micro-sites

SBA logo
Department of Agriculture logo
Department of Commerce logo
Department of Defense logo
Department of Education logo
Department of Energy logo
Department of Health and Human Services logo
Department of Homeland Security logo
Department of Transportation logo
Environmental Protection Agency logo
National Aeronautics and Space Administration logo
National Science Foundation logo
US Flag An Official Website of the United States Government