Formal Ontological Analysis for Medical Protocols

Clinical guidelines systematically assist practitioners to provide an appropriate health care in specific clinical circumstances. A significant number of guidelines and protocols is lacking in quality. Indeed, ambiguity and incompleteness are likely anomalies in medical practice. In order to find anomalies and to improve the quality of medical protocols, this paper presents a stepwise formal development of a medical protocol. In this development, we define the domain concepts based on ontologies and integrate them with the medical protocol in an explicit way. In this work, we use the Event B language for modelling a domain model using ontologies and capturing the functional behaviour of the medical protocol. Our main contributions are: to use domain-specific knowledge in a system model explicitly; to link a domain model and a system model using an annotation mechanism; and to use a proof-based formal approach to evaluate a medical protocol. An assessment of the proposed approach is given through a case study, relative to a real-life reference protocol (electrocardiogram (ECG) interpretation), which covers a wide variety of protocol characteristics related to different heart conditions.