pdf
postscript
ps.gz
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 mu-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.
PhD thesis, University of Ulm, Germany, July 2004.
@PhdThesis{Sorea04,
author = {Maria Sorea},
title = {Verification of real-time systems through lazy approximations},
school = {University of Ulm},
year = 2004,
address = {Germany}
}