Information Technology Reference
In-Depth Information
Module
Input
Output
Module
Voter
Module
Fig. 2.
TMR Arrangement
Before creating our new pattern, we have to decide on its applicability conditions.
First, our input model should have a variable representing the output of the compo-
nent for which TMR will be introduced. Moreover, it should have an event that models
the behaviour of a component by non-deterministically updating this variable. Non-
determinism is used here to model unpredictable (possibly faulty) results produced by
the component. We do not make any assumptions about the variable type. Furthermore,
the event can contain some additional actions on other variables. Finally, our input
model should also contain an event that handles the component failure.
In the refined model, we replace the single abstract component with three similar
components. The outputs of the new components are modelled by fresh variables. The
variable types and initialisation of these variables are simply copied from their abstract
counterpart in the input specification.
The TMR pattern that we define uses a number of configuration parameters, as shown
below. The parameter
s
identifies a variable modelling the output of a component;
u
is
an event updating the variable
s
(in addition to possible update of other variables);
zz
is
an event handling a failure of the component modelled by
u
; finally,
a
is an action from
u
updating the variable
s
.
conf
s, u, zz, a
:
s ∈ var ∧ u ∈ evt ∧ zz ∈ evt ∧ u
=
zz ∧
a ∈ u.actions ∧ a.style
=(:=)
∧{s}
=
a.var
do
conf
ph, s
1
,s
2
,s
3
,r
1
,r
2
,r
3
:
{s
1
,s
2
,s
3
,r
1
,r
2
,r
3
,ph}⊆
(VAR
− var
)
∧
part
(
{{s
1
}, {s
2
}, {s
3
}, {r
1
}, {r
2
}, {r
3
}, {ph}}
)
do
variables
;
events
;
voter
;
abort
;
invariant
end
end
As a result of pattern application, the new variables
ph
,
s
i
and
r
i
are introduced into the
refined model. The variable
ph
keeps track of the current phase in the TMR implemen-
tation, i.e., reading from the new components, voting on them, or delivering the final
result; the variables
s
i
,
i
=1
..
3
, are used to record the outputs produced by the com-
ponents; finally, the flags
r
i
reflect availability of new outputs in the respective output
variables
s
i
.
