Small Business Innovation Research/Small Business Tech Transfer
A Runtime Verification System for Developing, Analyzing and Controlling Complex Safety-Critical Software
Project Description
A comprehensive commercial-grade system for the development of safe parallel and serial programs is developed. The system has the ability to perform efficient parametric runtime verification of programs. This can be used to ensure the safety of mission critical systems at runtime. The system also has the ability to extrapolate all feasible program traces deriving from thread inter-leavings that meet the casual dependencies of a program from a single running. These feasible traces can be checked, using the same parametric trace slicing algorithm used for runtime verification, against safety properties. An extensive evaluation of the system on software critical to NASA is also performed, with the aid of Klaus Havelund.
More »
Anticipated Benefits
The Non-NASA applications are much the same. Not all companies produce software that is as safety critical as NASA, but even those that do not will benefit from the ability to rigorously test formal safety policies in pre-production software, and guarantee safety in production software. Predictive runtime analysis only becomes more important as commercial software adapts to the massively multi-core future.
The software developed by NASA is particularly safety critical. Our tool will allow NASA not only to test the safety of pre-production software, but also to guarantee safety of portions of software systems at runtime. The addition of predictive runtime analysis will allow NASA to easily find safety violations in multi-threaded programs. More »
The software developed by NASA is particularly safety critical. Our tool will allow NASA not only to test the safety of pre-production software, but also to guarantee safety of portions of software systems at runtime. The addition of predictive runtime analysis will allow NASA to easily find safety violations in multi-threaded programs. More »
Primary U.S. Work Locations and Key Partners
| Organizations Performing Work | Role | Type | Location |
|---|---|---|---|
| Runtime Verification Inc | Lead Organization | Industry | Champaign, Illinois |
Ames Research Center
(ARC)
|
Supporting Organization | NASA Center | Moffett Field, California |
Primary U.S. Work Locations
-
California
-
Illinois
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.