A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems - Formal Methods and Hybrid Real-Time Systems - page 325

3. The generators automatically transform the domain-specific description D

into a behavioural controller model M , a behavioural physical domain model

(describing how uncontrolled physical devices are behaving) and a set of
verification obligations Φ (safety properties as, for example, the requirement
that trains should never meet within a track segment or on a point).
4. It is proved that the controller model

P

M in concurrent combination with

satisfies the obligations Φ .Thisisdonebymeansof
an inductive proof strategy, where the induction step is performed using
bounded model checking techniques.
5. The controller model

the physical model P

is compiled into object code and data with conven-
tional C/C++ compilers. This results in an assembler “model”

M

A .

6. The assembler “model” A is verified to be behaviourally equivalent to the

using the object code verifier.
7. Finally the correctness of the hardware/software integration is automatically
tested, following the concepts described in [2].

controller model M

3 A Case Study

In a case study we have applied our approach to construct and verify a family
of route-based tramway control systems. In particular we designed a domain-
specific language and a SystemC model generator. In later sections we explain
how these were developed. Below, we first informally explain the required behav-
iour of the generated control systems and the contents of domain-specific descrip-
tions, and then we outline the SystemC models that the generator

produces.

3.1 Domain-Specific Description

The basic requirements for avoiding tram collisions are that trams must only
drive on predefined routes previously reserved and that two conflicting (over-
lapping) routes must not be reserved at the same time. As a consequence, con-
trollers built to enforce these requirements depend on the railway network to be
controlled and on a selection of predefined routes through that network. This
implies that the associated domain-specific description should include network
specifications and interlocking tables describing the routes.
Fig. 2 shows a DSL representation of a sample network, consisting of the
following track components:

- sensors : G20.0,. . . ,G25.1
- controllable points : W100, W102, W118
- non controllable points : W120, W121, W122
- signals : S20, S21, S22
- track segments : (G20.0,G20.1), (G20.1,G20.2), ..., shown as solid lines be-
tween two sensors