How to assure correctness and safety of medical software: The hemodialysis machine case study

Authors Paolo Arcaini
Silvia Bonfanti
Angelo Gargantini
Elvinia Riccobene
Editors Michael Butler
Klaus-Dieter Schewe
Atif Mashkoor
Miklós Biró
Title How to assure correctness and safety of medical software: The hemodialysis machine case study
Booktitle Abstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2016
Type in proceedings
Publisher Springer
Series Lecture Notes in Computer Science
Volume 9676
ISBN 978-3-319-33599-5
DOI 10.1007/978-3-319-33600-8_30
Month May
Year 2016
Pages 344-359
SCCH ID# 1648
Abstract

Medical devices are nowadays more and more software dependent, and software malfunctioning can lead to injuries or death for patients. Several standards have been proposed for the development and the validation of medical devices, but they establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability.

This paper takes advantage of the Hemodialysis machine case study to present a formal development process supporting most of the engineering activities required by the standards, and provides rigorous approaches for system validation and verification. The process is based on the Abstract State Machine formal method and its model refinement principle.