Verification of Hierarchical Graph Structures

Award Information
Agency:
Department of Defense
Amount:
$98,941.00
Program:
SBIR
Contract:
DAAH0101CR129
Solitcitation Year:
N/A
Solicitation Number:
N/A
Branch:
Defense Advanced Research Projects Agency
Award Year:
2001
Phase:
Phase I
Agency Tracking Number:
01SB1-0073
Solicitation Topic Code:
N/A
Small Business Information
GRAMMATECH, INC.
317 N. Aurora Street, Ithaca, NY, 14850
Hubzone Owned:
N
Woman Owned:
N
Socially and Economically Disadvantaged:
N
Duns:
603978321
Principal Investigator
 Paul Anderson
 Senior Software Engineer
 (607) 273-7340
 paul@grammatech.com
Business Contact
 Ray(Tim) Teitelbaum
Title: Chairman
Phone: (607) 273-7340
Email: tt@grammatech.com
Research Institution
N/A
Abstract
Embedded systems software is being used for increasingly complex and safety-critical applications. In order to ensure the safe and successful operation of these applications we must verify their safety and mission critical properties, and reduce relianceon a testing process that can only detect the presence of faults. Model checking is a verification technique that allows users to verify cross-cutting properties of systems. Model checking has been successfully applied to hardware designs, but has onlyyielded limited success in the software verification realm due to scalability issues. Exploitation of modularity has been recognized as a means of increasing the scalability of model checking. We propose a new context-free language reachability based modelchecking technique that allows us to exploit the inherent modularity in procedural abstraction. We also propose using our dependence graph and program slicing technology to construct models of a reduced size. We believe our technology will significantlyincrease the scalability of model checking, allowing it to be applied to complex safety-critical embedded systems.The proposed system will be of use in improving the quality of safety and mission-critical software in embedded systems. This system willallow companies to develop highly reliable embedded real-time systems.

* information listed above is at the time of submission.

Agency Micro-sites

US Flag An Official Website of the United States Government