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)
  • 21056: Software Testing and Verification (Spring 2020)
  • 39170-ENG: Data Science and Automation (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 Duan, Yu Lei
    ICTSS 2019
  • Dealing with Robustness of Convolutional Neural Networks for Image Classification

    SW-based systems depend more and more on AI also for critical tasks. For instance, the use of machine learning, especially for image recognition, is increasing ever more. As stateof-the-art, Convolutional Neural Networks (CNNs) are the most adopted techniques for image classification. Although they are proved to have optimal results, it is not clear what happens when unforeseen modifications during the image acquisition and elaboration occur. Thus, it is very important to assess the robustness of a CNN, especially when it is used in a safety critical system, as, eg, in the medical domain or in automated driving systems. Most of the analyses made about the robustness of CNNs are focused on adversarial examples which are created by exploiting the CNN internal structure; however, these are not the only problems we can encounter with CNNs and, moreover, they may be unlikely in some fields. This is why, in this paper, we focus on the robustness analysis when plausible alterations caused by an error during the acquisition of the input images occur. We give a novel definition of robustness wrt possible input alterations for a CNN and we propose a framework to compute it. Moreover, we analyse four methods (data augmentation, limited data augmentation, network parallelization, and limited network parallelization) which can be used to improve the robustness of a CNN for image classification. Analyses are conducted over a dataset of histologic images.

    Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini
    AI Test 2020
  • An Automata-Based Generation Method for Combinatorial Sequence Testing of Finite State Machines

    Combinatorial Interaction Testing has been applied to event-driven software systems by using as tests a set of sequences of inputs in desired combinations. This is generally called combinatorial sequence testing (CST). CST requires possibly new system models from which tests are generated and new test generation methods (or an adaptation of the classical ones). Finite State Machines (FSMs) can easily represent event-based systems where the constraints that certain inputs are valid only in some states can be represented by the incompleteness of the FSM. In this paper we propose an automata-based method to generate combinatorial tests from FMSs by representing FSMs and test requirements by automata and then by generating test sequences from those automata. When building the automata, we can directly embed the system constraints over the inputs, but we also analyse three different methods suitable to fix and repair event sequences generated without taking into account the constraints of the system. We compare our automata-based method with the standard approach of Sequences Covering Arrays (SCAs) that produces a set of sequences, all with the same length, composed by the permutation of all the events supported by the system.

    Andrea Bombarda, Angelo Gargantini
    IWCT 2020


Università degli Studi di Bergamo, Viale Marconi 5, 24044 Dalmine, Italy