Information Technology Reference
In-Depth Information
cannot be discharged without considering the context produced by the neighbour rules.
The following inductive definition shows how the list of proof obligations is built for
a particular refinement pattern. The context information for each proof obligation is
accumulated, while traversing the structure of a pattern, as a set of additional hypotheses
that can be then used in automated proofs.
po
(
Γ, basic
)(
c, s
) =
{Γ |
=
proof obligations
(
basic
)
}
po
(
Γ, p
;
q
)(
c, s
) =
po
(
Γ ∪{s
=
eff
(
p
;
q
)(
c, s
)
},p
(
c, s
))
∪
po
(
Γ ∪{s
=
eff
(
p
;
q
)(
c, s
)
},q
(
c, s
))
po
(
Γ, pq
)(
c, s
) =
po
(
Γ, p
)
∪
po
(
Γ, q
)
po
(
Γ,
if
G
(
c, s
)
then
p
end
)(
c, s
) =
po
(
Γ ∪{G
(
c, s
)
},p
)
po
(
Γ,
conf
i
:
Q
(
i, c, s
)
do
p
(
i
)
end
)(
c, s
)=
i ∈ Q
(
i, c, s
)
·
po
(
Γ ∪{Q
(
i, c, s
)
},p
(
i
))
po
(
Γ,
par
i
:
Q
(
i, c, s
)
do
p
(
i
)
end
)(
c, s
)=
po
(
Γ,
conf
i
:
Q
(
i, c, s
)
do
p
(
i
)
end
)(
c, s
)
Here
Γ
is a set of accumulated hypothesis containing pattern parameters
c
and the initial
model
s
as free variables. For each basic rule, we formulate a theorem whose right-hand
side is a list of the rule proof obligations and the left-hand side is a set of hypotheses
containing the knowledge about the context in which the rule is applied.
4.4
Assertions
The described procedure for building a list of proof obligations tries to include every
possible fact as a proof obligation hypothesis. This can be a problem for larger patterns
as the size of a list of accumulated hypotheses makes a proof obligation intractable.
To rectify the problem, we allow a modeller to manually add fitting hypotheses, called
assertions, that can be inferred from the context they appear in. An assertion would
be typically simple enough to be discharged automatically by a theorem prover. At the
same time, it can be used to assist in demonstrating the proof obligations of the rule
immediately following the assertion.
An assertion is written as
assert
(
A
(
c, s
))
and is delimited from the neighboring rules
by semicolons. An assertion has no effect on rule instantiation and application. The
following additional cases of the
po
definition are used to generate additional proof
obligations for assertions as well as insert an asserted knowledge into the set of collected
hypotheses of a refinement pattern.
po
(
Γ, p
;
assert
(
A
(
c, s
)))(
c, s
)=
Γ ∪{s
=
eff
(
p
)(
c, s
)
}|
=
A
(
c, s
)
po
(
Γ,
assert
(
A
(
c, s
));
p
)(
c, s
)=
po
(
Γ ∪{A
(
c, s
)
},p
)(
c, s
)
5
Triple Modular Redundancy Pattern
Triple Modular Redundancy (TMR) [15] is a fault-tolerance mechanism in which the
results of executing three identical components are processed by a voting element to
produce a single output that takes the majority view. This mechanism is schematically
shown in Figure 2.
The purpose of the mechanism is to mask a single component failure. In this section
we will demonstrate how to generalize a refinement step introducing the TMR arrange-
ment into a model as a refinement pattern.
