Grande Salle de VERIMAG

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.