Biomedical Engineering Reference
In-Depth Information
Fig. 6.2
Basic rules of
refinement chart
M
1
(M
2
M
3
...
M
n
−
1
M
n
)
M
1
(M
2
M
3
···
M
n
−
1
M
n
)
(M
1
M
2
,M
2
M
3
,...,M
n
−
1
M
n
)
other refinement according to the operating modes. The nesting relationship among
several refinement boxes states that the system operates in any subsystems. For ex-
ample, Fig.
6.1
(C) represents an abstract mode
M
1 and the subsystems refinement
by a nesting box
M
2 and the subsystem
M
2 is refined by a nesting box
M
3 in three
levels of hierarchy, where
M
2 is embedded in
M
1 and
M
3 is embedded in
M
2.
A transition is allowed to next level of refined subsystem. A transition out of one
refinement requires an exit out of all the refined sub level of refined subsystems.
As an example, Fig.
6.3
presents the diagrams of the most abstract modal system
for the one electrode pacemaker system (A) and the resulting models of three suc-
cessive refinement steps (B to D). The diagrams use a visual notation to represent
the bradycardia operating modes of the pacemaker under the functional and para-
metric requirements. An operating mode is represented by a box with a mode name;
an operating mode transition is an arrow connecting two operating modes. The di-
rection of an arrow indicates the previous and next operating modes in a transition.
Refinement is expressed by nesting boxes. A detailed description about these refine-
ment blocks related to the one-electrode cardiac pacemaker is given in case study
(see Chap.
9
).
Refinement based representation is used during the decomposition and synthesis
phases of a system. The purpose of the refinement chart is to provide an easily man-
ageable representation for different refinements of a system. The refinement chart
offers a clear view of assistance in system integration. This is an important issue not
only for being able to derive system-level performance and correctness guarantees,
but also for being able to assemble components in a cost-effective manner.
Refinement is a modelling technique that is used to introduce more concrete be-
haviour of a system in the next level of refinement, where it preserves the safety
properties and system behaviour between two refinement levels. This preservation
property allows us to model the whole system from initial specification to a con-
crete level in a form of executable specification using incremental development.
The concrete model is considered as that it preserves a system behaviour, thereby
establishing that the generated code satisfies the initial specification [
15
]. Proof of
consistency between source and target of a refinement is an intrinsic capability of a
refinement process, which can be composed in a similar fashion [
14
].
A refinement-based system development has a different cost structure than the
traditional development life-cycle. The cost of building models and related other
required design knowledge may be higher for producing the first system. How-
ever, these costs are amortised when reuse these models and designs for developing
the other future systems. Thus, the cost of producing first program may be higher,
but the cost of development for reproducing advanced version of the products and
reuse same codes in other products should be less than the conventional program-
ming [
14
,
15
]. The cost of handling of proof obligations of specifications and refine-
ments should be less than the cost of analysing the final product. It can also help to
Search WWH ::
Custom Search