Verification of Hierarchical Graph Structures
Embedded systems software is being used for increasingly complex and safety-critical applications (intercontinental ballistic missile interception, landing a probe on a comet, unmanned flight control, etc). In order to ensure the safe and successful operation of these applications we must verify their safety and mission-critical properties, and reduce reliance on a testing process that can only detect the presence of faults. To ensure the safety properties of these complex systems we must augment traditional testing techniques with software verification.
GrammaTech believes that the current software validation process needs to be augmented with verification of safety and mission-critical properties. We propose to use model checking to address this verification need. Model checking is a verification technique that can be used to check cross-cutting concerns of a system such as liveness and deadlock-freedom. Model checking has been applied successfully to hardware designs, where the state space is flat. However, it has yielded only limited success in the software-verification realm due to the fact that the global state space of a program is inherently non-flat—it has a hierarchical form caused by the procedure call-return patterns corresponding to feasible executions of the program. Attempts to get around this by inlining procedures leads to an explosion in the size of the model to be checked, which causes severe scalability problems.
Exploitation of modularity has been recognized as a means of increasing the scalability of model checking. GrammaTech co-founder and President Tom Reps has exploited the inherent modularity in procedural abstraction in his work on dataflow analysis. Under this DARPA SBIR contract, GrammaTech is developing similar methods for model checking. GrammaTech is developing a novel technique for model checking of hierarchically-structured graphs based on the concept of context-free-language reachability. This technique will be applicable to cross-cutting concerns of programs. Such concerns are inherently global properties of the system, and hence must be inter-procedural in nature.
Presentations:
- Program Composition for Embedded Systems (PCES) May 2001 Presentation (Powerpoint Presentation)