Refinement-based development of software-controlled safety-critical active medical devices
|Title||Refinement-based development of software-controlled safety-critical active medical devices|
|Booktitle||Software Quality. Software and Systems Quality in Distributed and Mobile Environments - Proc. SWQD 2015|
|Series||Lecture Notes in Business Information Processing|
Advanced medical devices exploit the advantages of embedded software whose development, due to their direct impact on human lives, is naturally subject to compliance with the stringent requirements of safety standards and regulations. This paper presents initial results and lessons learned from an ongoing project focusing on the development of a formal model of a sub-system 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 and analysis will contribute to the still sparse experience base available at the disposal of the scientific and practitioner community in the domain of AMDs.