Medical devices are safety-critical systems since their malfunctions can seriously compromise human safety. Correct operation of a medical device depends upon the controlling software, whose development should adhere to certification standards. However, these standards provide general descriptions of common software engineering activities without any indication regarding particular methods and techniques to assure safety and reliability. This paper discusses how to integrate the use of a formal approach into the current normative for the medical software development. The rigorous process is based on the Abstract State Machine (ASM) formal method, its refinement principle, and model analysis approaches the method supports. The hemodialysis machine case study is used to show how the ASM-based design process covers most of the engineering activities required by the related standards, and provides rigorous approaches for medical software validation and verification.

Integrating formal methods into medical software development : the ASM approach / P. Arcaini, S. Bonfanti, A. Gargantini, A. Mashkoor, E. Riccobene. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - 158(2018), pp. 148-167. [10.1016/j.scico.2017.07.003]

Integrating formal methods into medical software development : the ASM approach

P. Arcaini
;
E. Riccobene
2018

Abstract

Medical devices are safety-critical systems since their malfunctions can seriously compromise human safety. Correct operation of a medical device depends upon the controlling software, whose development should adhere to certification standards. However, these standards provide general descriptions of common software engineering activities without any indication regarding particular methods and techniques to assure safety and reliability. This paper discusses how to integrate the use of a formal approach into the current normative for the medical software development. The rigorous process is based on the Abstract State Machine (ASM) formal method, its refinement principle, and model analysis approaches the method supports. The hemodialysis machine case study is used to show how the ASM-based design process covers most of the engineering activities required by the related standards, and provides rigorous approaches for medical software validation and verification.
Medical device software; Hemodialysis device; Certification; Abstract State Machines; Formal analysis
Settore INF/01 - Informatica
Article (author)
File in questo prodotto:
File Dimensione Formato  
abz2016_SI_SCP_finalVersion.pdf

accesso aperto

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 661.41 kB
Formato Adobe PDF
661.41 kB Adobe PDF Visualizza/Apri
1-s2.0-S0167642317301430-main.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 2.39 MB
Formato Adobe PDF
2.39 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/585005
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 16
social impact