Skip to main content
SpringerLink
Log in

Medical Protocol Diagnosis Using Formal Methods

  • Conference paper
Foundations of Health Informatics Engineering and Systems (FHIES 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7151))

Abstract

Clinical guidelines systematically assist practitioners to provide appropriate health care in specific clinical circumstances. Today, a significant number of guidelines and protocols are lacking in quality. Indeed, ambiguity and incompleteness are likely anomalies in medical practice. Our objective is to find anomalies and to improve the quality of medical protocols using well-known mathematical formal techniques, such as Event B. In this paper, we use the Event B modelling language to capture guidelines for their validation. Our main contributions are: to apply mathematical formal techniques to evaluate real-life medical protocols for quality improvement; to derive verification proofs for the protocol and properties according to medical experts; and to publicize the potential of this approach. An assessment of the proposed approach is given through a case study, relative to a real-life reference protocol (ECG interpretation), which covers a wide variety of protocol characteristics related to several heart diseases. We formalize the reference protocol, verify a set of interesting properties of the protocol and finally determine anomalies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Lohr, K.N., Field, M.J.: Clinical practice guidelines: directions for a new program. In: Committee to Advise the Public Health Service on Clinical Practice Guidelines, United States and Institute of Medicine. National Academy Press, Washington, D.C. (1990)

    Google Scholar 

  2. Ten Teije, A., Marcos, M., Balser, M., van Croonenborg, J., Duelli, C., van Harmelen, F., Lucas, P., Miksch, S., Reif, W., Rosenbrand, K., Seyfang, A.: Improving medical protocols by formal methods. Artif. Intell. Med. 36(3), 193–209 (2006)

    Article  Google Scholar 

  3. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)

    Google Scholar 

  4. Project RODIN: Rigorous open development environment for complex systems (2004), http://rodin-b-sharp.sourceforge.net/

  5. Méry, D., Singh, N.K.: Technical Report on Interpretation of the Electrocardiogram (ECG) Signal using Formal Methods. Technical report, LORIA UMR 7503 (2011), http://hal.inria.fr/inria-00584177/en/

  6. 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)

    Google Scholar 

  7. Samson, M.M., Musen, M.A., Tu, S.W., Das, A.K., Shahar, Y.: Eon: A component-based approach to automation of protocol-directed therapy (1996)

    Google Scholar 

  8. Fox, J., Johns, N., Rahmanzadeh, A.: Disseminating medical knowledge: the proforma approach. Artificial Intelligence in Medicine 14(1-2), 157–182 (1998)

    Article  Google Scholar 

  9. Peleg, M., Tu, S., Bury, J., Ciccarese, P., Fox, J., Greenes, R.A., Miksch, S., Quaglini, S., Seyfang, A., Shortliffe, E.H., Stefanelli, M., et al.: Comparing computer-interpretable guideline models: A case-study approach. JAMIA 10 (2003)

    Google Scholar 

  10. Wang, D., Peleg, M., Tu, S.W., Boxwala, A.A., Greenes, R.A., Patel, V.L., Shortliffe, E.H.: Representation primitives, process models and patient data in computer-interpretable clinical practice guidelines: A literature review of guideline representation models. International Journal of Medical Informatics 68(1-3), 59–70 (2002)

    Article  Google Scholar 

  11. Isern, D., Moreno, A.: Computer-based execution of clinical guidelines: A review. International Journal of Medical Informatics 77(12), 787–808 (2008)

    Article  Google Scholar 

  12. Miller, P.L.: A critiquing approach to expert computer advice: Attending. Pitman Publishing, Inc., Marshfield (1985)

    Google Scholar 

  13. Marcos, M., Berger, G., van Harmelen, F., ten Teije, A., Roomans, H., Miksch, S.: Using Critiquing for Improving Medical Protocols: Harder than It Seems. In: Quaglini, S., Barahona, P., Andreassen, S. (eds.) AIME 2001. LNCS (LNAI), vol. 2101, pp. 431–441. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Shiffman, R.N., Greenes, R.A.: Improving Clinical Guidelines with Logic and Decision-table Techniques: Application to Hepatitis Immunization Recommendations. Med. Decis. Making 14(3), 245–254 (1994)

    Article  Google Scholar 

  15. Shiffman, R.N.: Representation of Clinical Practice Guidelines in Conventional and Augmented Decision Tables. Journal of AMIA 4(5), 382–393 (1997)

    Google Scholar 

  16. Miller, D.W., Frawley, S.J., Miller, P.L.: Using semantic constraints to help verify the completeness of a computer-based clinical guideline for childhood immunization. Computer Methods and Programs in Biomedicine 58(3), 267–280 (1999)

    Article  Google Scholar 

  17. Bottrighi, A., Giordano, L., Molino, G., Montani, S., Terenziani, P., Torchio, M.: Adopting model checking techniques for clinical guidelines verification. Artif. Intell. Med. 48, 1–19 (2010)

    Article  Google Scholar 

  18. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 279–295 (1997)

    Article  Google Scholar 

  19. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)

    Google Scholar 

  20. Prez, B., Porres, I.: Authoring and verification of clinical guidelines: A model driven approach. Journal of Biomedical Informatics 43(4), 520–536 (2010)

    Article  Google Scholar 

  21. Rumbaugh, J., Jacobson, I., Booch, G. (eds.): The Unified Modeling Language reference manual. Addison-Wesley Longman Ltd., Essex (1999)

    Google Scholar 

  22. Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA, 2nd edn. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)

    Google Scholar 

  23. Schmitt, J., Hoffmann, A., Balser, M., Reif, W., Marcos, M.: Interactive Verification of Medical Guidelines. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol. 4085, pp. 32–47. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Bäumler, S., Balser, M., Dunets, A., Reif, W., Schmitt, J.: Verification of Medical Guidelines by Model Checking – A Case Study. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 219–233. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  25. Balser, M., Coltell, O., Croonenborg, J.V., Duelli, C., Harmelen, F.V., Jovell, A., Lucas, P., Marcos, M., Miksch, S., Reif, W., Rosenbr, K., Seyfang, A., Teije, A.T.: Protocure: Supporting the development of medical protocols through formal methods. In: SCPG 2004. Studies in Health Technology and Informatics, vol. 101, pp. 103–108. IOS Press (2004)

    Google Scholar 

  26. Balser, M., Reif, W., Schellhorn, G., Stenzel, K.: Kiv 3.0 for Provably Correct Systems. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 330–337. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  27. Balzer, M., Duelli, C., Reif, W.: Formal Semantics of Asbru-An Overview. In: Integrated Design and Process Technology IPDT (2002)

    Google Scholar 

  28. Kosara, R., Miksch, S., Andreas, S.A., Votruba, P.: Tools for acquiring clinical guidelines in asbru (2002)

    Google Scholar 

  29. Seyfang, A., Miksch, S., Marcos, M., Wittenberg, J., Polo-Conde, C., Rosenbrand, K.: Bridging the gap between informal and formal guideline representations. In: 17th European Conference on Artificial Intelligence, Riva del Garda, Italy, pp. 447–451. IOS Press (2006)

    Google Scholar 

  30. Miksch, S., Hunter, J., Keravnou, E.T. (eds.): AIME 2005. LNCS (LNAI), vol. 3581. Springer, Heidelberg (2005)

    Google Scholar 

  31. Khan, M.G.: Rapid ECG Interpretation. Humana Press (2008)

    Google Scholar 

  32. Barold, S.S., Stroobandt, R.X., Sinnaeve, A.F.: Cardiac Pacemakers Step by Step. Futura Publishing (2004) ISBN 1-4051-1647-1

    Google Scholar 

  33. Bjorner, D.: Software Engineering 1-2-3. Texts in Theoretical Computer Science. An EATCS Series. Springer (2006)

    Google Scholar 

  34. Bjørner, D., Henson, M.C. (eds.): Logics of Specification Languages. EATCS Textbook in Computer Science. Springer (2007)

    Google Scholar 

  35. Chandy, K.M., Misra, J.: Parallel program design - a foundation. Addison-Wesley (1989)

    Google Scholar 

  36. Lamport, L.: Specifying Systems. The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)

    Google Scholar 

  37. Back, R.J., Xu, Q.: Refinement of fair action systems. Acta Inf. 35(2), 131–165 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  38. Leavens, G.T., Abrial, J.R., Batory, D., Butler, M., Coglio, A., Fisler, K., Hehner, E., Jones, C., Miller, D., Peyton-Jones, S., Sitaraman, M., Smith, D.R., Stump, A.: Roadmap for enhanced languages and methods to aid verification. In: Fifth Intl. Conf. Generative Programming and Component Engineering (GPCE 2006), pp. 221–235. ACM (October 2006)

    Google Scholar 

  39. Atelier, B.: ClearSy Aix-en-Provence (F), Version 3.6 (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Lorraine, LORIA, BP 70239, 54506, Vandoeuvre lès Nancy, France

    Dominique Méry & Neeraj Kumar Singh

Authors
  1. Dominique Méry
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Neeraj Kumar Singh
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, Casa Silva Mendes, Est. do Engenheiro Trigo No. 4, Macao, China

    Zhiming Liu

  2. Centre for Software Certification, McMaster University, 1280 Main Street West, ITB 202, L8S 4K1, Hamilton, ON, Canada

    Alan Wassyng

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Méry, D., Singh, N.K. (2012). Medical Protocol Diagnosis Using Formal Methods. In: Liu, Z., Wassyng, A. (eds) Foundations of Health Informatics Engineering and Systems. FHIES 2011. Lecture Notes in Computer Science, vol 7151. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32355-3_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32355-3_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32354-6

  • Online ISBN: 978-3-642-32355-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation