Skip Navigation

Static Detection of Bugs in Embedded Software Using Lightweight Verification, Phase II

Completed Technology Project

Project Introduction

Static Detection of Bugs in Embedded Software Using Lightweight Verification, Phase II
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. More »

Primary U.S. Work Locations and Key Partners

Project Library

Share this Project

Organizational Responsibility

Project Management

Project Duration

Light bulb

Suggest an Edit

Recommend changes and additions to this project record.

This is a historic project that was completed before the creation of TechPort on October 1, 2012. Available data has been included. This record may contain less data than currently active projects.