Information Technology Reference
In-Depth Information
The above rule
constructs an action from the abstract
action
a
in such a way that it would have the same effect but update the new variable
s
1
.Here
a.style
is one of non-deterministic assignment styles.
The voter event is simply a refined version of the event modelling the abstract
component. Whereas the abstracted version was computing results itself, its refined
counterpart votes on the results of component copies. The voter is enabled once all the
components have produced a result (which is ensured by the first guard in the rule be-
low). The final result is computed according to a simple majority voting protocol. The
event parameter
rr
is set to the voting outcome in the second guard.
voter
s
1
|
a.style
|
a.expression
df
=
newpar
(
u,
”
rr
”);
newgrd
(
u,
”
r
1
=
TRUE ∧ r
2
=
TRUE ∧ r
3
=
TRUE
”);
newgrd
(
u,
”(
s
1
=
s
2
∨ s
1
=
s
3
∧ rr
=
s
1
)
∨
(
s
2
=
s
1
∨ s
2
=
s
3
∧ rr
=
s
2
”);
(
delact
(
u, a
);
newact
(
u, s |
:=
|
”
rr
”
);
(
newact
(
u, r
1
|
:=
|
”
FALSE
”
)
newact
(
u, r
2
|
:=
|
”
FALSE
”
)
newact
(
u, r
3
|
:=
|
”
FALSE
”
));
newact
(
u, ph |
:=
|
”
TRUE
”
)
As a result, the abstract action
a
of the component is replaced by a deterministic assign-
ment (to the same variable
s
) of the result of the winning component. The flags
r
i
and
ph
are reset in preparation for the next iteration.
In case all the component copies disagree, no final result may be computed. This
corresponds to an
abort
event of the abstract specification. The refined model simply
constraints the guard of the event so it only gets enabled in the situations when the
voting has failed.
abort
df
=
newgrd
(
zz,
”
r
1
=
TRUE ∧ r
2
=
TRUE ∧ r
3
=
TRUE
”);
newgrd
(
zz,
”
s
1
=
s
2
∧ s
2
=
s
3
∧ s
1
=
s
3
”);
Finally, a new invariant is added to the refined model to characterise the state of the
refined system after voting is completed. It summarises the cases when the majority
voting on component results succeeds.
invariants
df
=
newinv
(”
ph
=
TRUE ∧
(
s
1
=
s
2
∨ s
2
=
s
3
))
⇒ s
=
s
1
”);
newinv
(”
ph
=
TRUE ∧ s
2
=
s
3
)
⇒ s
=
s
2
”)
Application of the pattern to a fairly simple abstract model (containing only two events
and two variables) saves a user from analysing and discharging 14 proof obligations,
three of which would have to be done manually in an interactive theorem prover. For
larger models or more elaborated patterns, the benefits are even greater.
6
Tool for Refinement Automation
A proof of concept implementation of the pattern tool for the Event B method has been
realised as a plug-in to the RODIN Platform [1]. The plug-in seamlessly integrates with
the RODIN Platform interface so that a user does not have to switch between different
tools and environments while applying patterns in an Event B development. The plug-in
