Biomedical Engineering Reference
In-Depth Information
determinism), or a new event can be added to refine the skip event. The feasi-
bility condition is crucial to avoiding possible states that have no successor, such
as division by zero. Furthermore, this refinement guarantees that the set of traces
of the refined model contains (up to stuttering) the traces of the resulting model.
The refinement of an event
e
by an event
f
means that the event
f
simulates the
event
e
.
The Event-B modelling language is supported by the Rodin platform [
36
] and
has been introduced in publications [
2
,
4
,
17
], where there are many case studies and
discussions about the language itself and the foundations of the Event-B approach.
The language of
generalised substitutions
is very rich, enabling the expression of
any relation between states in a set-theoretical context. The expressive power of the
language leads to a requirement for help in writing relational specifications, which is
why we should provide guidelines for assisting the development of Event-B models.
3.7 Decomposition
A large system needs several refinement steps to model the whole system from an
abstract to the concrete level. Increasing refinement steps introduces many state
variables to specify the desired behaviour of a system. Increasing number of state
variables makes the system too complex that becomes impossible to manage. De-
composition is a process that can split the whole system into several independent
subsystems. The decomposition process reduces the overall complexity of the sys-
tem that helps to apply the refinement technique on each subsystem. All the inde-
pendent subsystems are put together to form a single model that can guaranteed to
be a refinement of the original one [
4
].
For developing a large complex model, it is necessary to decompose a model
M
into sub-models. Suppose the model
M
can be decomposed into two sub-models
P
and
Q
. The decomposition process divides a set of events and variables of the
model
. However, there are
always some variables those are shared by both sub-models. The shared variables
are known as
external variables
, and to handle these shared variables we need to
introduce some
external events
.
Figure
3.2
presents the decomposition process of the model
M
into two groups related to the sub-models
P
and
Q
M
into the sub-
models
. A variable
v
2
is an
external variable
and
ex
3
and
ex
2
are
external
events
of the sub-models
P
and
Q
, respectively. Other variables
v
1
and
v
3
are the
internal variables
, and
e
1
,
e
2
,
e
3
and
e
4
are internal events of the sub-models
P
and
Q
P
and
.
Each subsystem can be refined independently after successful decomposition of
the system. Such as, subsystems
Q
P
and
Q
can be refined into
PR
and
QR
(see
Fig.
3.2
). The refined model
contains the
internal variables u
1
and
external
variables u
2
. Similarly, the refined model
PR
contains
internal variables u
2
and
external variables u
3
. The shared external variables
v
2
are common in both decom-
posed models that must be refined in a same way. The desired properties must be
QR
Search WWH ::
Custom Search