Grande Salle de VERIMAG
16 February 2010 - 14h00
Automated Invariant Generation for the Verification of Real-Time Systems
by Bahareh Badban from University of Konstanz
Abstract: Although real-time model checking has significantly advanced the quality of
safety-critical systems, the demand for more rigorous verification methods is
still increasing. The modeling of many such systems requires dense time
domains to reflect the fact that events may happen arbitrarily close to each
other in actual applications. Therefore, timed automata has emerged as the de
facto standard for modeling real-time concurrent systems. Timed automata
represent uncountable infinite state spaces for which the size of state space
grows exponentially dependent on different parameters; such as number of
clocks, and system components. Because of the concurrent and dense nature of
most real-life designs, verification of such models is substantially
challenging. To overcome this challenge, abstraction methods, in particular
region-based as well as zone-based abstraction as well as predicate
abstraction are being implemented by model checking tools. While, finding a
suitable abstraction has become essential in checking the model of a
nontrivial real-time system within the limited time and memory space,
unfortunately most of the existing tools, e.g. UPPAAL, do not provide any
method to simplify the automata under study. As states in [1]:
We would like to stress (and lament) the fact that current tools do not
provide any assistance worthy of the name when it comes to simplifying
automata. Such assistance would help avoiding conceptual mistakes and
would render simplification less tedious to implement. We can only wish
that the increasing popularity of model checking techniques will lead
to the development of true all-inclusive computer-assisted formal
verification environments. The various simplification methods, applied
to automata and in ubiquitous use today, can be justified
formally. Such a task adds credence to the methods, while delimiting
their application domains and bringing some indispensable precautions
to the fore. (P. 125)
To contribute to the automated simplification and verification, of dense
real-time we introduce the CIPM algorithm which would approach the problem by
searching the system’s “hidden†invariants, which can be used in the
simplification step. These invariants augment the model by bringing to light
timing conditions which implicitly constrained the behaviour of the
system. The algorithm detects and prunes away those discrete transitions which
true running the model are never enabled.
This is the first step towards developing a richer Counterexample Guided
Abstraction Refinement (CEGAR) based technique for the verification of
concurrent dense timed systems. The simplified and augmented time automata,
serving as the starting point for CEGAR, would reduce the refinement
iterations by avoiding much of spurious counter-examples. In our CEGAR, we
envision abstractions based upon the newly generated invariants which would be
considered as predicates. Predicate-abstraction subsumes zone-based
abstraction.
Although real-time model checking has significantly advanced the quality of
safety-critical systems, the demand for more rigorous verification methods is
still increasing. The modeling of many such systems requires dense time
domains to reflect the fact that events may happen arbitrarily close to each
other in actual applications. Therefore, timed automata has emerged as the de
facto standard for modeling real-time concurrent systems. Timed automata
represent uncountable infinite state spaces for which the size of state space
grows exponentially dependent on different parameters; such as number of
clocks, and system components. Because of the concurrent and dense nature of
most real-life designs, verification of such models is substantially
challenging. To overcome this challenge, abstraction methods, in particular
region-based as well as zone-based abstraction as well as predicate
abstraction are being implemented by model checking tools. While, finding a
suitable abstraction has become essential in checking the model of a
nontrivial real-time system within the limited time and memory space,
unfortunately most of the existing tools, e.g. UPPAAL, do not provide any
method to simplify the automata under study. As states in [1]:
We would like to stress (and lament) the fact that current tools do not
provide any assistance worthy of the name when it comes to simplifying
automata. Such assistance would help avoiding conceptual mistakes and
would render simplification less tedious to implement. We can only wish
that the increasing popularity of model checking techniques will lead
to the development of true all-inclusive computer-assisted formal
verification environments. The various simplification methods, applied
to automata and in ubiquitous use today, can be justified
formally. Such a task adds credence to the methods, while delimiting
their application domains and bringing some indispensable precautions
to the fore. (P. 125)
To contribute to the automated simplification and verification, of dense
real-time we introduce the CIPM algorithm which would approach the problem by
searching the system’s “hidden†invariants, which can be used in the
simplification step. These invariants augment the model by bringing to light
timing conditions which implicitly constrained the behaviour of the
system. The algorithm detects and prunes away those discrete transitions which
true running the model are never enabled.
This is the first step towards developing a richer Counterexample Guided
Abstraction Refinement (CEGAR) based technique for the verification of
concurrent dense timed systems. The simplified and augmented time automata,
serving as the starting point for CEGAR, would reduce the refinement
iterations by avoiding much of spurious counter-examples. In our CEGAR, we
envision abstractions based upon the newly generated invariants which would be
considered as predicates. Predicate-abstraction subsumes zone-based
abstraction.
