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

Generic Route Model. An abstract type of identifiers for routes is declared:
type Route

We state the signature for a function that for a given route returns a list of those
sensors which have to be passed in the stated order when travelling along the
route:
value sensors of : Route → Sensor ∗

A number of axioms express requirements to this function, i.e. impose restrictions
on what is an allowed route. For instance, there must be a signal at the first
sensor of any route:
∀ r:Route • ∃ s : Signal • sensor of(s) = hd sensors of(r)

4.2 Domain-Specific Language
RSL Specification. The domain model is now extended with value declarations
for each element to be part of a domain description. For each kind of physical
component there is an element (all together providing a network description):
value
sensors : Id -set ,
points : Id m ... ,

signals : Id m Sensor,

segments : Id

m ...
and for each kind of interlocking table there is an element 2 :
value
rdt : Id

m Sensor ∗ ,
rct : Route

→ Route -set × Route -set ,

ppt : Route → Point m PointPosition,

sst : Route → Signal × SignalSetting

We chose identifiers to be texts:
type Id = Text

The declarations give each element a name and a model-oriented type and hence
provide an abstract syntax for the elements. As an example, the abstract syntax
for the signals element is Id

m Sensor , and the intension is that a signals
element should map any signal identifier to the identifier of that sensor at which
it is placed.
Now, the Signal type can be explicitly defined as containing the identifiers of
the domain of the signals element:
type Signal = {| id : Id • id ∈ dom signals |}

The Sensor , Point , Segment and Route types can be defined in a similar way.
2

rdt for route definition table, rct for route conflict table, ppt for point position table,
and sst for signal setting table.