• model-based design prototyping
• formal verification
• co-simulation
• safety-critical medical systems

Electromedical devices are safety-critical systems, whose failure could result in injuries to patients and, in the worst case, in loss of life. In particular, interactive medical devices are prone to usage errors due to the increasing complexity or insufficient documentation of user interfaces. In addition, modern clinical practices involve interconnected medical devices operating under computer-assisted human supervision (Integrated Clinical Environments). In these types of environments, interoperability is a crucial concern, because equipment from disparate vendors must communicate over different networks. This work explores model-based design technologies for rapid prototyping of interactive medical devices and their co-simulation into an Integrated Clinical Environment. Model-based design allows the behaviour of the system to be tested and verified at an early stage of the system design, and before the real device is built and used on the patient. In particular, the thesis reports on implementing a prototype of the Medical Monitor Siemens SC 7000, together with its client-server application that allows communication with the embedded software. Widgets related to the user interface of the device have been developed, and a model of the software controller has been built in a formal language using reverse engineering. Properties of the devices have been analysed by formal tools. Finally, the prototype has been exported as a Functional Mock-up Unit (FMU), and used as a component in a co-simulation scenario together with an infusion pump, a supervisor and the pharmacokinetic model of a patient. Co-simulation results are discussed.