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

given by an initial state, (2) a set of locations one of which is designated as
the initial location l 0 , and, (3) a set of transition rules. Variables are classified
into input, output and processing variables. A transition rule from one location
l 1 to another location l 2 is specified by a guard that is a quantifier-free predi-
cate over the variables and by a multiple assignment ( v 1 ,...,v n ):=( e 1 ,...,e n ),
where v 1 ,...,v n are variables and e 1 ,...,e n are expressions over the given set
of variables. However, as a new thing, for an IOTS we also divide the locations
into pairwise disjoint sets of input, output and processing locations, and we put
further constraints on the allowed use of variables in guards and expressions in
an IOTS: guards must only use processing variables, for transitions into input
locations the assignments must only read input variables and make assignment
to processing variables, for transitions into processing locations the assignments
must only read processing variables and make assignment to processing vari-
ables, and, for transitions into output locations the assignments must only read
processing variables and make assignment to output variables.
One can obviously specify an abstract syntax of IOTS'es in RSL :

type
IOTS ::
vars : Var -set
initstate : State
locs : Loc -set
initloc : Loc
trans : TransitionRel -set ,
TransitionRel = Loc × Guard × Assign × Loc,

Expr) ∗ , Assign :: al : (Var ×

Expr ==
mk Const(i : Int )

| mk Var(v : Var) | mk Sum(e1 : Expr, e2 : Expr) | ... ,

Guard == TRUE | ... ,

where Guard and Expr are the abstract syntaxes of guards and expressions,
respectively, for space reasons not completely specified here.
For variables and locations two abstract types are used, each having an ob-
server function mode that informs about the mode (input, output or processing)
of variables and locations, respectively:

type Var, Lo c
value mode : Var

→ Mode, mode : Loc → Mode,

type Mode == IN | OUT | PROC

We also introduce a well-formedness predicate for IOTS'es formalising all the
conditions on the use of variables and locations stated informally above:

value
is wff : IOTS → Bool

is wff(iots) ≡

dom initstate(iots) = vars(iots) ∧ initloc(iots) ∈ locs(iots) ∧ ...