Publications | FOSELAB

2024

Design, implementation, and validation of a benchmark generator for combinatorial interaction testing tools

Andrea Bombarda, and Angelo Gargantini

Journal of Systems and Software, Mar 2024

2023

Multi-thread Combinatorial Test Generation with SMT solvers

Andrea Bombarda, Angelo Gargantini, and Andrea Calvagna

Mar 2023
A component framework for the runtime enforcement of safety properties

Silvia Bonfanti, Elvinia Riccobene, and Patrizia Scandurra

THE JOURNAL OF SYSTEMS AND SOFTWARE, Mar 2023
Modeling the MVM-Adapt System by Compositional I/O Abstract State Machines

Silvia Bonfanti, Elvinia Riccobene, Davide Santandrea, and 1 more author

Mar 2023
RATE: A model-based testing approach that combines model refinement and test execution

Andrea Bombarda, Silvia Bonfanti, Angelo Michele Gargantini, and 2 more authors

SOFTWARE TESTING VERIFICATION & RELIABILITY, Mar 2023

Abs HTML

In this paper, we present an approach to conformance testing based on abstract state machines (ASMs) that combines model refinement and test execution (RATE) and its application to three case studies. The RATE approach consists in generating test sequences from ASMs and checking the conformance between code and models in multiple iterations. The process follows these steps: (1) model the system as an abstract state machine; (2) validate and verify the model; (3) generate test sequences automatically from the ASM model; (4) execute the tests over the implementation and compute the code coverage; (5) if the coverage is below the desired threshold, then refine the abstract state machine model to add the uncovered functionalities and return to step 2. We have applied the proposed approach in three case studies: a traffic light control system (TLCS), the IEEE 11073-20601 personal health device (PHD) protocol, and the mechanical ventilator Milano (MVM). By applying RATE, at each refinement level, we have increased code coverage and identified some faults or conformance errors for all the case studies. The fault detection capability of RATE has also been confirmed by mutation analysis, in which we have highlighted that, many mutants can be killed even by the most abstract models.
Incremental generation of combinatorial test suites starting from existing seed tests

Andrea Bombarda, and Angelo Gargantini

Apr 2023

Abs HTML

Many researchers have been focusing on building combinatorial test generators having the best possible performances, in terms of smaller test suites and shorter generation times. The majority of tools generates test suites from scratch. This means that when the test suite must be regenerated, the old tests are discarded and a new test suite is built. However, there are many cases in which old test cases, possibly written by hand, need to be (or could be) included in the final test suite, and the test suite completed with new tests in order to reach the desired level of combinatorial coverage. These existing tests that are reused are generally called \emphseed tests. Seed tests could be important for testing domain-specific critical parts of the system, or they could represent old test suites that must be enriched to reach the desired (possibly higher) strength of coverage. In this paper, we propose a new architecture for incremental test generation that starts from existing test seeds. This new architecture is supported by the pMEDICI+ tool which extends our previous effort done for pMEDICI. We evaluate the proposed approach on the benchmarks given in the context of the second edition of the CT-Competition and w.r.t. two application scenarios. For each scenario, we automatically generate seed tests and then we apply pMEDICI+ to obtain the desired test suite. The experiments highlight that using incremental test generation can contribute significantly in the reduction of test generation time and, in many cases, in the reduction of the test suite size.
Formal MVC: A Pattern for the Integration of ASM Specifications in UI Development

Andrea Bombarda, Silvia Bonfanti, and Angelo Gargantini

Apr 2023

Abs HTML

Using architectural patterns is of paramount importance for guaranteeing the correct functionality, maintainability and modularity, especially for complex software systems. The model-view-controller (MVC) pattern is typically used in user interfaces (UIs), since it allows the separation between the internal representation of the information and the way it is shown to users. The main problem of using this approach in a formal setting, where formal models are used to specify the requirements and prove safety properties, is that those models are not directly used within the MVC pattern and, thus, all the activities performed at model-level are somehow lost when implementing the UI. For this reason, in this paper, we present the formal MVC pattern (fMVC), an extension of the classical MVC where the model is a formal specification, written using Abstract State Machines. This pattern is supported by the AsmetaFMVCLib, which allows the user to link the formal model with the view and the controller by using simple Java annotations. We present the application of fMVC on a simple example of a calculator for explanatory purposes, then we apply it to the AMAN case study, which has inspired the definition of fMVC. We discuss the advantages of fMVC and its shortcomings, trying to identify the scenarios where it should be applied and possible alternatives.
On the Reuse of Existing Configurations for Testing Evolving Feature Models

