Since February 2019 I have been a researcher with University of Bergamo (Italy) and since October 2019 I am a PhD student in Software Engineering within the PhD school of Engineering and Applied Sciences at University of Bergamo (Italy), in the Computer Science Group, under the supervision of Prof. Angelo Gargantini.
My ongoing research activity involves methods suitable to guarantee a better quality for medical software, systems, devices and protocols, mainly by means of software testing and formal methods.
You can find a better explaination of my research project here.
You can view my current updated CV here.
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 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.Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini
In this paper we propose a new approach to conformance testing based on Abstract State Machine (ASM) model refinement. It consists in generating test sequences from ASM models and checking the conformance between code and models in multiple iterations. This process is applied at different models, starting from the more abstract model to the one that is very close to the code. The process consists of the following steps: (1) model the system as an Abstract State Machine, (2) generate test sequences based on the ASM model, (3) compute the code coverage using generated tests, (4) if the coverage is low refine the Abstract State Machine and return to step 2. We have applied the proposed approach to Antidote, an open-source implementation of IEEE 11073-20601 Personal Health Device (PHD) protocol which allows personal healthcare devices to exchange data with other devices such as small computers and smartphonesAndrea Bombarda, Silvia Bonfanti, Angelo Gargantini, Marco Radavelli, Feng Dian, Yu Lei