The development of medical devices is a safety-critical process, because a failure or a malfunction of the device can cause serious injuries to the patients whom use it. The application of a rigorous process for their development reduces the risk of failures since validation and verification activities can be performed in a objective, reproducible, and documentable manner. In this paper we present an approach based on the Abstract State Machine (ASM) formal method. Starting from the model, validation and verification (V&V) techniques can be applied. Furthermore, by step-wise refinement, a final model can be obtained, which can be automatically translated to code. The process is applied to the smart pill box case study. Starting from the ASM model, we generate code for the Arduino platform after the application of V&V activities. Furthermore, we introduce regulation (IEC62304) and guidelines (FDA General Principles of Software Validation) that support the developer in medical software development. In particular, we explain how ASMs formal process can be compliant with them.

(2019). Developing Medical Devices from Abstract State Machines to Embedded Systems: A Smart Pill Box Case Study . Retrieved from http://hdl.handle.net/10446/150814

Developing Medical Devices from Abstract State Machines to Embedded Systems: A Smart Pill Box Case Study

Bombarda, Andrea;Bonfanti, Silvia;Gargantini, Angelo
2019-01-01

Abstract

The development of medical devices is a safety-critical process, because a failure or a malfunction of the device can cause serious injuries to the patients whom use it. The application of a rigorous process for their development reduces the risk of failures since validation and verification activities can be performed in a objective, reproducible, and documentable manner. In this paper we present an approach based on the Abstract State Machine (ASM) formal method. Starting from the model, validation and verification (V&V) techniques can be applied. Furthermore, by step-wise refinement, a final model can be obtained, which can be automatically translated to code. The process is applied to the smart pill box case study. Starting from the ASM model, we generate code for the Arduino platform after the application of V&V activities. Furthermore, we introduce regulation (IEC62304) and guidelines (FDA General Principles of Software Validation) that support the developer in medical software development. In particular, we explain how ASMs formal process can be compliant with them.
2019
Bombarda, Andrea; Bonfanti, Silvia; Gargantini, Angelo Michele
File allegato/i alla scheda:
File Dimensione del file Formato  
pillbox_tools2019_PostAR.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 763.91 kB
Formato Adobe PDF
763.91 kB Adobe PDF   Visualizza/Apri
10.1007_978-3-030-29852-4_7.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 563.07 kB
Formato Adobe PDF
563.07 kB Adobe PDF   Visualizza/Apri
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/150814
Citazioni
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact