Analyzing medical processes

ABSTRACT

This paper shows how software engineering technologies used to define and analyze complex software systems can also be effective in detecting defects in human-intensive processes used to administer healthcare. The work described here builds upon earlier work demonstrating that healthcare processes can be defined precisely. This paper describes how finite-state verification can be used to help find defects in such processes as well as find errors in the process definitions and property specifications. The paper includes a detailed example, based upon a real-world process for transfusing blood, where the process defects that were found led to improvements in the process.

References

1. V. Ambriola and V. Gervasi. On the systematic analysis of natural language requirements with circe. Automated Software Eng., 13(1):107--167, 2006.
2. G. S. Avrunin, L. A. Clarke, E. A. Henneman, and L. J. Osterweil. Complex medical processes as context for embedded systems. ACM SIGBED Rev., 3(4):9--14, 2006.
3. G. S. Avrunin, J. C. Corbett, and M. B. Dwyer. Benchmarking finite-state verifiers. Software Tools for Technology Transfer, 2(4):317--320, 2000.
4. M. Balser, W. Reif, G. Schellhorn, K. Stenzel, and A. Thums. Formal system development with kiv. In T. Maibaum, editor, Fundamental Approaches to Software Engineering, volume 1783 of LNCS, pages 363--366, 2000.
5. S. C. Bandinelli, A. Fugetta, and C. Ghezzi. Software process model evolution in the SPADE environment. IEEE Trans. on Softw. Eng., 19(12), December 1993.
6. J. Battles, H. Kaplan, T. van der Schaaf, and C. Shea. The attributes of medical event-reporting systems: experience with a prototype medical event-reporting system for transfusion medicine. Arch. Pathology Laboratory Medicine, 122:231--238, 1998.
7. S. Bäumler, M. Balser, A. Dunets, W. Reif, and J. Schmitt. Verification of medical guidelines by model checking - a case study. In A. Valmari, editor, SPIN, volume 3925 of LNCS, pages 219--233, 2006.
8. I. Z. Ben-Shaul and G. E. Kaiser. A paradigm for decentralized process modeling and its realization in the oz environment. In 16th international conference on Software Engineering, pages 179--188, 1994.
9. E. R. Boose, A. M. Ellison, L. J. Osterweil, L. Clarke, R. Podorozhny, J. L. Hadley, A. Wise, and D. R. Foster. Ensuring reliable datasets for environmental models and forecasts. In Ecological Informatics, volume 2, pages 237--247, 2007.
10. A. G. Cass, B. S. Lerner, E. K. McCall, L. J. Osterweil, J. Stanley M. Sutton, and A. Wise. Little-jil/juliette: A process definition language and interpreter. In 22nd Int. Conf. on Softw. Eng., pages 754--757, Limerick, Ireland, 2000.
11. B. Chen, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil. Automatic fault tree derivation from little-jil process definitions. In SPW/ProSim, volume 3966 of LNCS, pages 150--158, Shanghai, May 2006.
12. S. Christov, B. Chen, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil. Rigorously defining and analyzing medical processes: An experience report. In 1st International Workshop on Model-Based Trustworthy Health Information Systems, September 2007.
13. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV version 2: An opensource tool for symbolic model checking. In Proc. Int. Conf. on Computer-Aided Verification, volume 2404 of LNCS, Copenhagen, Denmark, July 2002. Springer.
14. E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans. on Prog. Lang. and Syst., 16(5):1512--1542, September 1994.
15. E. M. Clarke, O. G. Jr., and D. A. Peled. Model Checking. MIT Press, 2000.
16. J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil. Verifying properties of process definitions. In ACM SIGSOFT Int. Symp. on Software Testing and Analysis, pages 96--101, Portland, OR, August 2000.
17. R. L. Cobleigh, G. S. Avrunin, and L. A. Clarke. User guidance for creating precise and accessible property specifications. In 14th ACM SIGSOFT Int. Symp. on Foundations of Software Eng., pages 208--218, Portland, OR, November 2006.
18. J. C. Corbett and G. S. Avrunin. Using integer programming to verify general safety and liveness properties. Formal Methods System Design, 6(1):97--123, 1995.
19. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, 1977.
20. D. Drusinsky. Visual formal specification using (n)tlcharts: Statechart automata with temporal logic and natural language conditioned transitions. In International Workshop on Parallel and Distributed Systems: Testing and Debugging, April 2004.
21. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In 21st Int. Conf. on Softw. Eng., pages 411--420, Los Angeles, May 1999.
22. M. B. Dwyer, L. A. Clarke, J. M. Cobleigh, and G. Naumovich. Flow analysis for verifying properties of concurrent software systems. ACM Trans. Softw. Eng. Methodol., 13(4):359--430, October 2004.
23. M. Foss and S. Moore. Evolution of quality management: integration of quality assurance functions into operations, or "quality is everyone's responsibility". Transfusion, 43(9):1330--1336, September 2003.
24. N. E. Fuchs, U. Schwertel, and R. Schwitter. Attempto controlled english - not just another logic specification language. In P. Flener, editor, 8th International Workshop on Logic Programming Synthesis and Transformation, number 1559 in LNCS, pages 1--20, 1998.
25. S. Galel and C. Richards. Practical approaches to improve laboratory performance and transfusion safety. American Journal of Clinical Pathology, 107(4):S43--S49, 1997.
26. S. Graf and H. Saïdi. Construction of abstract state graphs with pvs. In 9th Int. Conf. on Computer Aided Verification, number 1254 in LNCS, pages 72--83, 1997.
27. B. N. Grosof, Y. Labrou, and H. Y. Chan. A declarative approach to business rules in contracts: courteous logic programs in XML. In ACM Conf. on Electronic Commerce, pages 68--77, Denver, CO, 1999.
28. E. A. Henneman, G. S. Avrunin, L. A. Clarke, L. J. Osterweil, C. Andrzejewski, Jr., K. Merrigan, R. Cobleigh, K. Frederick, E. Katz-Bassett, and P. L. Henneman. Increasing patient safety and efficiency in transfusion therapy using formal process definitions. In Transfusion Medicine Review, volume 21, pages 49--57, January 2007.
29. G. J. Holzmann. The SPIN Model Checker. Addison-Wesley, 2004.
30. R. Iosif, M. B. Dwyer, and J. Hatcliff. Translating java for multiple model checkers: The bandera back-end. Formal Methods in System Design, 26(2):137--180, March 2005.
31. L. T. Kohn, J. M. Corrigan, and M. S. Donaldson, editors. To Err Is Human: Building a Safer Health System. National Academy Press, Washington, D.C., 1999.
32. B. S. Lerner. Verifying process models built using parameterized state machines. In ACM SIGSOFT Int. Symp. on Software Testing and Analysis, pages 274--284, New York, USA, 2004.
33. G. Molino, P. Terenziani, S. Montani, A.Bottrighi, and M. Torchio. Glare: a domain-independent system for acquiring, representing and executing clinical guidelines. In J. of the Amer. Medical Informatics Association (JAMIA) Symposium supplement, 2006.
34. R. Noumeir. Radiology interpretation process modeling. J. of Biomedical Informatics, 39(2):103--114, 2006.
35. L. J. Osterweil, N. K. Sondheimer, L. A. Clarke, E. Katsh, and D. Rainey. Using process definitions to facilitate the specification of requirements. Technical report, Department of Computer Science, University of Massachusetts Amherst, 2006.
36. S. Paul, E. Park, and J. Chaar. Rainman: a work flow system for the internet. In USENIX Symp. on Internet Technologies and Systems, Berkeley, CA, 1997.
37. M. S. Raunak, B. Chen, A. Elssamadisy, L. A. Clarke, and L. J. Osterweil. Definition and analysis of election processes. In SPW/ProSim 2006, volume 3966 of LNCS, pages 178--185, Shanghai, May 2006.
38. M. S. Raunak and L. J. Osterweil. Effective resource allocation for process simulation: A position paper. In 6th International Workshop on Software Process Simulation and Modeling, St. Louis, MO, May 2005.
39. P. P. Reid, W. D. Compton, J. H. Grossman, and G. Fanjiang, editors. Building a Better Delivery System: A New Engineering/Health Care Partnership. National Academy Press, Washington, D.C., 2005.
40. M. Ruffolo, C. Information, and R. Curia. Process management in health care: A system for preventing risks and medical errors. In Business Process Management, pages 334--343, 2005.
41. Y. Shahar, S. Miksch, and P. Johnson. The asgaard project: a task-specific framework for the application and critiquing of time-oriented clinical guidelines. Artificial Intelligence in Medicine, 14(1-2):29--51, 1998.
42. D. H. Stamatis. Failure Mode and E ect Analysis: FMEA from Theory to Execution. Amer Society for Quality, March 1995.
43. D. R. Sutton and J. Fox. The syntax and semantics of the proforma guideline modeling language. In Journal of the American Medical Informatics Association, volume 10, pages 433--443, Sep-Oct 2003.
44. J. S. M. Sutton, D. Heimbigner, and L. J. Osterweil. Appl/a: a language for software process programming. ACM Trans. on Software Engineering and Methodology, 4(3):221--286, 1995.
45. A. ten Teije, M. Marcos, M. Balser, J. van Croonenborg, C. Duelli, F. van Harmelen, P. Lucas, S. Miksch, W. Reif, K. Rosenbrand, and A. Seyfang. Improving medical protocols by formal methods. Artificial Intell. in Medicine, 36(3):193--209, 2006.
46. P. Terenziani, L. Giordano, A. Bottrighi, S. Montani, and L. Donzella. Spin model checking for the verification of clinical guidelines. In ECAI 2006 Workshop on AI techniques in healthcare: evidence-based guidelines and protocols, August 2006.
47. L. van der Gaag, S. Renooji, C. Witteman, B. Aleman, and B. Taal. Probabilities for a probabilistic network: a case study in oesophageal cancer. Artificial Intelligence in Medicine, 25(2):123--148, June 2002.
48. W. Vesely, F. Goldberg, N. Roberts, and D. Haasl. Fault Tree Handbook (NUREG-0492). U.S. Nuclear Regulatory Commission, Washington, D.C., Jan. 1981.
49. D. Voak, J. Chapman, and P. Phillips. Quality of transfusion practice beyond the blood transfusion laboratory is essential to prevent abo-incompatible death. Transfusion Medicine, 10(2):95--96, June 2000.
50. J. M. Wilkinson and K. V. Leuven. Fundamentals of Nursing. F. A. Davis Company, June 2007.
51. J. M. Wilkinson and K. V. Leuven. Procedure checklist for administering a blood transfusion. http://davisplus.fadavis.com/wilkinson/PDFs/Procedure_Checklists/PC_Ch36-01.pdf, 2007.

Index Terms

• Applied computing

  • Life and medical sciences

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification