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

2. A parser that takes a domain-specific description as input and returns con-
crete configuration data and instantiation parameters for the generic algo-
rithms.
We have selected SystemC [19] as the target language for the generators,
since it is associated with a formal transition system semantics and can be di-
rectly compiled into executable code [29,3]. As a consequence, the original DSL
descriptions “inherit” formal behavioural semantics from the transformations
performed by the generators.

Generic Configurable Library. Since the SystemC code is automatically
generated, the emphasis of the coding structure - whose layout is already fixed
in the configurable library - lies on easy verifiability and ecient executability:
Configuration data is encoded in global arrays of integers, and the control struc-
tures of the algorithms are in one-one-correspondence with the safety properties
Φ , while controlling signal and point states: For example, if allocation of route
r i excludes simultaneous allocation of routes r and requires point states p j ( r )
and signal states s k ( r ), then the allocation is guarded by code structures like
bool mayAllocate = true;
for (int l = 0; l < m1; l++)
mayAllocate = mayAllocate and not allocated(r[i][l]);
for (int j = 0; j < m2; j++)
mayAllocate = mayAllocate and p[i][j];
for (int k = 0; k < m3; k++)
mayAllocate = mayAllocate and s[i][k];
if ( mayAllocate )
allocate(i);
This also ensures a close relationship between SystemC and assembler code
which facilitates the object code verification in a considerable way.
The generic parameters referenced in the control algorithms of the library are
of a very simple nature: They comprise number parameters, specifying the con-
crete quantities of sensors, signals, points and routes to be fixed for each system
and offset parameters used for looking up specific routes and track elements in
the static configuration data or in the dynamic control states.
The most important aspect of the static configuration data is the description
of available track elements and route specifications. Routes are represented as
sequences of index references to track elements, together with information about
the required signal and point states to be enforced when allocating a route to
a tram. An additional integer array is used for specifying the conflict relations
between routes.

DSL SystemC Parser. The parser for producing concrete SystemC code

from DSL descriptions proceeds in two passes: First, the number parameters
are determined from the DSL and represented as C constant declarations. As a
result the dimensions of all arrays used for storing static configuration data and
dynamic state information are fixed.

→