Static Detection of Bugs in Embedded Software Using Lightweight Verification

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.

The proposed tool will search source code and flag those parts that do not conform to coding standards and best practices. The tool will improve software development by:

Identifying non-conformant code that slips through other quality control efforts, and thereby increase software quality.
Reducing the effort required for manual code review. Code inspectors can spend more time on identifying subtle flaws in software and less on checking rule compliance.
Encouraging codification and application of best practices.

The presence of a tool to define and check coding rules will make it easier for engineers and project managers to apply best practices to projects that would otherwise ignore them because manual inspections are too cumbersome. We expect the Phase II work will be applicable in any industry that develops high confidence software. Department of Defense projects often adopt their own coding standards for safety-critical software (for example, the Joint Strike Fighter project). Defense contractors can use the proposed tool to identify non-compliant code cheaply, increasing productivity and software quality. Other industries that develop high-assurance code, such as the automotive, medical device, and banking industries, can apply the tool to enhance their own development processes.

The proposed tool will be applicable to all NASA centers and contractors that develop or validate flight software written in C/C++. Flight software must meet a higher standard of quality than typical general-purpose software, and a common technique for encouraging quality software is by applying coding rules. For example, Holzmann's Ten Rules are being adopted for mission-critical flight software across JPL. The proposed tool will search source code and flag those parts that do not conform to the rules.