Andrea Bombarda, Silvia Bonfanti, and Angelo Gargantini

Aug 2023

Abs HTML

Software Product Lines (SPLs) are used for representing a variety of highly configurable systems or families of systems. They are commonly represented by feature models (FMs). Starting from FMs, configurations, used as test cases, can be generated to identify the products of interest for further activities. As the other types of software, SPLs and their FMs may evolve due to changing requirements or bug-fixing. However, no guidance is usually given on what to do with derived configurations when an FM evolves. The common approach is based on generating all configurations from scratch, which is not optimal since a greater effort is required for concretizing the new tests, and some of the old ones may be still applicable. In this paper, we present the use of a technique for generating combinatorial tests for evolving feature models: this technique incrementally builds the new combinatorial configuration set starting from the one generated from the previous model. Furthermore, we present a novel definition of dissimilarity among configuration sets that can be used to evaluate how much an evolved test suite differs from the previous one and thus allows evaluating the effort required for adapting old test cases to the new ones. Our experiments confirm that using the proposed technique, in general, leads to lower dissimilarity and test suite size w.r.t. the generation of tests from scratch.

2022

Automatic test generation with ASMETA for the Mechanical Ventilator Milano controller

Andrea Bombarda, Silvia Bonfanti, and Angelo Michele Gargantini

Aug 2022

Abs HTML

This paper presents an automatic test cases generation method from Abstract State Machine specifications. Starting from the ASMETA specification, the proposed approach applies the following steps: 1. Generation of abstract tests from a ASMETA model; 2. Optimization of the abstract tests; 3. Concretization of the abstract tests in GoogleTest; 4. Execution of the concrete tests on code. We have applied this approach to the Mechanical Ventilator Milano (MVM) project, which our research group has contributed to develop, test, and certify during the Covid-19 pandemic.
Compositional Simulation of Abstract State Machines for Safety Critical Systems

Silvia Bonfanti, Angelo Michele Gargantini, Elvinia Riccobene, and 1 more author

Aug 2022
Evaluation of Algorithms to Measure a Psychophysical Threshold Using Digital Applications

Silvia Bonfanti, and Angelo Michele Gargantini

Aug 2022
Guidelines for the development of a critical software under emergency

Andrea Bombarda, Silvia Bonfanti, Cristiano Galbiati, and 4 more authors

INFORMATION AND SOFTWARE TECHNOLOGY, Aug 2022

Abs HTML

Context: During the first wave of the COVID-19 pandemic, an international and heterogeneous team of scientists collaborated on a social project to produce a mechanical ventilator for intensive care units (MVM). MVM has been conceived to be produced and used also in poor countries: it is open-source, no patents, cheap, and can be produced with materials that are easy to retrieve. Objective: The objective of this work is to extract from the experience of the MVM development and software certification a set of lessons learned and then guidelines that can help developers to produce safety-critical devices in similar emergency situations. Method: We conducted a case study. We had full access to source code, comments on code, change requests, test reports, every deliverable (60 in total) produced for the software certification (safety concepts, requirements specifications, architecture and design, testing activities, etc.), notes, whiteboard sketches, emails, etc. We validated both lessons learned and guidelines with experts. Findings: We contribute a set of validated lessons learned and a set of validated guidelines, together with a discussion of benefits and risks of each guideline. Conclusion: In this work we share our experience in certifying software for healthcare devices produced under emergency, i.e. with strict and pressing time constraints and with the difficulty of establishing a heterogeneous development team made of volunteers. We believe that the guidelines will help engineers during the development of critical software under emergency.
Robustness assessment and improvement of a neural network for blood oxygen pressure estimation

Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, and 3 more authors

Aug 2022

HTML
Towards an Evaluation Framework for Autonomous Systems

Andrea Bombarda, Silvia Bonfanti, Martina De Sanctis, and 4 more authors

Aug 2022

HTML
Parallel Test Generation for Combinatorial Models Based on Multivalued Decision Diagrams

Andrea Bombarda, and Angelo Gargantini

Apr 2022

Abs HTML

