Information Technology Reference
In-Depth Information
The pattern consists of four major parts: the rules declaring the types and initialisa-
tion of new variables of the refined model; the definition of new events; the refinement
rules for transforming a single abstract event representing the functionality of a sole
component into the voter event; and, finally, the addition of an invariant characterising
the behaviour of a TMR block. The condition using the operator
part
simply states that
its arguments are disjoint sets.
variables
df
=
(
newinv
(”
ph ∈ BOOL
”);
newini
(
ph |
:=
|
”
FALSE
”
))
(
newinv
(”
s
1
∈ s.type
”);
newini
(
s
1
| init
(
s
)
.style | init
(
s
)
.expr
))
(
newinv
(”
r
1
∈ BOOL
”);
newini
(
r
1
|
:=
|
”
FALSE
”
))
...
Each new variable definition should come with a typing invariant and an initialisation
action. These are normally grouped together so that the related proof obligation rules
would work with a smaller context. For the sake of brevity, we omit showing here the
rules defining the types and initialisation for the variables
s
2
,s
3
and
r
2
,r
3
(the omitted
part is indicated by
...
). The shortcut notation
newini
(
a
)
used in the pattern descrip-
tion stands for declaration of the initialisation action:
newini
(
a
)
df
=
newact
(
init
,a
)
.
The shortcut
init
(
v
)
refers to an action of the initialisation event assigning to the
variable
v
.
The refined model specifies the behavior of three components of TMR (we call them
replicated components) as copies of the behaviour of the component specified in the
input model. Since we assumed that a component is represented by a single event, the
replicated components are created by adding three new events into the refined model in
the following way.
The guard of the event modelling behaviour of a replicated component essentially
coincides with the guard of an abstract component. However, it also contains an ex-
tra conjunct ensuring that the event is executed before passing control to the voter.
The event actions essentially copy the corresponding actions of the abstract component
(given as the pattern parameter
a
). The only difference is that each replicated event
records the result into a separate variable
s
i
(for the copy
i
) instead of the abstract vari-
able
s
. In addition, a component copy also assigns to
r
i
to indicate the availability of
result in
s
i
.
events
df
=
conf
u
1
,u
2
,u
3
:
{u
1
,u
2
,u
3
}⊂
EVENT
\ s.evt ∧ part
(
{{u
1
}, {u
2
}, {u
3
}}
)
do
copy
1
copy
2
copy
3
end
The above creates three component copies, each constructed according to the following
rule.
copy
1
df
=
newevt
(
u
1
|−|{
”
r
1
=
FALSE
”
}∪u.guards |
s
1
| a.style | a.expression, r
1
|
:=
|
”
TRUE
”
, ph |
:=
|
”
FALSE
”
...
