Advanced medical devices exploit the advantages of embedded software whose development is subject to compliance with stringent requirements of standardization and certification regimes due to the critical nature of such systems. This paper presents initial results and lessons learned from an ongoing project focusing on the development of a formal model of a subsystem of a software-controlled safety-critical active medical device (AMD) responsible for renal replacement therapy. The use of formal approaches for the development of AMDs is highly recommended by standards and regulations, and motivates the recent advancement of the state of the art of related methods and tools including Event-B and Rodin applied in this paper. It is expected that the presented model development approach and the specification of a high-confidence medical system will contribute to the still sparse experience base available at the disposal of the scientific and practitioner community of formal methods and software engineering.
One of the medical devices relatively close to hemodialysis machines is an infusion pump. It is primarily responsible for delivering fluids, such as nutrients and medications, into a patient's body in controlled amounts. @cite_30 present a reference model of PCA (Patient Control Analgesia) infusion pumps and test the model for structural and safety properties, Jos ' e et al @cite_27 present a formal model in MAL (Modal Action Logic) @cite_36 that helps compare different infusion devices and their provided functionalities, and @cite_1 use the ProZ model checker @cite_28 to test various safety properties of infusion pumps.
@cite_30 @cite_28 @cite_36 @cite_1 @cite_27
2149519129 1491364274 2103839338 2023753675 2107114959
As software becomes ever more ubiquitous and complex in medical devices, it becomes increasingly important to assure that it performs safely and effectively. The critical nature of medical devices necessitates that the software used therein be reliable and free of errors. It becomes imperative, therefore, to have a conformance review process in place to ascertain the correctness of the software and to ensure that it meets all requirements and standards. Formal methods have long been suggested as a means to design and develop medical device software. However, most manufacturers shy from using these techniques, citing them as too complex and time consuming. As a result, (potentially life-threatening) errors are often not discovered until a device is already on the market. In this paper we present a reference model based approach to software conformance checking. Reference models enable the application of formal methods to software conformance checking, and provide a framework for rigorous testing. To illustrate the approach, we develop the reference model for a generic patient controlled analgesic infusion pump, and explain how it can be used to aid software conformance checking in a regulatory environment. We present the architecture and implementation of the proz tool to validate high-level Z specifications. The tool was integrated into prob, by providing a translation of Z into B and by extending the kernel of prob to accommodate some new syntax and data types. We describe the challenge of going from the tool friendly formalism B to the more specification-oriented formalism Z, and show how many Z specifications can be systematically translated into B. We describe the extensions, such as record types and free types, that had to be added to the kernel to support a large subset of Z. As a side-effect, we provide a way to animate and model check records in prob. By incorporating proz into prob, we have inherited many of the recent extensions developed for B, such as the integration with CSP or the animation of recursive functions. Finally, we present a successful industrial application, which makes use of this fact, and where proz was able to discover several errors in Z specifications containing higher-order recursive functions. The paper explores the role that formal modeling may play in aiding the visualization and implementation of usability requirements of a control panel. We propose that this form of analysis should become a systematic and routine aspect of the development of such interfaces. We use a notation for describing the interface that is convenient to use by software engineers, and describe a set of tools designed to make the process systematic and exhaustive. Formally modelling the software functionality and interactivity of safety-critical devices allows us to prove properties about their behaviours and be certain that they will respond to user interaction correctly. In domains such as medical environments, where many different devices may be used, it is equally important to ensure that all devices used adhere to a set of safety, and other, principles designed for that environment. In this paper we look at modelling important properties of interactive medical devices including safety considerations mandated by their users. We use ProZ for model checking to ensure that properties stated in temporal logic hold, and also to check invariants. In this way we gain confidence that important properties do hold of the device, and that models of particular devices adhere to the properties described. This paper is concerned with the scaleable and systematic analysis of interactive systems. The motivating problem is the procurement of medical devices. In such situations several different manufacturers offer solutions that support a par- ticular clinical activity. Apart from cost, which is a dominating factor, the variations between devices are relatively subtle and the consequences of particular design fea- tures are not clear from manufacturers' manuals, demonstrations or trial uses. De- spite their subtlety these differences can be important to the safety and usability of the device. The paper argues that formal analysis of the range of offered devices can provide a systematic means of comparison. The paper also explores barriers to the use of such techniques, demonstrating how layers of specification may be used to make it possible to reuse common specification. Infusion pumps provide a motivat- ing example. A specific model is described and analysed and comparison between competitive devices is discussed.