Biomedical Engineering Reference
In-Depth Information
Jonathan et al. [
31
] have proposed a way to apply formal methods, namely inter-
active verification to improve the quality of medical protocols or guidelines. They
have applied this technique for the management of jaundice in newborns based on
guidelines of American Academy of Pediatrics. This paper includes formalisation
of the jaundice protocol and verifies some interesting properties. Simon et al. [
5
]
have used the same protocol for improvement purpose using a modelling language
Asbru, temporal logic for expressing the quality requirements, and model checking
for proof and error detection.
Applying a formal approach for improving medical protocol is one major area
of research, which helps to the medical practitioners for improve the quality of pa-
tient care. A project Protocure [
37
] is a European project, which is carried out by
five different institutions. The main objective of this project is for improving med-
ical protocol through integration of formal methods. The main motivation of this
project is to identify anomalies like ambiguity and incompleteness in the medical
guidelines and protocols. Presently, all medical protocols and guidelines are in text,
flow diagrams and tables formats, which are easily understandable by the medical
practitioners. But these are incomplete and ambiguous due to lack of formal seman-
tics. The idea of using formal methods is to uncover these ambiguous, incomplete
or even inconsistent parts of the protocols, by defining all the different descrip-
tions more precisely using a formal language and to enable verification. Mainly, the
researchers have used Asbru [
36
] language for protocol description and KIV for
interactive verification system [
3
].
Asbru [
36
] is a main modelling language for describing medical protocol and
formal proof of the medical protocol is possible through KIV interactive theorem
prover [
3
]. Guideline Markup Tool (GMT) [
17
] is an editor who helps to translate
guidelines into Asbru. An additional functionality of the tool is to define relations
between the original protocol and its Asbru translation with a link macro [
17
]. As-
bru language is used for protocol description and Asbru formalisations are translated
into KIV. Asbru is considered as a semi-formal language to support the tasks nec-
essary for protocol-based care. It is called a semi-formal language because of its
semantics, although more precise than in other protocol representation languages,
are not defined in a formal way. This semi-formal quality makes Asbru suitable for
an initial analysis but not for systematic verification of protocols [
23
].
According to our literatures survey, existing medical protocol tools are based
on semi-formal techniques. Existing techniques [
6
,
25
,
36
] based on formal tech-
niques are failed to scale the complexity of the protocol. They have not given any
proper idea to model the medical protocols only using formal techniques due to
complex nature of the medical protocol. To tackle the complexity of the protocol
in formal methods is only a solution to use the refinement approach to model the
whole protocol from abstract level to a final concrete model. In this chapter, we
have provided sufficient detailed information about modelling a complex protocol
using any formal method technique. In this study, we have tried to model a medical
protocol, completely based on formal semantics and to check various anomalies.
To overcome from the existing problems [
23
,
32
] in the area of development of
medical protocols, we have used the general formal modelling tool like Event-B [
1
]
Search WWH ::
Custom Search