Biomedical Engineering Reference
In-Depth Information
9.1.1 Why Model-Checker?
Model checking [
3
] and theorem proving are both applicable in medical device de-
velopment. This approach requires a model of the system under consideration to-
gether with a desired property and systematically checks whether the given model
satisfies this property. The basic technique of model checking is a systematic, usu-
ally exhaustive, state-space search to check whether the property is satisfied in each
state of the model, thereby using effective methods to combat the infamous state-
space explosion problem. Using model checking with formal verification for medi-
cal device has several benefits:
•
To understand the formal verification of any system is not an easy task. A group
of non-formal people (doctors, engineering, coder and so on) cannot understand
it due to lack of knowledge of formal mathematics. Non-formal people can un-
derstand the desirable system behaviour through model checker and can give the
proper feedback.
•
A model-checker is also useful for a model designer to improve the system.
A model-checker may provide a counter-example showing under which circum-
stance the error can be generated. The counter-example provides evidence that
the system is faulty and needs to be revised. This allows the user to locate the
error and to repair the system before continuing. If no error is found, the user can
refine the model description and can restart the verification process.
9.1.2 Related Work for the Cardiac Pacemaker
Macedo et al. [
38
] have developed a distributed real-time model of a cardiac pace-
maker using a formal tool VDM [
6
], where they have modelled the subset of pace-
maker functionalities. In another pacemaker case study, Manna et al. [
34
]have
shown a simple pacemaker implementation. Gomes et al. [
19
] have presented a for-
mal specification of a cardiac pacemaker using Z modelling language, and they have
modelled the sequential model similar to Macedo et al. work [
38
]. A detailed formal-
isation of the one- and two electrode pacemaker is represented in [
40
,
43
,
48
]. The
model has been developed in an incremental way using refinements in the Event-B
modelling language. Tuan et al. [
58
] have proposed a formal model of the pacemaker
based on its behaviour including the communication with the external environment.
They have designed a real-time model of the pacemaker using timed extensions of
CSP and used the model checker Process Analysis Toolkit (PAT) in order to ver-
ify the critical properties, such as deadlock freeness and heart rate limits. Recently,
Gomes et al. [
20
] have presented the pacemaker case study by providing a means to
execute the model using a translation of Z model into Perfect Developer [
12
]. They
have used the existing tool Perfect Developer [
12
] to generate an executable code
of Z model. In [
30
], authors have used dual chamber implantable pacemaker as a
case study for modelling and verification of control algorithms for medical devices
in UPPAAL.
Search WWH ::
Custom Search