Information Technology Reference
In-Depth Information
In the second pass the parser generates constant C array assignments carrying
the configuration data and auxiliary offset information for looking up routes and
track elements.
6
Safety Requirements and Their Verification
Verification Ob jectives.
Our verification strategy is driven by the following
boundary conditions:
-
DSL specifications inherit their formal behavioural semantics from the Sys-
temC models which are automatically generated. As a consequence, no re-
finement proofs are required to ensure consistency between internal SystemC
models and high-level DSL descriptions.
-
No assumptions about the correctness of the generators are made.
-
No assumptions about the correctness of interlocking tables are made.
-
It is assumed that the railway network description (Fig. 2) is complete and
correct.
-
The rules how trains can move in the uncontrolled network (physical model
P
) are complete and correct.
-
The safety conditions
Φ
are complete and correct.
-
Trains stop at signals in HALT state.
Under these assumptions our verification objective is to show that all possible
P
executions, when controlled by the model
M
executed in parallel, respect safety
conditions
Φ
.
Observe further that, since we are not assuming that generators and interlock-
ing tables are correct, an universal “once-and-for-all” verification is impossible:
Each system instance has to be verified with its concrete configuration data. As
a consequence, it is desirable to elaborate a verification strategy which can be
executed in an automated way.
Verification Method.
With respect to full automation the property checking
approach for (
PM
)
sat
Φ
seems attractive. It is well known, however, that
conventional model checking would lead to state explosions for train control tasks
of realistic size. As a consequence, we have adopted a
bounded model checking
strategy combined with inductive reasoning: Instead of elaborating a complete
system model ((
) in our case), bounded model checking starts in an
arbitrary system state
s
which may be additionally restricted by some auxiliary
property
Ψ
,and
unwinds
the model, thereby obtaining all possible transitions
emanating from
s for a bounded number of n>
0
discrete time steps
.The
property
Φ
is checked in each state reachable by means of this unwinding.
For the verification task at hand, auxiliary property
Ψ
mainly states rela-
tionships between sensor events and associated updates of internal counters per-
formed within the controller
PM
M
.Weprovethat
Φ
∧
Ψ
holds in the initial state of
(
Ψ
holds in some state
s
, it will also
hold for the next
n>
0 discrete time steps. As property specification language
PM
). Next it is shown that, provided
Φ
∧
Search WWH ::
Custom Search