Abstract
This paper presents a case study on how to apply formal modeling and verification in the context of quality improvement in medical healthcare. The aim is to verify quality requirements of medical guidelines and clinical treatment protocols that are used to standardize patient care both for general practitioners and hospitals. This research is supported by the European Commission’s IST program and brings together experts from computer science, artificial intelligence in medicine, hospitals, and the Dutch Institute for Healthcare Improvement (CBO). We present the process of formal modeling and verification of guidelines using the modeling language Asbru, temporal logic for expressing the quality requirements, and model checking for proof and error detection. The approach is illustrated with a case study on a guideline from the American Association for Pediatrics on “Jaundice in healthy Newborns”.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
American Academy of Pediatrics, Provisional Committee for Quality Improvement and Subcommittee on Hyperbilirubinemia. Practice parameter: management of hyperbilirubinemia in the healthy term newborn Pediatrics 94, 558-565 (1994)
Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 363. Springer, Heidelberg (2000)
Balser, M., Duelli, C., Reif, W.: Formal Semantics of Asbru - An Overview. In: Proc. of the 6th World Conference on Integrated Design and Process Technology(IDPT 2002) (June 2002)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium of Programming Language, pp. 238–252 (1977)
Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD Thesis, Eindhoven University of Technology (1996)
Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems 19(2), 253–291 (1997)
Pnueli, A., Josko, B., Hungar, H., Damm, W.: A Compositional Real-time Semantics of STATEMATE Designs. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, p. 186. Springer, Heidelberg (1998)
Duftschmid, G., Miksch, S.: Knowledge-based verification of clinical guidelines by detection of anomalies OEGAI Journal, 37 – 39 (1999)
Allen Emerson, E.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pp. 995–1072. North- Holland Pub. Co., MIT Press (1990)
Field, M.J., Lohr, K.N.: Clinical Practice Guidelines: Directions for a New Program. National Academy Press, Washington D.C. (1992)
Fox, J., Johns, N., Lyons, C., Rahmanzadeh, A., Thomson, R., Wilson, P.: PROforma: a general technology for clinical decision support systems. Computer Methods and Programs in Biomedicine 54, 59–67 (1997)
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based Model Checking using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)
Grumberg, O.: Abstractions and Reductions in Model Checking. Nato Science Series, vol. 62. Marktoberdorf summer school (2001)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Long, D.E.: Model checking, Abstraction, and Compositional Reasoning. PhD Thesis, Carnegie Mellon University (1993)
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, Dordrecht (1993)
Shahar, Y., Miksch, S., Johnson, P.: The Asgaard project: a task-specific framework for the application and critiquing of time-oriented clinical guidelines. Artificial Intelligence in Medicine, 29–51 (1998)
Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)
ten Teije, A., Marcos, M., Balser, M., van Croonenborg, J., Duelli, C., van Harmelem, F., Lucas, P., Miksch, S., Reif, W., Rosenbrand, K., Seyfang, A., Coltel, J., Jovell, A.: Supporting the development of medical protocols through formal methods. In: Proc. of the Symposium on Computerized Guidelines and Protocols (CGP 2004), IOS Press, Amsterdam (2004)
Larsen, K.G., Peterson, P., Yi, W.: UPPAL in a nuttshell. Journal of Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bäumler, S., Balser, M., Dunets, A., Reif, W., Schmitt, J. (2006). Verification of Medical Guidelines by Model Checking – A Case Study. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_13
Download citation
DOI: https://doi.org/10.1007/11691617_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33102-5
Online ISBN: 978-3-540-33103-2
eBook Packages: Computer ScienceComputer Science (R0)