USA flag logo/image

An Official Website of the United States Government

Verification of Hierarchical Graph Structures

Award Information

Agency:
Department of Defense 		Branch:
Defense Advanced Research Projects Agency 		Award ID:
53293 		Program Year/Program:
2001 / SBIR
Agency Tracking Number:
01SB1-0073 		Solicitation Year:
N/A 		Solicitation Topic Code:
N/A 		Solicitation Number:
N/A
Small Business Information
GrammaTech, Inc
317 N. Aurora Street Ithaca, NY -
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
 

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.

Principal Investigator:

Paul Anderson
Senior Software Engineer
6072737340
paul@grammatech.com

Business Contact:

Ray(Tim) Teitelbaum
Chairman
6072737340
tt@grammatech.com
Small Business Information at Submission:

GRAMMATECH, INC.
317 N. Aurora Street Ithaca, NY 14850

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