DiRePro : Real-Time Systems
Heuristic Search and Abstract Model Checking for Real-Time Systems
This subproject considers highly concurrent real-time systems and develops model checking techniques that combine heuristic search with abstraction.
In the automated verification of timed systems, one has to account for two sources of state explosion. Firstly, the control part can lead to state explosion resulting from the number of states that is exponential in the number of parallel processes in a concurrent systems. Secondly, since the clock variables range over the infinite data domain of reals, the data part leads to an infinite number of states. So far, no verification method exists for real-time systems that scales in both the number of parallel processes and the number of clocks; such a method must attack the two sources in an interleaved fashion. There is a promising potential of synergy resulting from the combination of two approaches, namely heuristic search and abstraction. Directed model checking and AI planning based on heuristic search are techniques to deal with the first source of state explosion. Abstraction in combination with automated abstraction-refinement is a technique to deal with the second source.
This subproject considers the use of heuristic search and directed model checking in the analysis of real-time systems. In particular, we consider the development of a heuristics-supported abstraction refinement method for concurrent real-time systems based on the notion of counterexample guided abstraction refinement. The refinement step is improved by the use of directed explicit state model checking in the generation of counterexamples. The context is the automated verification method for an infinite-state system that iterates the following four steps:
- Use a given abstraction function to construct a finite-state abstraction of the infinite-state system. For instance, in the first iteration the abstraction function can ignore all clock variables and keep only the control flow.
- Check the finite-state system, and if the finite-state system exhibits an error, return an error trace (counter-example) of the finite-state system.
- Check whether an error trace of the finite-state system is also an error trace of the infinite-state system by symbolic execution of its sequence of instructions.
- If the error trace is spurious, extract information from it to return a more precise abstraction function and restart with (1).
Step (1) eliminates the 'data' part of the state explosion problem but not the 'control' part. That is, the finite-state system constructed in Step (1) is still large (exponential in the number of parallel components) but is no longer subject to the exponential blow-up due to clock variables. Heuristic search has proven a good means to address that problem. More important, however, is its effect in finding short error traces. Short error traces are crucial for the abstraction refinement, i.e., the construction of a more precise abstraction function in Step (4). This is because a short error trace facilitates the generation of new predicates in the subsequent refinement steps and it helps to minimize their number. The abstraction refinement step is presently the bottleneck in the application of the verification method described above which is why we focus our attention here. Currently, the verification technology we develop will be capable of handling timed automata as well as PLC-automata (which can be reduced to timed automata). We will also investigate how to exploit the structural information contained in PLC-automata in the determination of search heuristics. In later funding periods we will also investigate how we can exploit the special structure of CSP-OZ-DC specifications.
- Bahareh Badban, Stefan Leue, Jan-Georg Smaus: Automated Predicate Abstraction for Real-Time Models, INFINITY 2009, 11th International Workshop on Verification of Infinite-State Systems, 2009. (PDF)
- Bahareh Badban, Stefan Leue, Jan-Georg Smaus: Automated Invariant Generation for the Verification of Real-Time Systems, in the International Workshop on Invariant Generation (WING), 2009. (PDF)
- Bahareh Badban: A Term Rewriting Technique for Decision Graphs, in the International Workshop on Computing with Terms and Graphs (TERMGRAPH), 2009. (PDF)
- Bahareh Badhan: Prove with GDPLL-WD. A Complete Proof Procedure for Recursive Data Structures, Technical Report soft-08-07, Chair for Software Engineering, University of Konstanz, 2008. (PDF)
- Bahareh Badban: Culling predicates for the Verification of Real-Time Models, Technical Report soft-08-06, Chair for Software Engineering, University of Konstanz, 2008. (PDF)