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.