Towards Formal Modeling and Analysis of Networks of Embedded Medical Devices in Real-Time Maude

With the increasing number of medical devices and of accidents resulting from them being used in isolation in a hectic operating room, there is a trend towards integrating such devices into networks. This paper describes the application of the Real-Time Maude tool to the formal modeling and analysis of a network integrating an x-ray machine, a ventilation machine, and a controller. This case study is motivated by an accidental death in an operating room. As part of the formal specification and analysis, the paper introduces novel techniques for: (i) modeling nondeterministic transmission delays while maintaining completeness and reasonable performance of the analysis; (ii) modeling clock drifts; and (iii) analyzing bounded response properties.

• Type: Conference
• Year: 2008
• Where: SNPD
• Authors: Peter Csaba Ölveczky
• Keywords: Artificial Intelligence, Hectic Operating Room, Operating Room, Real-Time Maude Tool, SNPD 2008