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 veri?cation 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 veri?cation (V&V) techniques can be applied. Furthermore, by step-wise re?nement, a ?nal model can be obtained, which
can be automatically translated to C ++ code. The process is applied to the smart pill box case study. Starting from the ASM
model, we generate C ++ 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.
[download the pdf file] [DOI]