Biomedical Engineering Reference
In-Depth Information
Ta b l e 3 . 2
List of generalised
substitutions
Type
Generalised substitution
Empty
skip
x
:=
E(x,t)
Deterministic
Non-deterministic
x
:∈
E(x,t)
x
:|
P(x,x
)
Second form of an event (
e
), when event (
e
) has not any local variable (
t
), then
an event is represented as follows:
WHEN
G(x)
THEN
x
R(x,x
)
END
:|
Third form of an event (
e
), when event (
e
) has not any guard (
G
) and local
variable (
t
), then an event is represented as follows:
BEGIN
x
:|
R(x,x
)
END
The first form for an event means that it is guarded by a guard that states the
necessary condition for this event to occur. The guard is represented by
∃
t
·
G(t, x)
.
It defines a possibly non-deterministic event where
t
represents a vector of distinct
local variables. It is also semantically equivalent to
∃
t
·
(G(t, x)
∧
R(x,x
,t))
.In
the first, second and third forms,
before-after
predicate
BA(e)(x, x
)
, associated
with each event
e
, describes the event as a logical predicate expressing the relation-
ship linking the values of the state variables just before (
x
) and just after (
x
)the
execution
of event
e
. The third form of the event (
e
) is used for initialisation.
Generalised substitutions (see Table
3.2
) are also borrowed from the B nota-
tion [
2
]. They provide a means to express changes to state variable values. The ac-
tion of an event is composed of mainly three kinds of assignments:
skip
(do nothing),
deterministic assignment and non-deterministic assignment. Where
x
is a variable,
E
is an expression and
P
is a predicate. The value of
x
in each case depends on its
corresponding expression/predicate. For example,
x
:∈
E(x,t)
,
x
will be assigned
as an element of
E(x,t)
. In the case of
x
:|
P(x,x
)
,
x
will be assigned as a value
satisfying the predicate
P
.
x
:|
P(x,x
)
is a more general substitution form of an as-
signment predicate. This should be read as
x is modified in such a way that the value
of x afterwards, denoted by x
,
satisfies the predicate P(x,x
)
, where
x
denotes the
new value
of the vector and
x
denotes its
old value
.
3.5 Proof Obligations
Proof obligations are generated by Rodin tool [
36
]. Different kinds of proof obli-
gations are produced by Rodin tool that are as follows:
WD
(well-definedness),
INV
(Invariant Preservation),
GRD
(Guard Strengthening),
SIM
(Action Simulation),
FIS
(Feasibility), etc. The
WD
proof obligations are generated to ensure that formal pred-
icates and expressions are well defined, which covers generally axioms, invariants,
Search WWH ::
Custom Search