Combinatorial interaction testing (CIT) is a testing technique that has proved to be effective in finding faults due to the interaction among inputs, and in reducing the number of test cases. One of the most crucial parts of combinatorial testing is the test generation for which many tools and algorithms have been proposed in recent years, with different methodologies and performances. However, generating tests remains a complex procedure that can require a lot of effort (mainly time). Thus, in this paper, we present the tool pMEDICI which aims to reduce the test generation time by parallelizing the generation process and exploiting the recent multithread hardware architectures. It uses Multivalued Decision Diagrams (MDDs) for representing the constraints and the tuples to be tested and extracts from them the t-wise test cases. Our experiments confirm that our tool requires a shorter amount of time for generating combinatorial test suites, especially for complex models, with a lot of parameters and constraints.

2021

A Runtime Safety Enforcement Approach by Monitoring and Adaptation

Silvia Bonfanti, Elvinia Riccobene, and Patrizia Scandurra

Apr 2021
Comparison of Algorithms to Measure a Psychophysical Threshold using Digital Applications: The Stereoacuity Case Study

Angelo Michele Gargantini, and Silvia Bonfanti

Apr 2021
Developing a Prototype of a Mechanical Ventilator Controller from Requirements to Code with ASMETA

Andrea Bombarda, Silvia Bonfanti, Angelo Michele Gargantini, and 1 more author

Apr 2021

HTML
Efficient Computation of Robustness of Convolutional Neural Networks

Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, and 1 more author

Apr 2021

HTML
Evaluation of stereoacuity with a digital mobile application

Silvia Bonfanti, Angelo Michele Gargantini, Gabriele Esposito, and 3 more authors

GRAEFE’S ARCHIVE FOR CLINICAL AND EXPERIMENTAL OPHTHALMOLOGY, Apr 2021
Extending ASMETA with Time Features

Andrea Bombarda, Silvia Bonfanti, Angelo Michele Gargantini, and 1 more author

Apr 2021

HTML
Il successo di MVM, un progetto social e internazionale per realizzare un ventilatore polmonare

Silvia Bonfanti, Andrea Bombarda, Angelo Michele Gargantini, and 2 more authors

IL GIORNALE DELL’INGEGNERE, Apr 2021
Lessons Learned from the Development of a Mechanical Ventilator for COVID-19

Andrea Bombarda, Silvia Bonfanti, Cristiano Galbiati, and 4 more authors

Apr 2021

HTML
ROBY: A Tool for Robustness Analysis of Neural Network Classifiers

Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, and 1 more author

Apr 2021

HTML
The ASMETA Approach to Safety Assurance of Software Systems

Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, and 3 more authors

Apr 2021

HTML
The novel Mechanical Ventilator Milano for the COVID-19 pandemic

A. Abba, C. Accorsi, P. Agnes, and 233 more authors

PHYSICS OF FLUIDS, Apr 2021
An environment for benchmarking combinatorial test suite generators

Andrea Bombarda, Edoardo Crippa, and Angelo Gargantini

Apr 2021

Abs HTML

New tools for combinatorial test generation are proposed every year. However, different generators may have different performances on different models, in terms of the number of tests produced and generation time, so the choice of which generator has to be used can be challenging. Classical comparison between CIT generators considers only the number of tests composing the test suite. Still, especially when the time dedicated to testing activity is limited, generation time can be determinant. Thus, we propose a benchmarking framework including 1) a set of generic benchmark models, 2) an interface to easily integrate new generators, 3) methods to benchmark each generator against the others and to check validity and completeness. We have tested the proposed environment using five different generators (ACTS, CAgen, CASA, Medici, and PICT), comparing the obtained results in terms of the number of test cases and generation times, errors, completeness, and validity. Finally, we propose a CIT competition, between combinatorial generators, based on our framework.

2020

Addressing usability in a formal development environment

Paolo Arcaini, Silvia Bonfanti, Angelo Michele Gargantini, and 2 more authors

Apr 2020
Dealing with Robustness of Convolutional Neural Networks for Image Classification

Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, and 1 more author

Apr 2020

HTML
Design and validation of a C++ code generator from Abstract State Machines specifications

Silvia Bonfanti, Angelo Michele Gargantini, and A. Mashkoor

JOURNAL OF SOFTWARE, Apr 2020
Modelling an Automotive Software-Intensive System with Adaptive Features Using ASMETA

Paolo Arcaini, Silvia Bonfanti, Angelo Michele Gargantini, and 2 more authors

