My photo


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.


I have served as a teaching assistant for the following courses at University of Bergamo:

  • 21029: Industrial Automation (Fall 2018)
  • 38068-2: Informatica III (Software Design and Algorithms) (Fall 2019)
  • 21013: Informatica II (Object Oriented Programming) (Spring 2020)
  • 21013: Informatica II (Operating Systems) (Spring 2020)

I have also been a teacher of:

  • The course "Industrial Automation" during the summer school CI-LAM at University of Naples (Summer 2019)
  • The courses "Software Architecture" and "Internet of Things" at Jobs Academy (Fall 2019)


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

    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
    TOOLS 2019
  • Combining Model Refinement and Test Generation for Conformance Testing of the IEEE PHD Protocol Using Abstract State Machines

    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 smartphones

    Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, Marco Radavelli, Feng Dian, Yu Lei
    ICTSS 2019


Università degli Studi di Bergamo, Viale Marconi 5, 24044 Dalmine, Italy
Building B - Room 3.02