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