High level verification of control intensive systems using predicate abstraction
- 1 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Predicate abstraction has been widely used for model checking hardware/software systems. However, for control intensive systems, existing predicate abstraction techniques can potentially result in a blowup of the size of the abstract model. We deal with this problem by retaining important control variables in the abstract model. By this method we avoid having to introduce an unreasonable number of predicates to simulate the behavior of the control variables. We also show how to improve predicate abstraction by extracting useful information from a high level representation of hardware/software systems. This technique works by first extracting relevant branch conditions. These branch conditions are used to invalidate spurious abstract counterexamples through a new counterexample-based lazy refinement algorithm. Experimental results are included to demonstrate the effectiveness of our methods.Keywords
This publication has 6 references indexed in Scilit:
- Counterexample-guided abstraction refinementPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- The semantic challenge of Verilog HDLPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Lazy abstractionPublished by Association for Computing Machinery (ACM) ,2002
- Automatic predicate abstraction of C programsPublished by Association for Computing Machinery (ACM) ,2001
- Property preserving abstractions for the verification of concurrent systemsFormal Methods in System Design, 1995
- Model checking and abstractionPublished by Association for Computing Machinery (ACM) ,1992