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.
Download paper: pdf.