USA flag logo/image

An Official Website of the United States Government

Verification of Hierarchical Graph Structures

Award Information

Department of Defense
Defense Advanced Research Projects Agency
Award ID:
Program Year/Program:
2001 / SBIR
Agency Tracking Number:
Solicitation Year:
Solicitation Topic Code:
Solicitation Number:
Small Business Information
GrammaTech, Inc
531 Esty Street Ithaca, NY 14850-
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
Phase 1
Fiscal Year: 2001
Title: Verification of Hierarchical Graph Structures
Agency / Branch: DOD / DARPA
Contract: DAAH0101CR129
Award Amount: $98,941.00


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.

Principal Investigator:

Paul Anderson
Senior Software Engineer

Business Contact:

Ray(Tim) Teitelbaum
Small Business Information at Submission:

317 N. Aurora Street Ithaca, NY 14850

EIN/Tax ID: 161338879
Number of Employees:
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No