Information Technology Reference
In-Depth Information
Abstraction refinement.
A parallel composition
A
=
A
0
×
A
C
ensures that any
(infinite) run not accepted by
A
C
cannot be exhibited by
A
.With
A
C
being
incrementally extended to not accept conflicts found in subsequent model check-
ing iterations, we get a sequence
A
1
,
A
2
,...,
A
n
of refined abstract transition
systems, where the model checker can finally prove that either
A
k
|
=
ϕ
from
=
ϕ
or that a counterexample
π
violates
ϕ
with
π
having a valid projection to a path
π
in
H
as computed in the analysis phase.
|
which can be concluded that
H
Remarks.
The finite state model checker used to verify the abstract system in
each iteration can be freely exchanged even in between iterations. Thus, advan-
tages of different technologies can be combined by
1. starting with (faster) bounded model checking (BMC) while counterexam-
ples within the given bound can be generated and
2. switching to unbounded model checking (e.g., CTL model checker) if no
counterexamples within a given bound
k
are found anymore.
This way computation times of iteration cycles can be kept short while being
able to prove if a property
ϕ
holds for a model (
certification
). However, since
the approach is a semi-decision one, armation of properties might fail even by
using unbounded model checkers.
The restriction to step-discrete linear hybrid models is due to the implementa-
tion only and does not follow from the approach. Currently, only safety properties
can be verified. An extension to CTL-formulae is possible with the limitation,
that valid infinite counterexamples cannot be confirmed as such.
7.4
Discrete-Time Modes and Verification Results
Our abstraction-refinement approach deals with step-discrete linear hybrid sys-
tems modelled as discrete transition graphs, in which assignments and transition
guards may use linear arithmetical expressions, this subsumes the capability to
describe the evolvement of plant variables by linear equations. Hence, the approx-
imations in Subsection 7.2 are not necessary. The discrete-time models of our ex-
ample can be derived from the Matlab-Simulink model with a given sampling rate
δ
. The discrete transitions for the cooperation protocol and for mode-switchings
in the speed supervision are encoded exactly the same as in the continuous-time
models (see Subsection 7.2). In this part, we focus on time-discretization of the
plant behavior. Our main assumption is that the acceleration of the train during
a discrete time step keeps unchanged. If the train is in the modes of
MotorOff
,
EmergencyBraking
and
ServiceBraking
, the velocity and position of the train
can be simply updated by
v
δ
2
/
2,where
a
is the constant deceleration for those modes. If the train is in the
Normal-
Move
mode, the formulas for computing acceleration are given in the form of
f
and
g
in Fig. 14. Hence, we can calculate the train's new acceleration using
a
=
c
1
·
a
and
p
=
v
+
δ
·
=
p
+
v
·
δ
+
a
·
v
d
at each discrete time step (
c
1
,
c
2
,
c
3
are constants
in Fig. 14). Updates of the velocity and position can be done in the same way
(
v
−
v
d
)+
c
2
·
s
+
c
3
·
Search WWH ::
Custom Search