Apr 2020
An Automata-Based Generation Method for Combinatorial Sequence Testing of Finite State Machines

Andrea Bombarda, and Angelo Gargantini

Oct 2020

Abs HTML

Combinatorial Interaction Testing has been applied to event-driven software systems by using as test suite 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 certain inputs are valid only in some states and such constraints can be represented by the incompleteness of the FSM. In this paper, we propose an approach to CST where tests are generated from FSMs which are represented by automata together with test requirements. First, automata can be used to check if test sequences contain invalid inputs. We propose three methods to repair tests with invalid inputs. Moreover, we can directly embed into automata the system constraints over the inputs during generations, to generate only valid test sequences. 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. We found that generating only valid tests from automata provides several advantages iv.r.t. repairing tests and SCAs.

2019

Combining Model Refinement and Test Generation for Conformance Testing of the IEEE PHD Protocol Using Abstract State Machines

Andrea Bombarda, Silvia Bonfanti, Angelo Michele Gargantini, and 3 more authors

Oct 2019

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

Andrea Bombarda, Silvia Bonfanti, and Angelo Michele Gargantini

Oct 2019

HTML

2018

AsmetaA: Animator for abstract state machines

Silvia Bonfanti, Angelo Michele Gargantini, and Atif Mashkoor

Oct 2018
A systematic literature review of the use of formal methods in medical software systems

Silvia Bonfanti, Angelo Michele Gargantini, and Atif Mashkoor

JOURNAL OF SOFTWARE MAINTENANCE AND EVOLUTION: RESEARCH AND PRACTICE, Oct 2018
Behind optical factors in anisometropic aniseiconia

Gabriele Esposito, Alessio Facchin, MARTA NICOLE Maffioletti, and 5 more authors

Oct 2018
Generation of behavior-driven development C++ tests from abstract state machine scenarios

Silvia Bonfanti, Angelo Michele Gargantini, and Atif Mashkoor

Oct 2018
Generation of C++ Unit Tests from Abstract State Machines Specifications

Silvia Bonfanti, Angelo Michele Gargantini, and Atif Mashkoor

Oct 2018
Integrating formal methods into medical software development: The ASM approach

Paolo Arcaini, Silvia Bonfanti, Angelo Michele Gargantini, and 2 more authors

SCIENCE OF COMPUTER PROGRAMMING, Oct 2018
Stereo Digital Displays for Diagnosis and Treatment of Amblyopia

Silvia Bonfanti, and Angelo Michele Gargantini

Oct 2018
Validation of transformation from abstract state machine models to C++ code

Silvia Bonfanti, Angelo Michele Gargantini, and Atif Mashkoor

Oct 2018

2017

Amblyopia Rehabilitation by Games for Low-Cost Virtual Reality Visors

Silvia Bonfanti, and Angelo Michele Gargantini

Oct 2017
Asm2C++: A tool for code generation from abstract state machines to Arduino

Silvia Bonfanti, Marco Carissoni, Angelo Michele Gargantini, and 1 more author

Oct 2017
The female contribution in architecting a set of tools for a formal method. Role of women in Software Architecture

Silvia Bonfanti, Valentina Centurelli, Elvinia Riccobene, and 1 more author

Oct 2017

2016

A preliminary systematic literature review of the use of formal methods in medical software systems

Silvia Bonfanti, Angelo Michele Gargantini, and Atif Mashkoor

Oct 2016
How to assure correctness and safety of medical software: The hemodialysis machine case study

Paolo Arcaini, Silvia Bonfanti, Angelo Michele Gargantini, and 1 more author

Oct 2016
Unified syntax for abstract state machines

Paolo Arcaini, Silvia Bonfanti, Marcel Dausend, and 6 more authors

Oct 2016
Visual Notation and Patterns for Abstract State Machines

Paolo Arcaini, Silvia Bonfanti, Angelo Michele Gargantini, and 1 more author

Oct 2016

2015

A Low-cost Virtual Reality Game for Amblyopia Rehabilitation

Angelo Michele Gargantini, Fabio Terzi, Matteo Zambelli, and 1 more author

Oct 2015
A mobile application for the stereo acuity test

Silvia Bonfanti, Angelo Michele Gargantini, and Andrea Vitali

Oct 2015
Formal validation and verification of a medical software critical component

Paolo Arcaini, Silvia Bonfanti, Angelo Michele Gargantini, and 2 more authors

Oct 2015