Information Technology Reference
In-Depth Information
Tabl e 1 . It shows: number of continuous dimensions (
inputs
+
state-based
), number
of exhibited regulation laws/generalized partial regulation laws, number of conflicts,
iterations, final path length, size of
A
C
in terms of statebits, and total runtime.
dimensions regulation laws conflicts iterations
| π |
A
C
time
Proof
¬
(
v
=0
⇒
p
≤
EoA
)
0+10
34
31
15
3 3 min
as for other modes. Here,
s
denotes the integration part of the PI controller (see
Equation (2)), and it is accumulated at each step by
s
=
s
+(
v
d
−
v
)
·
δ
,where
v
=
v
+
a
δ
denotes the average velocity during the time interval
δ
.
Table 1 shows statistical data of the application of the
ω
-Cegar approach to
a central part of the train system presented in Section 2: to prove that the train
always stops before the crossing if it is not secured. The property was certified
within 3 minutes and only 15 iterations by first using BMC (Prover-CL V5.0.6)
for the iterations and switching to an unbounded model checker (VIS Version
2.0) to finally prove the unreachability on the refined model, which consisted of
16 state bits.
·
8
Conclusion and Future Work
Industrial design processes for cooperating trac agents exploit a layered design
structure to separate concerns in addressing cooperation strategies, control de-
sign, and design implementation. We have provided a verification methodology
covering these design steps, where safety and stability properties resulting from
the overall safety objective of collision freedom are traced to design entities at
all levels, and have provided layer specific verification approaches to establish
such derived safety and stability requirements at each layer. The feasibility of
the approach has been established using a variation of the ETCS level 3 protocol
enforcing collision freedom of trains following the moving block principle.
Theoretical approaches to cover multi-layered designs, such as refinement and
compositional reasoning, fail to provide semantic bridges across this design space,
in particular due to their inability to support the degree of deviations between
models tolerated by industrial design processes. Horizontal composition theories
provide the semantic foundation for compositional verification, deducing prop-
erties of composed systems in terms of their constituents. Vertical composition
theories exploit the layered structure of designs, allowing to abstract from design
aspects manifest at lower levels when verifying safety properties such as collision
freedom for a “higher” level model.
8
Vertical composition theories typically built
on refinement relations.
Of particular relevance to our application domain are approaches for refine-
ment and compositional verification of hybrid systems. Compositional verifica-
tion techniques for hybrid systems have only recently being investigated, e.g.,
8
We assume that the cooperation layer is “higher” than the local control layer, which
in turn is “higher” than the design layer.
Search WWH ::
Custom Search