Automating Verification of Cooperation, Control, and Design in Traffic Applications - Formal Methods and Hybrid Real-Time Systems - page 158

excluded. Since the reasons are fully independent from the discrete behavior, the
approach converges fast also for huge discrete state spaces.
The implementation is currently restricted to step-discrete linear hybrid mod-
els being represented as a discrete transition graph where the transitions are
guarded by linear constraints ( guard expressions ) and extended with linear trans-
formations ( computations ) on the set of continuous variables. This corresponds
exactly to the semantics of linear reactive systems being modeled in industrial
contexts based on CASE-tools, where executable target code can be generated
from. Thanks to an appropriate compiler and the realization of the algorithm on
a symbolic representation level, the procedure can be applied to the generated
C code of such models even for very large systems.

Initial abstraction. To verify a property ϕ , the procedure starts by creating an
initial abstraction A 0 of a hybrid automaton H by removing all guard expressions
and computations on continuous items, but fully preserving the discrete structure
of the model. This entails a translation of ϕ to a new property ϕ to hold for
some corresponding states in A 0 .

Analysis phase. A 0 can be analyzed by any finite state model checker being able
to generate a counterexample π . The counterexample π consisting of a sequence
of discrete states is analyzed by projecting it to the hybrid automaton H to
retrieve the corresponding guard expressions and computations ( regulation laws )
that have to be fulfilled or performed in H , respectively, for π to be a valid
counterexample. For linear hybrid automata, this analysis consists of solving
conjunctions of linear constraints directly derived from the projected regulation
laws. The result of this analyzation is either a valid sequence of valuations of
continuous state variables or a generalized conflict ( ρ 1 ,ρ 2 ,...,ρ k ) consisting of
a minimized sequence of partial regulation laws for which no solution exists in
the corresponding conjunctive formula.
Since such conflicts are fully independent of the discrete state sequence they
occurred with, there is a high probability that they apply to many other frag-
ments of the discrete transition system as well, especially for huge discrete state
spaces combined with only few regulation laws exhibited by the model.

Construction of ω -automaton. Thus we follow a strategy of completely ruling
out generalized conflictsbyconstructingan ω -automaton A C that accepts all
runs not containing any known conflict as a subsequence. Considering partial
regulation laws as atomic characters and C as the set of all previously detected
generalized conflicts, the behavior of A C

can be described by an LTL formula:

A C | = ¬ F ( ρ 1 ∧ X( ρ 2 ∧ X( ... ∧ X ρ n ))) (21)

( ρ 1 ,ρ 2 ,...,ρ k ) ∈ C

Instead of using standard algorithms to translate LTL formulae to Büchi-auto-
mata, we apply an ecient automaton construction algorithm dedicated to the
structure of LTL formulae as presented above, resulting in rather small automata,
especially in comparison to general Büchi-automata construction algorithms [50].