A Model-Driven Approach For Designing Time-Critical Medical Devices

Abstract

While embracing the advances of embedded software and network connectivity, the medical devices industry is facing a swift transformation. The manufactures are intending to shrink the size of the equipment while keeping versatile capabilities as well as functional reliability. A distinguished class of cyber-physical system (CPS) has been put forward, namely medical cyber physical systems (MCPS). The challenge that is of most interests to us is the high assurance of the software safety of such systems. Model-driven design (MDD) has been used in developing software of safety-critical systems such as medical devices. Such a development process starts creating models based on mathematical semantics. Also, the process supports automatic transformation from models to low-level code that is correct-by-construction. Despite some benefits gained from the MDD, formal verification of the properties in terms of response times lacks considerations of the low-level execution time. This may lead to spurious verification results. We provide, for the first time, a framework for response time analysis of medical cyber-physical systems such as cardiac pacemakers that combines low-level worst case execution time with high-level response time analysis. In addition, the proposed approach relates timing verification results to determining the minimum frequency for an implementation. While ensuring the safety of timing behaviors, the approach could also provide a way to prolong the battery life, which is crucial for implantable devices. Our approach has been applied to the development of the pacemaker. We use BlokIDE, a tool-chain that supporting synchronous composition of IEC 61499 function block to complete high-level modeling based on the synchrony hypothesis, UPPAAL for checking the timing behavior of models and a timing analysis technique for statically predicting run-time execution based on a PRET machine. The results demonstrate that our approach is ideal for designing time-critical medical devices.