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

initloc(iots2) = initloc(iots1) ∧

trans(iots2) =
trans(iots1)

\

{ }

(l0, g, mk Assign( (x, mk Sum(mk Var(x), mk Const(1))) ), l3)

∪
{

(l0, g, mk Assign( (y, mk Var(x)) ), l1),

(l1, TRUE, mk Assign( (y, mk Sum(mk Var(y), mk Const(1))) ), l2),

(l2, TRUE, mk Assign( (x, mk Var(y)) ), l3)

}∧
assigned before read(iots1, l3, y)

⇒

equiv(iots1, iots2)

l0 l0

<=>

x[i] := y[i] aux1 := i

l4 l1

aux2 := i

l2

aux2 := y[aux2]

l3

x[aux1] := aux2

l4

Fig. 6. Another transformation rule

Another example of a transformation rule is one stating that an IOTS iots 1
can be transformed into an equivalent IOTS iots 2 by replacing the transition
shown on the left hand side of Fig. 6 with the four transitions shown on the
right hand side of Fig. 6, or vice versa, provided that (1) l 1, l 2and l 3are
not locations of iots 1, aux 1and aux 2 are local variables, and (2) in any path
emanating from location l 4, the variables aux 1and aux 2 are assigned before
read. The rule is generic in locations l 0, l 1, l 2, l 3and l 4, and variables aux 1,
aux 2, x and y .

7.5 IOTS Semantics of the Source and Target Languages

In [30] it is explained how to derive the IOTS semantics for generated SystemC
models and assembler code. This can be formalised in RSL by defining abstract