Static Detection of Bugs in Embedded Software Using Lightweight Verification

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$599,999.00
Award Year:
2008
Program:
SBIR
Phase:
Phase II
Contract:
NNC08CA25C
Award Id:
83829
Agency Tracking Number:
066977
Solicitation Year:
n/a
Solicitation Topic Code:
n/a
Solicitation Number:
n/a
Small Business Information
315-317 N. Aurora Street, Ithaca, NY, 14850
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
603978321
Principal Investigator:
Michael McDougall
Principal Investigator
(607) 273-7340
mcdougall@grammatech.com
Business Contact:
Ray Teitelbaum
CEO
(607) 273-7340
tt@grammatech.com
Research Institute:
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

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government