Verification of Real-Time Systems through Lazy Approximations

We develop in this thesis effective verification techniques for real-time systems based on novel combinations of theorem proving and model checking. Although the resulting algorithms do not improve the worst-case complexity, they are usually much more effective in practice, since state spaces are only explored on demand. Moreover, in contrast to dedicated model-checking techniques for real-time systems, our algorithms are not restricted to specific modeling formalisms such as timed automata, and are therefore applicable for a much larger class of problems. The main contribution, lazy approximation, is an effective and complete method for verifying safety and liveness properties of real-time systems, and is based on predicate abstraction for timed automata, finite-state model checking, and counterexample-guided abstraction refinement. This is the first time that predicate abstraction is used for model checking real-time systems specified with real-time logics. This method is also complete for verifying liveness properties. The proposed technique is lazy in that approximations of real-time systems are computed on demand and incrementally refined until the desired property is refuted or verified. In this way, lazy approximation is significantly less memory and time consuming than conventional, region graph based verification methods for real-time systems. Lazy approximation requires information about counterexamples from failed model-checking attempts on the abstract, finite state space. We define a general form of counterexamples both for CTL and TCTL logics, in a symbolic way, as sequences over sets of states. We use symbolic counterexamples in the abstraction-refinement algorithm as a heuristic for selecting new abstraction predicates from the given set of abstraction predicates. The use of symbolic counterexamples for the lazy refinement of approximations has two main advantages compared to refinement methods based on linear counterexamples. First, the refinement process converge more quickly towards a strongly preserving abstraction since multiple spurious counterexamples are discarded in every refinement step. Second, lazy approximation is applicable for full TCTL, and not only for a fragment of universal formulas as is the case when using linear counterexamples. Bounded model checking (BMC) has been recently introduced as a technique for finding bugs in finite state systems. We extend the BMC paradigm to timed automata and LTL formulas augmented with a decidable set of clock constraints, and show that this yields a complete refutation method for real-time systems. Through the technique of k-induction it is possible to extend BMC for timed automata to proof by induction, providing therefore a complete verification method for timed automata and invariant properties. The model-checking problem for real-time systems can be recast as a validity problem in an appropriate logic, which in turn can be solved using theorem proving. Unfortunately, the satisfiability problem for existing branching-time logics with dense-time models is undecidable. We introduce the Event-Recording Logic (ERL) as a real-time extension of the modal μ-calculus with clock variables. ERL is the first decidable real-time logic for specifying branching-time properties of real-time systems. The decidability problem is shown to be EXPTIME complete.

Online Copy

Thesis is available as PDF-File (247 pages / 1.6 MB)

BibTeX Entry

@phdthesis{sorea04:phd, author = {Maria Sorea}, title = "{Verification of Real-Time Systems through Lazy Approximations}", school = {Universit{\"{a}}t Ulm}, address = {Germany}, year = 2003, url = {http://www.informatik.uni-ulm.de/ki/Papers/sorea04-diss.pdf}}