Complex medical processes as context for embedded systems

ABSTRACT

Many embedded systems are intended for use in complex and highly concurrent processes with multiple human agents. In these cases, the requirements for the system depend critically on the details of the process. If certification is to be useful for such systems, it must take the details of the process into account. In this paper, we describe some current research involving the formal definition and analysis of complex medical processes. We discuss the ways in which this work may provide a basis for a more complete understanding of the behavior of medical devices in the context of the processes in which they are used, and thus for certification methods for sophisticated embedded systems.

REFERENCES

• 1: Aaron G. Cass , Barbara Staudt Lerner , Stanley M. Sutton, Jr. , Eric K. McCall , Alexander Wise , Leon J. Osterweil, Little-JIL/Juliette: a process definition language and interpreter, Proceedings of the 22nd international conference on Software engineering, p.754-757, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337623]
• 2: [2] B. Chen, G.S. Avrunin, L.A. Clarke, and L.J. Osterweil. Automatic fault tree derivation from Little-JIL process definitions. In Proceedings of the Software Process Workshop/Workshop on Software Process Simulation (SPW/ProSim 2006), Shanghai, May 2006. to appear.
• 3: [3] E.M. Clarke, Jr., O. Grumberg, and D.A. Peled. Model Checking. MIT Press, Cambridge, 2000.
• 4: [4] L.A. Clarke, Y. Chen, G.S. Avrunin, B. Chen, R. Cobleigh, K. Frederick, E.A. Henneman, and L.J. Osterweil. Process programming to support medical safety. In M. Li, B. Boehm, and L.J. Osterweil, editors, Unifying the Software Process Spectrum: International Software Process Workshop, SPW 2005, number 3840 in LNCS, pages 347-359, Beijing, May 2005.
• 5: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 6: Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004 [doi>10.1145/1040291.1040292]
• 7: [7] G.J. Holzmann. The SPIN Model Checker. Addison-Wesley, Boston, 2004.
• 8: Jeff Magee , Jeff Kramer, Concurrency: state models & Java programs, John Wiley & Sons, Inc., New York, NY, 2000
• 9: [9] R.L. Smith, G.S. Avrunin, and L.A. Clarke. From natural language requirements to rigorous property specifications. In Workshop on Software Engineering for Embedded Systems (SEES 2003): From Requirements to Implementation, pages 40-46, Chicago, IL, Sept. 2003.
• 10: Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581345]
• 11: A. Wise, Little-JIL 1.0 Language Report TITLE2:, University of Massachusetts, Amherst, MA, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

  J. Computer Applications
  J.3 LIFE AND MEDICAL SCIENCES

General Terms:
Standardization