Medical device software malfunctioning can lead to injuries or death for humans and, therefore, its development should adhere to certification standards. However, these standards 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 presents a formal development process, based on the Abstract State Machine method, that integrates most of the activities required by the standards. The process permits to obtain, through a sequence of refinements, more detailed models that can be formally validated and verified. Offline and online testing techniques permit to check the conformance of the implementation w.r.t. the specification. The process is applied to the validation of the SAM medical software, that is used to measure the patients' stereoacuity in the diagnosis of amblyopia.
Formal validation and verification of a medical software critical component / P. Arcaini, S. Bonfanti, A. Gargantini, A. Mashkoor, E. Riccobene - In: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)[s.l] : IEEE, 2015. - ISBN 9781509002375. - pp. 80-89 (( convegno ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 tenutosi a Austin nel 2015.
Formal validation and verification of a medical software critical component
E. RiccobeneUltimo
2015
Abstract
Medical device software malfunctioning can lead to injuries or death for humans and, therefore, its development should adhere to certification standards. However, these standards 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 presents a formal development process, based on the Abstract State Machine method, that integrates most of the activities required by the standards. The process permits to obtain, through a sequence of refinements, more detailed models that can be formally validated and verified. Offline and online testing techniques permit to check the conformance of the implementation w.r.t. the specification. The process is applied to the validation of the SAM medical software, that is used to measure the patients' stereoacuity in the diagnosis of amblyopia.File | Dimensione | Formato | |
---|---|---|---|
07340473.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
799.13 kB
Formato
Adobe PDF
|
799.13 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.