Abstract
In the medical domain, there is a tendency to standardize health care by providing medical guidelines as summary of the best evidence concerning a particular topic. Based on the assumption that guidelines are similar to software, we try to carry over techniques from software engineering to guideline development. In this paper, we show how to apply formal methods, namely interactive verification to improve the quality of guidelines. As an example, we have worked on a guideline from the American Academy of Pediatrics for the management of jaundice in newborns. Contributions of this paper are as follows: (I) a formalized model of a nontrivial example guideline, (II) an approach to verify properties of medical guidelines interactively, and (III) verification of a first example property.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Seyfang, A., Kosara, R., Miksch, S.: Asbru 7.3 reference manual. Technical report, Vienna University of Technology (2002)
Seyfang, A., Miksch, S., Marcos, M.: Combining diagnosis and treatment using Asbru. International Journal of Medical Informatics 68(1-3), 49–57 (2002)
Marcos, M., Roomans, H., ten Teije, A., van Harmelen, F.: Improving medical protocols through formalisation: a case study. In: Proc. of the Session on Formal Methods in Healthcare, 6th International Conference on Integrated Design and Process Technology (IDPT 2002) (2002)
Balser, M., Duelli, C., Reif, W.: Formal semantics of Asbru – An Overview. In: Proceedings of IDPT 2002, Society for Design and Process Science (2002)
Bäumler, S., Balser, M., Dunets, A., Reif, W., Schmitt, J.: Verification of medical guidelines by model checking – a case study. In: SPIN conference proceedings (to appear, 2006)
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)
AAP: 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.: Verifying Concurrent System with Symbolic Execution – Temporal Reasoning is Symbolic Execution with a Little Induction. PhD thesis, University of Augsburg, Augsburg, Germany (2005)
Stegers, R.: From natural language to formal proof goal: Structured goal formalisation applied to medical guidelines. Master’s thesis, Vrije Universiteit, Amsterdam (2006)
Balser, M., Duelli, C., Reif, W., Schellhorn, G.: Verifying concurrent systems with symbolic execution. Journal of Logic and Computation 12(4), 549–560 (2002)
Peleg, M., Tu, S., Bury, J., Ciccarese, P., Fox, J., Greenes, R., Hall, R., Johnson, P., Jones, N., Kumar, A., Miksch, S., Quaglini, S., Seyfang, A., Shortliffe, E., Stefanelli, M.: Comparing Computer-interpretable Guideline Models: A Case-study Approach. Journal of the American Medical Informatics Association 10(1), 52–68 (2003)
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)
Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Manna, Z., the STeP group: Step: The stanford temporal prover. Technical report, Computer Science Department, Stanford University (1994)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1990)
Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
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
Schmitt, J., Hoffmann, A., Balser, M., Reif, W., Marcos, M. (2006). Interactive Verification of Medical Guidelines. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_3
Download citation
DOI: https://doi.org/10.1007/11813040_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)