Biomedical Engineering Reference
In-Depth Information
Ta b l e 3 . 1
Set-theoretical notation
Name
Syntax
Definition
s
↔
t
(
P
)(s
×
t)
Binary relation
Composition of relations
r
1
;
r
2
{
x,y
|
x
∈
a
∧
y
∈
b
∧∃
z.(z
∈
c
∧
x,z
∈
r
1
∧
z, y
∈
r
2
)
}
r
−
1
Inverse relation
{
x,y
|
x
∈
P
(a)
∧
y
∈
D
(b)
∧
a
→
b
∈
r
}
Domain
dom(r)
{
a
|
a
∈
s
∧∃
b.(b
∈
t
∧
a
→
b
∈
r)
}
dom(r
−
1
)
Range
ran(r)
Identity
id(s)
{
x,y
|
x
∈
s
∧
y
∈
s
∧
x
=
y
}
Restriction
s
r
id(s)
;
r
Co-restriction
r
s
r
;
id(s)
Anti-restriction
s
r
(dom(r)
−
s)
r
Anti-co-restriction
r
−
s
r
(ran(r)
−
s)
Image
r
[
w
]
ran(w
r)
Overriding
q
−
r dom(r)
q)
∪
r
(r
−
1
Partial function
s
→
t
{
r
|
r
∈
s
↔
t
∧
;
r)
⊆
id(t)
}
by the refinement mechanism which provides a mechanism for relating an abstract
model and a concrete model by adding new events or by adding new variables. This
mechanism allows us to develop gradually Event-B models and to validate each de-
cision step using the proof tools. The refinement relationship should be expressed
as follows: a model
M
is refined by a model
P
, when
P
is simulating
M
. The final
concrete model is close to the behaviour of the real system that is executing events
using real source code. We give details now on the definition of events, refinement
and guidelines for developing the complex system models.
3.4 Modelling Actions over States
The event-driven approach [
4
,
17
] is based on the Classical B notation [
2
]. It ex-
tends the methodological scope of basic concepts to take into account the idea of
formal reactive models
. Briefly, a formal reactive model is characterised by a (fi-
nite) list
x
of
state variables
possibly modified by a (finite) list of
events
, where an
invariant
I(x)
states properties that must always be satisfied by the variables
x
and
maintained
by the activation of the events. Table
3.1
presents some set-theoretical
notations of Event-B [
4
] and Classical B [
2
], which are used to formalise a system.
We summarise the definitions and principles of formal models and explain how they
can be managed by tools [
36
].
Each event is composed of a guard
G(t, x)
and an action
R(t,x)
, where
t
are lo-
cal variables the event may contain. The guard states the necessary condition under
which an event may occur, and the action describes how the state variables evolve
when the event occurs. The first general form for an event is as follows:
ANY
t
WHERE
G(x, t)
THEN
x
:|
R(x,x
,t)
END
Search WWH ::
Custom Search