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

4 From Static Domain Model to Domain-Specific

Language

In this section we explain how a domain-specific description language for our
case study can be formally developed from a static domain model using RSL.
At the end of this development process, the RSL model obtained represents the
abstract syntax and static semantics of the DSL under construction. It then
only remains to associate the abstract syntactic elements with concrete syntax,
in order to complete the DSL definition: The behavioural semantics is defined in
a transformational way by means of the generator translating DSL specifications
into SystemC.

4.1 RSL Static Domain Model

We start by describing how a domain model can be established. The domain
model covers the concepts of railway networks and routes. More general models
would typically cover further aspects like time tables, but here we only present
those concepts that are relevant for the development of the application consid-
ered in this paper. The model of each concept is generic (algebraic) in the sense
that it defines which properties any concrete instance of the concept should have.
The generic model can be instantiated to produce a concrete one defining what
the specific properties are for that specific instance.

Generic Network Model. Any concrete network model should describe the
topology of a railway network consisting of the physical components: segments,
sensors, signals and points.
In the generic model, for each kind of component, an abstract type of identi-
fiers for its components is declared:

type Sensor, Point, Signal, Segment

Furthermore, signatures for functions that describe the relationship between the
components are given. For instance, the following function gives the sensor at
which a given signal is placed:

value sensor of : Signal → Sensor

Finally, a number of axioms express requirements to these functions, i.e. impose
restrictions on which network topologies are allowed. For instance, the following
axiom requires that any two distinct signals are placed at distinct sensors:

∀ s1, s2 : Signal • s1 =s2 ⇒ sensor of(s1) =sensorof(s2)

To describe a concrete network , the elements of the types should be specified
and the functions should be explicitly defined in such a way that the axioms are
satisfied.