Information Technology Reference
In-Depth Information
Approximations.
Currently, our model checker only supports models with dy-
namics given by constants. In the train example, the dynamics
v
•
in mode
Nor-
malMove
(controlled by a PID controller) relies on the difference between
v
d
and
v
(see Fig. 6), and the evolution for the position
p
is normally defined as
p
•
=
v
.
Therefore, both
v
•
and
p
•
are linear if
v
is a variable. So the train system cannot
be described and checked directly by our approach. We need to have an over-
approximation of the train's behavior using the method developed in [26]. First,
the mode
NormalMove
is split into a set of sub-modes, we define accelerations
v
•
as constants, depending the relation between
v
and
v
d
. Second, for each mode
defined in the previous section (together with sub-modes for
NormalMove
), we
divide the speed into several regions, and use this information to safely over-
approximate the evolution of the position
p
•
by its possible maximal changing
rate. Therefore, the number of modes depends on the concrete approximation.
The constraints on the speed and the desired speed and the constraints whether
the train has reached the positions
EoA
SB
(start-
braking), are treated as the boundary conditions for each mode. An appropriate
mode is selected depending the phase of the cooperation protocol, current ve-
locity
v
and its relation to
v
d
. For instance, if
v
d
≥
−
ST
(start-talking) or
EoA
−
40
.
0,and
the cooperation protocol is in the
FAR
phase, then the speed controller of the
train will choose a mode with
v
•
=2
.
0 (a fast acceleration) and
p
•
=40
.
0 (the
maximal changing rate of
p
). The condition
v
d
1
.
5
·
v
, 30
.
0
≤
v
≤
40
.
0
will be part of the boundary condition for such mode. The condition whether the
crossing is secured is treated as a discrete input. The decisions in the cooperation
protocol constitute discrete transitions in the model.
≥
1
.
5
·
v
and 30
.
0
≤
v
≤
Experimental results.
The safety property for the models is that the
FAIL
phase
can never been entered, i.e., the train comes to a complete stop in front of the
crossing if it is not secured. For the continuous-time models, we have successfully
proven the given safety invariant for a model with 16 modes in 376 seconds. The
final state set representation contained 3906 Lin-AIG nodes with 2358 linear
constraints. During model checking, up to 7798 Lin-AIG nodes were used, 36683
HySAT calls occurred and 2582 redundant linear constraints were removed. Ex-
periments are performed on a PC with an AMD Opteron Processor with 2.6
GHz and 16 GB RAM.
7.3
Iterative Abstraction Refinement for Step-Discrete Linear
Hybrid Systems
Alternatively, an iterative abstraction refinement approach called
ω
-Cegar [48] is
being developed with the focus on open-loop systems, exploiting the characteris-
tics of huge discrete state spaces by ruling out comprehensive classes of spurious
counterexamples for subsequent iterations, so that counterexamples with com-
mon reasons of invalidity cannot occur again. With the incremental construction
of an omega-automaton and its parallel composition with a course abstraction
of the model, all runs containing already detected reasons of being invalid are
Search WWH ::
Custom Search