A Scalable Semantics-Based Verification System for Flight Critical Software
Project Description
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
We anticipate that our tool and definition of CIL will be used in verification of all safety and mission critical flight systems. NASA has shown themselves to be very amenable to formal methods techniques in the past. Our technical contact within NASA expects such a tool to be used on vehicles targeted at manned space missions as well as mission critical systems such as the rockets, probes, space telescopes, and landers/rovers.
TAM for our work would be the entire software industry. Realistically, we do not have the manpower to target the entirety of the software industry. A more reasonable SAM would be those companies in the software industry where correctness is key, either because bugs are very expensive to fix (Microsoft) or where bugs are disastrous to life and limb (NASA/Boeing/medical device manufacturers). We feel that our realistic SOM is larger software development corporations that would be willing to pay larger amounts for site licenses as well as be willing to hire on verification engineers from our Runtime Verification, Inc. This will allow us to leverage our smaller number of employees in a way that results in maximal possible profits, versus marketing to smaller software developers, which will be less willing to pay for site licenses. We can move into that segment of the market later, once Runtime Verification is able to grow. Initially, we would like to focus on Aerospace companies (Boeing), Automotive (Toyota-ITC, DENSO), Finance (2Sigma), Microsoft (in particularly Windows and Office), Apple (OS X), the US Military, NSA, the large hadron collider, and Facebook (they have already shown themselves amenable to formal methods tools).
Project Library
Primary U.S. Work Locations and Key Partners
| Organizations Performing Work | Role | Type | Location |
|---|---|---|---|
| Runtime Verification Inc | Lead Organization | Industry | Champaign, Illinois |
Langley Research Center
(LaRC)
|
Supporting Organization | NASA Center | Hampton, Virginia |
Primary U.S. Work Locations
-
Illinois
-
Virginia
