Biomedical Engineering Reference
In-Depth Information
10.6.3 Incompleteness
Either missing pieces of information or insufficient information in the original doc-
ument are always related to the incompleteness anomaly. In either case, incomplete-
ness hinders a correct interpretation of the guidelines and protocols. For example,
the original protocol contains “normal variant” factors to be considered when as-
sessing the T-wave. However, what “normal variant” exactly means is missing in
the protocol. As an example of insufficient information for “normal variant”, we
provide the class of diseases for further analysis the system.
10.7 Summary
Refinement is a key concept for developing the complex systems, since it starts with
a very abstract model and incrementally adds new details to the set of requirements.
We have outlined an incremental refinement-based approach for formalising med-
ical protocols using the Rodin tool. The approach we have taken is not specific to
the Event-B. We believe a similar approach could be taken using others state-based
notations such as ASM, TLA
+
, Z, etc. The Rodin proof tool is used to generate
the hundreds of proof obligations and to discharge those obligations automatically
and interactively. Another key role of the tool is in helping us to discover appro-
priate gluing invariants to prove the refinements. In summary, some key lessons are
that incremental development with small refinement steps; appropriate abstractions
at each level and powerful tool support are all invaluable in such a kind of formal
development.
In this chapter, we have shown the formal representation of medical protocol.
The formal model of medical protocol is verified, and this verified model is not only
feasible but also useful for improving the existing medical protocol. We have fully
formalised a real-world medical protocols (ECG interpretation) in an incremental
refinement-based formalisation process, and we have used proof tools to systemat-
ically analyse whether the formalisation complies with certain medically relevant
protocol properties [
21
,
22
]. The formal verification process has discovered a num-
ber of anomalies which all are discussed in the previous section. Throughout this
process, we have obtained the following concrete results:
•
A formal specification language like Event-B is used for modelling a complex
system, is used to model the medical practice protocols. The Event-B is a general
modelling language tool. The Event-B is used to present a formal specification
for a real-life medical protocols; ECG interpretation.
•
The ECG interpretation protocol is formalised in the Event-B modelling lan-
guage. The medical protocol ECG interpretation is used in our study has been
developed in incremental way and finally transformed into a concrete formal rep-
resentation. Each proved refinement level of the formal model of the protocol
represents feasibility and correctness.
Search WWH ::
Custom Search