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

For instance, the predicate checks that the initial state of an IOTS gives initial
values to the variables in its variable set and that the initial location is in its
location set.
We are now going to define a notion of I/O equivalence of IOTS'es. In order to
do that, first we need a to define an operational semantics of IOTS'es involving
states. A state σ foranIOTSisavaluationofitsvariables.

type State = Var m Int

Each transition relation specification of an IOTS denotes a state transformer:

value
eval : TransitionRel → (State → State)

eval(l,g,a,l )( σ )

≡
if eval(g)( σ ) then eval(a)( σ ) else σ end

Here eval ( g )( σ )and eval ( a )( σ ) are the standard extensions of the valuation σ
to guards g and assignments a .
The semantics of an IOTS is the set of its possible runs. A possible run of an
IOTS is a non-empty sequence of pairs of locations and states such that the first
location is its initial location, the first state is its initial state, and that for each
consecutive pairs in the list there is a transition relation in the IOTS from the
location of the first pair to the location of the second pair so that the associated
state transformer maps the state of the first pair to the state of the second pair:

State) ∗

type Run = (Loc ×

value
eval : IOTS

→ Run -set

≡

eval(iots)

{ |

r r:Run •

len r > 0

∧
let (l0, σ 0) = hd r in
l0 = initloc(iots) ∧ σ 0 = initstate(iots)
end ∧

( ∀ i: Int • i > 0 ∧ i < len r ⇒

let
(l i, σ i) = r(i), (l i , σ i )=r(i+1)
in
( (l,g,a,l ) : TransitionRel •

(l,g,a,l )

∃

∈ trans(iots) ∧

l =li ∧
eval(l,g,a,l )( σ i) = σ i )
end

l= li ∧

)

}