Skip Navigation
Small Business Innovation Research/Small Business Tech Transfer

A Scalable Semantics-Based Verification System for Flight Critical Software

Completed Technology Project

Project Description

A Scalable Semantics-Based Verification System for Flight Critical Software, Phase II

Flight-critical systems rely on an ever increasing amount of software—the Boe- ing 777 contains over 2 million lines of code. Most of this code is written in the C programming language. We need a scalable static formal program verification tool that is able to prove the functional correctness of flight-critical software, limiting any failure of flight critical software to hardware faults. This project seeks to leverage the matching logic verification framework. Matching logic is generic in an operational semantic of a given programming language, so we also seek to give a semantics of a subset of C, called CIL, which is guaranteed to be deterministic. While we already have a semantics for the entirety of C, CIL is more representative of flight-critical software, and the simpler, deterministic semantics will result in a more efficient, and thus more scalable, static program verification tool. We are also building a new unification- based rewrite engine that will result in a more powerful version of the Matching Logic Framework. In order to make the tool more commercially feasible, we will develop new techniques in pattern inference, so that loop invariants and some pre/post conditions can be determined automatically. We will perform a thorough evaluation of our tool on a large-scale piece of software with similar characteristics to a flight system.

More »

Anticipated Benefits

Project Library

Primary U.S. Work Locations and Key Partners

Technology Transitions

Light bulb

Suggest an Edit

Recommend changes and additions to this project record.