Biomedical Engineering Reference
In-Depth Information
finement provides a way to strengthen invariants and to add details to a model. It is
also used to transform an abstract model to a more concrete version by modifying
the state description. This is done by extending the list of state variables (possibly
suppressing some of them), by refining each abstract event to a set of possible con-
crete version, and by adding new events. The abstract (
x
) and concrete (
y
) state
variables are linked by means of a
gluing invariant J(x,y)
. A number of proof
obligations ensures that,
•
each abstract event is correctly refined by its corresponding concrete version;
•
each new event refines
skip
;
•
no new event takes control for ever;
•
relative deadlock freedom is preserved.
Details of the formulation of these proofs follow. We suppose that an abstract
model
AM
with variables
x
and invariant
I(x)
is refined by a concrete model
CM
with variables
y
and gluing invariant
J(x,y)
. Event
e
is in abstract model
AM
and event
f
is in concrete model
CM
. Event
f
refines event
e
.
BA(e)(x, x
)
and
BA(f )(y, y
)
are predicates of events
e
and
f
, respectively. We have to prove the
following statement, corresponding to proof obligation (1):
I(x)
BA(f )(y, y
)
x
·
(BA(e)(x, x
)
J(x
,y
))
∧
J(x,y)
∧
⇒∃
∧
A set of new introduced events in a refinement step can be viewed as hidden
events not visible to the environment of a system and are thus outside the control
of the environment. In Event-B, requiring a new event to refine
skip
means that
the effect of the new event is not observable in the abstract model. Any number of
executions of an internal action may occur in between each execution of a visible
action. Now, proof obligation (2) states that
BA(f )(y, y
)
must refine
skip
(
x
=
x
),
generating the following simple statement to prove (2):
I(x)
∧
BA(f )(y, y
)
J(x,y
)
J(x,y)
∧
⇒
The third kind of proof obligation is related to the progress of its execution,
where a standard technique is to introduce a variant
V(y)
that is decreased by each
new event (to guarantee that an abstract step may occur). This leads to the following
simple statement to prove (3):
I(x)
BA(f )(y, y
)
V(y
)<V(y)
∧
J(x,y)
∧
⇒
The relative deadlock freeness [
16
] is the property to prove that the concrete
model does not introduce additional deadlocks. We give formalisms for reasoning
about the guards of an event in the concrete and abstract models:
grds(AM)
repre-
sents the disjunction of the guards of events of the abstract model, and
grds(CM)
represents the disjunction of the guards of events of the concrete model. Relative
deadlock freeness is now easily formalised as the following proof obligation (4):
I(x)
∧
J(x,y)
∧
grds(AM)
⇒
grds(CM)
In refining a model, an existing event can be refined by strengthening the
guard and/or the before-after predicate (effectively reducing the degree of non-
Search WWH ::
Custom Search