Contact Teaching Publications Research Home
Matching entries: 0
settings...
AuthorTitleYearJournal/ProceedingsReftypeDOI/URL
Bonfanti, S., Riccobene, E. and Scandurra, P. A component framework for the runtime enforcement of safety properties

[BibTeX]

 2023 THE JOURNAL OF SYSTEMS AND SOFTWARE
Vol. 198(art. 111605), pp. 1-46 		 article DOI  
BibTeX: 
@article{10446_235472,
  author = {Bonfanti, Silvia and Riccobene, Elvinia and Scandurra, Patrizia},
  title = {A component framework for the runtime enforcement of safety properties},
  journal = {THE JOURNAL OF SYSTEMS AND SOFTWARE},
  year = {2023},
  volume = {198},
  number = {art. 111605},
  pages = {1--46},
  doi = {https://doi.org/10.1016/j.jss.2022.111605}
}
Bombarda, A., Bonfanti, S., Gargantini, A.M., Lei, Y. and Duan, F. RATE: A model-based testing approach that combines model refinement and test execution

[BibTeX]

 2022 SOFTWARE TESTING VERIFICATION & RELIABILITY(Art. n. 1835), pp. 1-34  article DOI  
BibTeX: 
@article{10446_235470,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo Michele and Lei, Yu and Duan, Feng},
  title = {RATE: A model-based testing approach that combines model refinement and test execution},
  journal = {SOFTWARE TESTING VERIFICATION & RELIABILITY},
  year = {2022},
  number = {Art. n. 1835},
  pages = {1--34},
  doi = {https://doi.org/10.1002/stvr.1835}
}
Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene, Patrizia Scandurra Compositional Simulation of ASM for Safety Critical Systems

[Abstract] [BibTeX]

 2022 International Conference on Formal Aspects of Component Software (FACS)  Conference  
Abstract: Model-based simulation is nowadays an accepted practice for reliable prototyping of system behavior. To keep requirements complexity under control, system components are specified by separate models, validated and verified in isolation from the rest, but models have to be subsequently integrated and validated as a whole. For this reason, engines for orchestrated simulation of separate models are extremely useful. In this paper, we present a compositional simulation technique for managing the co-execution of Abstract State Machines (ASMs) communicating through I/O events. The proposed method allows the co-simulation of ASM models of separate subsystems of a Discrete Event System in a straight-through processing manner according to a predefined orchestration schema. We also present our experience in applying and validating the proposed technique in the context of the MVM (Mechanical Ventilator Milano) system, a mechanical lung ventilator that has been designed, successfully certified, and deployed during the COVID-19 pandemic.
BibTeX:
Andrea Bombarda, Silvia Bonfanti, Martina De Sanctis, Angelo Gargantini, Patrizio Pelliccione, Elvinia Riccobene, Patrizia Scandurra Towards an Evaluation Framework for Autonomous Systems

[Abstract] [BibTeX]

 2022 International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS)  Conference  
Abstract: Despite the active and proficuous research in autonomous and self-adaptive systems of the last years, an evaluation framework to assess abilities related to adaption and to provide guidance to make a system smarter is still missing. In this paper, we perform the first steps towards an evaluation framework for autonomous systems to (i) make an assessment of a system from the perspective of its capacity to adapt and learn over time to handle new and unexpected conditions, (ii) explore and identify the possiblepathways of improvement of the smart abilities (e.g., decisional autonomy, adaptability, perception, interaction, etc.) of a system, (iii) make a re-assessment when the improvement has been performed.
BibTeX:
Bombarda, Andrea; Bonfanti, Silvia; Galbiati, Cristiano; Gargantini, Angelo; Pelliccione, Patrizio; Riccobene, Elvinia; Wada, Masayuki Guidelines for the development of a critical software under emergency

[Abstract] [BibTeX]

 2022 Information and Software Technology  article DOI  
Abstract: 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.
BibTeX: 
@article{10446_222609,
title = {Guidelines for the development of a critical software under emergency},
journal = {Information and Software Technology},
volume = {152},
pages = {107061},
year = {2022},
issn = {0950-5849},
doi = {https://doi.org/10.1016/j.infsof.2022.107061},
url = {https://www.sciencedirect.com/science/article/pii/S0950584922001707},
author = {Andrea Bombarda and Silvia Bonfanti and Cristiano Galbiati and Angelo Gargantini and Patrizio Pelliccione and Elvinia Riccobene and Masayuki Wada},
keywords = {Safety–critical systems development, Software certification, Lessons learned, Guidelines, Healthcare},
}
Arcaini, P., Bombarda, A., Bonfanti, S., Gargantini, A., Gamba, D. and Pedercicni, R. Robustness assessment and improvement of a neural network for blood oxygen pressure estimation

[Abstract] [BibTeX]

 2022 IEEE Conference on Software Testing, Verification and Validation (ICST), pp. 312-322  conference DOI  
Abstract: Neural networks have been widely applied for performing tasks in critical domains, such as, for example, the medical domain; their robustness is, therefore, important to be guaranteed. In this paper, we propose a robustness definition for neural networks used for regression, by tackling some of the problems of existing robustness definitions. First of all, by following recent works done for classification problems, we propose to define the robustness of networks used for regression w.r.t. alterations of their input data that can happen in reality. Since different alteration levels are not always equally probable, the robustness definition is parameterized with the probability distribution of the alterations. The error done by this type of networks is quantifiable as the difference between the estimated value and the expected value; since not all the errors are equally critical, the robustness definition is also parameterized with a “tolerance” function that specifies how the error is tolerated. The current work has been motivated by the collaboration with the industrial partner that has implemented a medical sensor employing a Multilayer Perceptron for the estimation of the blood oxygen pressure. After having computed the robustness for the case study, we have successfully applied three techniques to improve the network robustness: data augmentation with recombined data, data augmentation with altered data, and incremental learning. All the techniques have proved to contribute to increasing the robustness, though in different ways.
BibTeX: 
@conference{10446_222608,
	author = {Arcaini, Paolo and Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo Michele and Gamba, Daniele and Pedercini, Rita},
	title = {Robustness assessment and improvement of a neural network for blood oxygen pressure estimation},
	year = {2022},
	publisher = {IEEE},
	address = {Piscataway},
	booktitle = {2022 IEEE Conference on Software Testing, Verification and Validation (ICST)},
	doi = {10.1109/ICST53961.2022.00040},
	isbn = {978-1-6654-6679-0},	
	pages = {312--322},
	organization ={IEEE}
}
Bombarda, A., Bonfanti, S. and Gargantini, A. Automatic Test Generation with ASMETA for the Mechanical Ventilator Milano Controller

[Abstract] [BibTeX]

 2022 Testing Software and Systems. ICTSS 2021, pp. 65-72  conference DOI  
Abstract: 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.
BibTeX: 
@conference{10446_202114,
	author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo Michele},
	title = {Automatic test generation with ASMETA for the Mechanical Ventilator Milano controller},
	year = {2022},
	publisher = {Springer},
	address = {Cham},
	volume = {13045},
	booktitle = {Testing Software and Systems. ICTSS 2021},
	doi = {10.1007/978-3-031-04673-5_5},
	isbn = {978-3-031-04672-8},	
	pages = {65--72}
}
Bombarda, A., Bonfanti, S., Gargantini, A. and Riccobene, E. Extending ASMETA with Time Features

[BibTeX]

 2021 Vol. 12709 Rigorous State-Based Methods, pp. 105-111  conference DOI  
BibTeX: 
@conference{10446_185264,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo and Riccobene, Elvinia},
  title = {Extending ASMETA with Time Features},
  booktitle = {Rigorous State-Based Methods},
  publisher = {Springer},
  year = {2021},
  volume = {12709},
  pages = {105--111},
  doi = {https://doi.org/10.1007/978-3-030-77543-8_8}
}
Bonfanti, S., Riccobene, E. and Scandurra, P. A Runtime Safety Enforcement Approach by Monitoring and Adaptation

[BibTeX]

 2021 Vol. 12857 Software Architecture, 15th European Conference, ECSA 2021, Virtual Event, Sweden, September 13-17, 2021, Proceedings, pp. 20-36  conference DOI  
BibTeX: 
@conference{10446_190932,
  author = {Bonfanti, Silvia and Riccobene, Elvinia and Scandurra, Patrizia},
  title = {A Runtime Safety Enforcement Approach by Monitoring and Adaptation},
  booktitle = {Software Architecture, 15th European Conference, ECSA 2021, Virtual Event, Sweden, September 13-17, 2021, Proceedings},
  publisher = {Springer Nature},
  year = {2021},
  volume = {12857},
  pages = {20--36},
  doi = {https://doi.org/10.1007/978-3-030-86044-8_2}
}
Arcaini, P., Bombarda, A., Bonfanti, S. and Gargantini, A.M. Efficient Computation of Robustness of Convolutional Neural Networks

[BibTeX]

 2021 IEEE International Conference on Artificial Intelligence Testing (AITest), pp. 21-28  conference DOI  
BibTeX: 
@conference{10446_197120,
  author = {Arcaini, Paolo and Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo Michele},
  title = {Efficient Computation of Robustness of Convolutional Neural Networks},
  booktitle = {IEEE International Conference on Artificial Intelligence Testing (AITest)},
  publisher = {Institute of Electrical and Electronics Engineers Inc.},
  year = {2021},
  pages = {21--28},
  doi = {https://doi.org/10.1109/AITEST52744.2021.00015}
}
Bombarda, A., Bonfanti, S., Gargantini, A.M. and Riccobene, E. Developing a Prototype of a Mechanical Ventilator Controller from Requirements to Code with ASMETA

[BibTeX]

 2021 ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Vol. 349Proceedings First Workshop on Applicable Formal Methods, pp. 13-29 		 conference DOI  
BibTeX: 
@conference{10446_197122,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo Michele and Riccobene, Elvinia},
  title = {Developing a Prototype of a Mechanical Ventilator Controller from Requirements to Code with ASMETA},
  booktitle = {Proceedings First Workshop on Applicable Formal Methods},
  journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},
  publisher = {Open Publishing Association},
  year = {2021},
  volume = {349},
  pages = {13--29},
  doi = {https://doi.org/10.4204/EPTCS.349.2}
}
Bombarda, A., Bonfanti, S., Galbiati, C., Gargantini, A.M., Pelliccione, P., Riccobene, E. and Wada, M. Lessons Learned from the Development of a Mechanical Ventilator for COVID-19

[Abstract] [BibTeX]

 2021 IEEE 32nd International Symposium on Software Reliability Engineering, pp. 24-35  conference DOI  
Abstract: During the COVID-19 pandemic, many researchers all over the world have offered their time and competencies to face the heavy consequences of the disease. This is the case of a group of physicists, engineers, and physicians that around the middle of March 2020 started to develop a simplified mechanical lung ventilator, called MVM (Mechanical Ventilator Milano), to answer the high request of ventilators for Acute Respiratory Distress Syndrome (ARDS) in intensive care units. A prototype was ready in around one month. Since medical software malfunctions can lead to injuries or death of patients, before marketing MVM ventilators and distributing them in hospitals, software certification in accordance with the IEC 62304 standard was mandatory to guarantee system reliability. The team was then complemented by computer scientists specifically devoted to this task. The software reengineering process, which lasted around two months from the end of the prototype, brought to a strong re-implementation of the device software components, which involved all the stakeholders in a continuous integration setting. In this paper, we report the experience of the MVM control SW re-engineering necessary to show evidence that the SW adheres to the standards and to consequently obtain the certification. We share results and lessons learned from this social project, where more than 100 volunteer researchers worked towards software certification at the extreme of their strength to get a real device finished in a rush since strongly required to support physicians in treating COVID-19 patients.
BibTeX: 
@conference{10446_202108.3,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Galbiati, Cristiano and Gargantini, Angelo Michele and Pelliccione, Patrizio and Riccobene, Elvinia and Wada, Masayuki},
  title = {Lessons Learned from the Development of a Mechanical Ventilator for COVID-19},
  booktitle = {IEEE 32nd International Symposium on Software Reliability Engineering},
  year = {2021},
  pages = {24--35},
  doi = {https://doi.org/10.1109/ISSRE52982.2021.00016}
}
Bonfanti, S., Bombarda, A., Gargantini, A.M., Riccobene, E. and Pelliccione, P. Il successo di MVM, un progetto social e internazionale per realizzare un ventilatore polmonare

[BibTeX]

 2021 IL GIORNALE DELL'INGEGNERE  article  
BibTeX: 
@article{10446_202112.1,
  author = {Bonfanti, Silvia and Bombarda, Andrea and Gargantini, Angelo Michele and Riccobene, Elvinia and Pelliccione, Patrizio},
  title = {Il successo di MVM, un progetto social e internazionale per realizzare un ventilatore polmonare},
  journal = {IL GIORNALE DELL'INGEGNERE},
  year = {2021}
}
Bombarda, A., Bonfanti, S. and Gargantini, A.M. Automatic test generation with ASMETA for the Mechanical Ventilator Milano controller

[BibTeX]

 2021 Testing Software and Systems, pp. 1-7  conference  
BibTeX: 
@conference{10446_202114.3,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo Michele},
  title = {Automatic test generation with ASMETA for the Mechanical Ventilator Milano controller},
  booktitle = {Testing Software and Systems},
  year = {2021},
  pages = {1--7}
}
Gargantini, A. and Bonfanti, S. Comparison of Algorithms to Measure a Psychophysical Threshold using Digital Applications: The Stereoacuity Case Study

[Abstract][BibTeX]

 2021 Proceedings of the 14th International Joint Conference on Biomedical Engineering Systems and Technologies. Volume 5: HEALTHINF, pp. 78-86  conference DOI  
Abstract: The use of digital applications to perform psychophysical measurements led to the introduction of algorithms to guide the users in test execution. In this paper we show three algorithms, two already well known: StrictStaircase and PEST, and a new one that we propose: PEST3. All the algorithms aim at estimating the level of a psychophysical capability by performing a sequence of simple tests; starting from initial level N, the test is executed until the target level is reached. They differ in the choice of the next steps in the sequences and the stopping condition. We have applied the algorithms to the stereoacuity case study and we have compared them by answering a set of research questions. Finally, we provide guidelines to choose the best algorithm based on the test goal. We found that while StrictStaircase provides optimal results, it requires the largest number of steps and this may hinder its use; PEST3 can overcome these limits without compromising the final results.
BibTeX: 
@conference{10446_176598,
  author = {Gargantini, Angelo and Bonfanti, Silvia},
  title = {Comparison of Algorithms to Measure a Psychophysical Threshold using Digital Applications: The Stereoacuity Case Study},
  booktitle = {Proceedings of the 14th International Joint Conference on Biomedical Engineering Systems and Technologies. Volume 5: HEALTHINF},
  publisher = {Science and Technology Publications},
  year = {2021},
  pages = {78--86},
  doi = {https://doi.org/10.5220/0010204000780086}
}
Abba, A. and Accorsi, C. and Agnes, P. and Alessi, E. and Amaudruz, P. and Bonfanti, S. et al The novel Mechanical Ventilator Milano for the COVID-19 pandemic

[Abstract][BibTeX]

 2021 PHYSICS OF FLUIDS
Vol. 33, pp. 1-11 		 article DOI  
Abstract: This paper presents the Mechanical Ventilator Milano (MVM), a novel intensive therapy mechanical ventilator designed for rapid, large-scale, low-cost production for the COVID-19 pandemic. Free of moving mechanical parts and requiring only a source of compressed oxygen and medical air to operate, the MVM is designed to support the long-term invasive ventilation often required for COVID-19 patients and operates in pressure-regulated ventilation modes, which minimize the risk of furthering lung trauma. The MVM was extensively tested against ISO standards in the laboratory using a breathing simulator, with good agreement between input and measured breathing parameters and performing correctly in response to fault conditions and stability tests. The MVM has obtained Emergency Use Authorization by U.S. Food and Drug Administration (FDA) for use in healthcare settings during the COVID-19 pandemic and Health Canada Medical Device Authorization for Importation or Sale, under Interim Order for Use in Relation to COVID-19. Following these certifications, mass production is ongoing and distribution is under way in several countries. The MVM was designed, tested, prepared for certification, and mass produced in the space of a few months by a unique collaboration of respiratory healthcare professionals and experimental physicists, working with industrial partners, and is an excellent ventilator candidate for this pandemic anywhere in the world.
BibTeX: 
@article{10446_177978,
  author = {Abba, A. and Accorsi, C. and Agnes, P. and Alessi, E. and Amaudruz, P. and Bonfanti, S. et al},
  title = {The novel Mechanical Ventilator Milano for the COVID-19 pandemic},
  journal = {PHYSICS OF FLUIDS},
  year = {2021},
  volume = {33},
  pages = {1--11},
  doi = {https://doi.org/10.1063/5.0044445}
}
Bonfanti, S., Gargantini, A., Esposito, G., Facchin, A., Maffioletti, M. and Maffioletti, S. Evaluation of stereoacuity with a digital mobile application

[Abstract][BibTeX]

 2021 GRAEFE'S ARCHIVE FOR CLINICAL AND EXPERIMENTAL OPHTHALMOLOGY, pp. 1-6  article DOI  
Abstract: Purpose: Stereopsis is a fundamental skill in human vision and visual actions. There are many ways to test and quantify stereoacuity: traditional paper and new digital applications are both valid ways to test the stereoacuity. The aim of this study is to compare the results obtained using standard tests and the new Stereoacuity Test App developed by the University of Bergamo. Methods: A group of 497 children (272 males), aged between 6 and 11 years old, were tested using different tests for the quantification of stereopsis at near. These tests were TNO, Weiss EKW, and the new developed Stereoacuity Test App. Results: A one-way repeated measure ANOVA showed that the three tests give different thresholds of stereoacuity (p < 0.0001). Post hoc analyses with Bonferroni correction showed that all tests showed different thresholds (p < 0.0001). The lower threshold was obtained by Titmus Stereo Test followed by Stereoacuity App, Weiss MKW, and TNO. Conclusion: The stereoacuity based on global stereopsis showed that the better values were obtained in order by Stereoacuity Test App, TNO, and Weiss EKW. However, the clinical significance of their values is similar. The new digital test showed a greater compliance by the child, showing itself in tune with the digital characteristics of today's children. Keywords: Anaglyph colors; Binocular vision; Digital stereotest; Global stereopsis; Randot stereotest; Stereo threshold; Stereoacuity.
BibTeX: 
@article{10446_181058,
  author = {Bonfanti, Silvia and Gargantini, Angelo and Esposito, Gabriele and Facchin, Alessio and Maffioletti, Marta and Maffioletti, Silvio},
  title = {Evaluation of stereoacuity with a digital mobile application},
  journal = {GRAEFE'S ARCHIVE FOR CLINICAL AND EXPERIMENTAL OPHTHALMOLOGY},
  year = {2021},
  pages = {1--6},
  doi = {https://doi.org/10.1007/s00417-021-05195-z}
}
Arcaini, P., Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E. and Scandurra, P. The ASMETA Approach to Safety Assurance of Software Systems

[Abstract][BibTeX]

 2021
Vol. 12750Logic, Computation and Rigorous Methods. Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday, pp. 215-238 		 inbook DOI  
Abstract: Safety-critical systems require development methods and processes that lead to provably correct systems in order to prevent catastrophic consequences due to system failure or unsafe operation. The use of models and formal analysis techniques is highly demanded both at design-time, to guarantee safety and other desired qualities already at the early stages of the system development, and at runtime, to address requirements assurance during the system operational stage. In this paper, we present the modeling features and analysis techniques supported by ASMETA (ASM mETAmodeling), a set of tools for the Abstract State Machines formal method. We show how the modeling and analysis approaches in ASMETA can be used during the design, development, and operation phases of the assurance process for safety-critical systems, and we illustrate the advantages of integrated use of tools as that provided by ASMETA.
BibTeX: 
@inbook{10446_184707,
  author = {Arcaini, Paolo and Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo and Riccobene, Elvinia and Scandurra, Patrizia},
  title = {The ASMETA Approach to Safety Assurance of Software Systems},
  booktitle = {Logic, Computation and Rigorous Methods. Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday},
  publisher = {Springer},
  year = {2021},
  volume = {12750},
  pages = {215--238},
  doi = {https://doi.org/10.1007/978-3-030-76020-5_13}
}
Bombarda, A., Bonfanti, S., Gargantini, A. and Riccobene, E. Extending ASMETA with Time Features

[Abstract][BibTeX]

 2021
Vol. 12709Rigorous State-Based Methods, pp. 105-111 		 conference DOI  
Abstract: ASMs and the ASMETA framework can be used to model and analyze a variety of systems, and many of them rely on time constraints. In this paper, we present the ASMETA extension to deal with model time features.
BibTeX: 
@conference{10446_185264,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo and Riccobene, Elvinia},
  title = {Extending ASMETA with Time Features},
  booktitle = {Rigorous State-Based Methods},
  publisher = {Springer},
  year = {2021},
  volume = {12709},
  pages = {105--111},
  doi = {https://doi.org/10.1007/978-3-030-77543-8_8}
}
Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E. and Scandurra, P. Addressing usability in a formal development environment

[Abstract][BibTeX]

 2020
Vol. 12232Formal Methods. FM 2019 International Workshops, pp. 61-76 		 conference DOI  
Abstract: Even though the formal method community tends to overlook the problem, formal methods are sometimes difficult to use and not accessible to average users. On one hand, this is due to the intrinsic complexity of the methods and, therefore, some level of required expertise is unavoidable. On the other hand, however, the methods are sometimes hard to use because of lack of a user-friendly tool support. In this paper, we present our experience in addressing usability when developing a framework for the Abstract State Machines (ASMs) formal method. In particular, we discuss how we enhanced modeling, validation, and verification activities of an ASM-based development process. We also provide a critical review of which of our efforts have been more successful as well as those that have not obtained the results we were expecting. Finally, we outline other directions that we believe could further lower the adoption barrier of the method.
BibTeX: 
@conference{10446_164546,
  author = {Arcaini, P. and Bonfanti, S. and Gargantini, A. and Riccobene, E. and Scandurra, P.},
  title = {Addressing usability in a formal development environment},
  booktitle = {Formal Methods. FM 2019 International Workshops},
  publisher = {Springer},
  year = {2020},
  volume = {12232},
  pages = {61--76},
  doi = {https://doi.org/10.1007/978-3-030-54994-7_6}
}
Arcaini, P., Bombarda, A., Bonfanti, S. and Gargantini, A. Dealing with Robustness of Convolutional Neural Networks for Image Classification

[Abstract][BibTeX]

 2020 2020 IEEE International Conference On Artificial Intelligence Testing (AITest), pp. 7-14  conference DOI  
Abstract: 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, e.g., 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 w.r.t. 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.
BibTeX: 
@conference{10446_164544,
  author = {Arcaini, Paolo and Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo},
  title = {Dealing with Robustness of Convolutional Neural Networks for Image Classification},
  booktitle = {2020 IEEE International Conference On Artificial Intelligence Testing (AITest)},
  publisher = {IEEE},
  year = {2020},
  pages = {7--14},
  doi = {https://doi.org/10.1109/AITEST49225.2020.00009}
}
Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E. and Scandurra, P. Modelling an Automotive Software-Intensive System with Adaptive Features Using ASMETA

[Abstract][BibTeX]

 2020
Vol. 12071Rigorous State-Based Methods, pp. 302-317 		 conference DOI  
Abstract: In the context of automotive domain, modern control systems are software-intensive and have adaptive features to provide safety and comfort. These software-based features demand software engineering approaches and formal methods that are able to guarantee correct operation, since malfunctions may cause harm/damage. Adaptive Exterior Light and the Speed Control Systems are examples of software-intensive systems that equip modern cars. We have used the Abstract State Machines to model the behaviour of both control systems. Each model has been developed through model refinement, following the incremental way in which functional requirements are given. We used the ASMETA tool-set to support the simulation of the abstract models, their validation against the informal requirements, and the verification of behavioural properties. In this paper, we discuss our modelling, validation and verification strategies, and the results (in terms of features addressed and not) of our activities. In particular, we provide insights on how we addressed the adaptive features (the adaptive high beam headlights and the adaptive cruise control) by explicitly modelling their software control loops according to the MAPE-K (Monitor-Analyse-Plan-Execute over a shared Knowledge) reference control model for self-adaptive systems.
BibTeX: 
@conference{10446_164542,
  author = {Arcaini, P. and Bonfanti, S. and Gargantini, A. and Riccobene, E. and Scandurra, P.},
  title = {Modelling an Automotive Software-Intensive System with Adaptive Features Using ASMETA},
  booktitle = {Rigorous State-Based Methods},
  publisher = {Springer Nature Switzerland},
  year = {2020},
  volume = {12071},
  pages = {302--317},
  doi = {https://doi.org/10.1007/978-3-030-48077-6_25}
}
Bonfanti, S., Gargantini, A. and Mashkoor, A. Design and validation of a C++ code generator from Abstract State Machines specifications

[Abstract][BibTeX]

 2020 JOURNAL OF SOFTWARE
Vol. 32, pp. 1-25 		 article DOI  
Abstract: According to best practices of model-driven engineering, the implementation of a system should be obtained from its model through a systematic model-to-code transformation. We present in this paper a methodology supported by the Asm2C++ tool, which allows the users to generate C++ code from abstract state machine models. Thanks to Asm2C++, the implementation is generated in a seamless manner with an assurance of potential bug freeness of the generated code. Following the same approach, model-based testing suggests deriving also (unit) tests from abstract models. We extend the Asm2C++ tool such that it can automatically produce unit tests for the generated code. Abstract test sequences, either generated randomly or through model checking, are translated to concrete C++ unit tests using the Boost library. In a similar manner, also, scenarios are generated in a behavior-driven development (BDD) approach. To guarantee the correctness of the transformation process, we define a mechanism to test the correctness of the model-to-code transformation with respect to two main criteria: syntactical correctness and semantic correctness, which is based on the definition of conformance between the specification and the code. Using this approach, we have devised a process able to test the generated code by reusing unit tests. The process has been used to validate our model-to-code transformations.
BibTeX: 
@article{10446_150836,
  author = {Bonfanti, S. and Gargantini, A. and Mashkoor, A.},
  title = {Design and validation of a C++ code generator from Abstract State Machines specifications},
  journal = {JOURNAL OF SOFTWARE},
  year = {2020},
  volume = {32},
  pages = {1--25},
  doi = {https://doi.org/10.1002/smr.2205}
}
Bombarda, A., Bonfanti, S., Gargantini, A., Radavelli, M., Duan, F. and Lei, Y. Combining Model Refinement and Test Generation for Conformance Testing of the IEEE PHD Protocol Using Abstract State Machines

[Abstract][BibTeX]

 2019
Vol. 11812Testing Software and Systems: 31st IFIP WG 6.1 International Conference, ICTSS 2019, Paris, France, October 15–17, 2019, Proceedings, pp. 67-85 		 conference DOI  
Abstract: 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.
BibTeX: 
@conference{10446_150840,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo and Radavelli, Marco and Duan, Feng and Lei, Yu},
  title = {Combining Model Refinement and Test Generation for Conformance Testing of the IEEE PHD Protocol Using Abstract State Machines},
  booktitle = {Testing Software and Systems: 31st IFIP WG 6.1 International Conference, ICTSS 2019, Paris, France, October 15–17, 2019, Proceedings},
  publisher = {Springer},
  year = {2019},
  volume = {11812},
  pages = {67--85},
  doi = {https://doi.org/10.1007/978-3-030-31280-0_5}
}
Bombarda, A., Bonfanti, S. and Gargantini, A. Developing Medical Devices from Abstract State Machines to Embedded Systems: A Smart Pill Box Case Study

[Abstract][BibTeX]

 2019
Vol. 11771Software Technology: Methods and Tools: 51st International Conference, TOOLS 2019, Innopolis, Russia, October 15–17, 2019, Proceedings, pp. 89-103 		 conference DOI  
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 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 code. The process is applied to the smart pill box case study. Starting from the ASM model, we generate 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.
BibTeX: 
@conference{10446_150814,
  author = {Bombarda, Andrea and Bonfanti, Silvia and Gargantini, Angelo},
  title = {Developing Medical Devices from Abstract State Machines to Embedded Systems: A Smart Pill Box Case Study},
  booktitle = {Software Technology: Methods and Tools: 51st International Conference, TOOLS 2019, Innopolis, Russia, October 15–17, 2019, Proceedings},
  publisher = {Springer Nature},
  year = {2019},
  volume = {11771},
  pages = {89--103},
  doi = {https://doi.org/10.1007/978-3-030-29852-4_7}
}
Bonfanti, S., Gargantini, A. and Mashkoor, A. Validation of transformation from abstract state machine models to C++ code

[Abstract][BibTeX]

 2018 Vol. 11146Testing Software and Systems. 30th IFIP WG 6.1 International Conference, ICTSS 2018, Cádiz, Spain, October 1-3, 2018, Proceedings, pp. 17-32  conference DOI  
Abstract: The automatic transformation of models to code is one of the most important cornerstones in the model-driven engineering paradigm. Starting from system models, users are able to automatically generate machine code in a seamless manner with an assurance of potential bug freeness of the generated code. Asm2C++ [4] is the tool that transforms Abstract State Machine models to code. However, no validation activities have been performed in the past to guarantee the correctness of the transformation process. In this paper, we define a mechanism to test the correctness of the model-to-code transformation with respect to two main criteria: syntactical correctness and semantic correctness, which is based on the definition of conformance between the specification and the code. Using this approach, we have devised a process able to test the generated code by reusing unit tests. Coverage measures give a user the confidence that the generated code has the same behavior as specified by the ASM model.
BibTeX: 
@conference{10446_131417,
  author = {Bonfanti, Silvia and Gargantini, Angelo and Mashkoor, Atif},
  title = {Validation of transformation from abstract state machine models to C++ code},
  booktitle = {Testing Software and Systems. 30th IFIP WG 6.1 International Conference, ICTSS 2018, Cádiz, Spain, October 1-3, 2018, Proceedings},
  publisher = {Springer},
  year = {2018},
  volume = {11146},
  pages = {17--32},
  doi = {https://doi.org/10.1007/978-3-319-99927-2_2}
}
Bonfanti, S., Gargantini, A. and Mashkoor, A. Generation of behavior-driven development C++ tests from abstract state machine scenarios

[Abstract][BibTeX]

 2018 Vol. 929New Trends in Model and Data Engineering. MEDI 2018 International Workshops, DETECT, MEDI4SG, IWCFS, REMEDY, Marrakesh, Morocco, October 24–26, 2018, Proceedings, pp. 146-152  conference DOI  
Abstract: In this paper, we present the AsmetaVBDD tool that automatically translates the scenarios written in the AValLa language (used by the asmeta validator (AsmetaV)) into Behavior-Driven Development scenarios for C++.
BibTeX: 
@conference{10446_131419,
  author = {Bonfanti, Silvia and Gargantini, Angelo and Mashkoor, Atif},
  title = {Generation of behavior-driven development C++ tests from abstract state machine scenarios},
  booktitle = {New Trends in Model and Data Engineering. MEDI 2018 International Workshops, DETECT, MEDI4SG, IWCFS, REMEDY, Marrakesh, Morocco, October 24–26, 2018, Proceedings},
  publisher = {Springer},
  year = {2018},
  volume = {929},
  pages = {146--152},
  doi = {https://doi.org/10.1007/978-3-030-02852-7_13}
}
Bonfanti, S. and Gargantini, A. Stereo Digital Displays for Diagnosis and Treatment of Amblyopia

[Abstract] [BibTeX]

 2018 Nova Science Publisher, Advances in Health and Disease. Vol. 8, pp. 229-249  inbook URL  
Abstract: In this chapter, we are going to show how we use the stereo digital displays for the diagnosis and treatment of amblyopia. In the last years, many technologies, that we call stereo digital displays, have been introduced to provide the 3D illusion: 3D active, anaglyph and tethered/mobile Virtual Reality (VR). Usually, they are used for recreational purposes, but the idea underlying can be applied to medical field. The operating principle behind these technologies is based on the transmission of two images simultaneously, one per each eye. This dichoptic vision can be exploited for the diagnosis and treatment of amblyopia. In particular, we have developed a random dot test using 3D active, anaglyph and mobile VR visors for the diagnosis of amblyopia. While for the treatment we have developed ad hoc applications. The applications developed are mainly games and entertainment applications, that through the dichoptic vision stimulate the amblyopic eye without the use of traditional therapies. Particular attention has been paid to the cost of the devices. For this reason, now we are focusing on cheaper solutions which are anaglyph and mobile VR.
BibTeX: 
@inbook{10446_131512,
  author = {Bonfanti, Silvia and Gargantini, Angelo},
  title = {Stereo Digital Displays for Diagnosis and Treatment of Amblyopia},
  booktitle = {Advances in Health and Disease. Vol. 8},
  publisher = {Nova Biomedical},
  year = {2018},
  pages = {229--249}
}
Bonfanti, S., Gargantini, A. and Mashkoor, A. AsmetaA: Animator for Abstract State Machines

[Abstract] [BibTeX]

 2018 International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z  conference DOI URL 
Abstract: In this paper, we present AsmetaA – a graphical animator for Abstract State Machines integrated within the ASMETA framework. The execution of formal specifications through animation provides several advantages, e.g., it provides an immediate feedback about system behavior, it helps understand system evolution, and it increases the overall acceptability of formal methods.
BibTeX: 
@conference{abz2018,
  author = {Bonfanti, Silvia and Gargantini, Angelo and Mashkoor, Atif},
  title = {AsmetaA: Animator for Abstract State Machines},
  booktitle = {International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z},
  year = {2018}
  doi = {https://doi.org/10.1007/978-3-319-91271-4_25}
  url={https://link.springer.com/chapter/10.1007%2F978-3-319-91271-4_25}
}
Bonfanti, S., Gargantini, A. and Mashkoor, A. Generation of C++ Unit Tests from Abstract State Machines Specifications

[Abstract] [BibTeX]

 2018 14th Workshop on Advances in Model Based Testing (A-MOST), ICST 2018, Vasteras, Sweden  conference DOI URL 
Abstract: According to best practices of model-driven engineering, the implementation of a system should be obtained from its model through a systematic model-to-code transformation. Following the same approach, model-based testing suggests deriving also (unit) tests from abstract models. Previously, we have presented ASM2C++ -- a tool that translates Abstract State Machines (ASMs) to C++ code. In this paper, we extend the ASM2C++ tool such that it can now automatically produce unit tests for the generated code. Abstract test sequences, either generated randomly or through model checking, are translated to concrete C++ unit tests using the BOOST library. We also present some experiments that prove the feasibility of the proposed approach.
BibTeX: 
@conference{amost2018,
  author = {Bonfanti, Silvia and Gargantini, Angelo and Mashkoor, Atif},
  title = {Generation of C++ Unit Tests from Abstract State Machines Specifications},
  booktitle = {14th Workshop on Advances in Model Based Testing (A-MOST), ICST 2018, Vasteras, Sweden},
  year = {2018}
  doi = {https://doi.org/10.1109/ICSTW.2018.00049}
  url={https://ieeexplore.ieee.org/document/8411752/}
}
}
Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A. and Riccobene, E. Integrating formal methods into medical software development: The ASM approach

[Abstract] [BibTeX]

 2018 Science of Computer Programming
Vol. 158, pp. 148 - 167 		 article DOI URL 
Abstract: Medical devices are safety-critical systems since their malfunctions can seriously compromise human safety. Correct operation of a medical device depends upon the controlling software, whose development should adhere to certification standards. However, these standards provide general descriptions of common software engineering activities without any indication regarding particular methods and techniques to assure safety and reliability. This paper discusses how to integrate the use of a formal approach into the current normative for the medical software development. The rigorous process is based on the Abstract State Machine (ASM) formal method, its refinement principle, and model analysis approaches the method supports. The hemodialysis machine case study is used to show how the ASM-based design process covers most of the engineering activities required by the related standards, and provides rigorous approaches for medical software validation and verification.
BibTeX: 
@article{ARCAINI2018148,
  author = {Paolo Arcaini and Silvia Bonfanti and Angelo Gargantini and Atif Mashkoor and Elvinia Riccobene},
  title = {Integrating formal methods into medical software development: The ASM approach},
  journal = {Science of Computer Programming},
  year = {2018},
  volume = {158},
  pages = {148 - 167},
  note = {Abstract State Machines, Alloy, B, TLA, VDM and Z (ABZ 2016)},
  url = {http://www.sciencedirect.com/science/article/pii/S0167642317301430},
  doi = {http://doi.org/10.1016/j.scico.2017.07.003}
}
Bonfanti, S., Gargantini, A. and Mashkoor, A. A systematic literature review of the use of formal methods in medical software systems

[Abstract] [BibTeX]

 2018 Journal of Software: Evolution and Process  article DOI URL 
Abstract: Abstract The use of formal methods is often recommended to guarantee the provision of necessary services and to assess the correctness of critical properties, such as functional safety, cybersecurity, and reliability, in medical and health care devices. In the past, several formal and rigorous methods have been proposed and consequently applied for trustworthy development of medical software and systems. In this paper, we perform a systematic literature review on the available state of the art in this domain. We collect the relevant literature on the use of formal methods for modeling, design, development, verification, and validation of software‐intensive medical systems. We apply standard systematic literature review techniques and run several queries in well‐known repositories to obtain information that can be useful for people who are either already working in this field or planning to start. Our study covers both quantitative and qualitative aspects of the subject.
BibTeX: 
@article{doi:10.1002/smr.1943,
  author = {Silvia Bonfanti and Angelo Gargantini and Atif Mashkoor},
  title = {A systematic literature review of the use of formal methods in medical software systems},
  journal = {Journal of Software: Evolution and Process},
  year = {2018},
  url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/smr.1943},
  doi = {http://doi.org/10.1002/smr.1943}
}
Bonfanti, S., Carissoni, M., Gargantini, A. and Mashkoor, A. Asm2C++: A Tool for Code Generation from Abstract State Machines to Arduino

[Abstract] [BibTeX]

 2017 NASA Formal Methods, pp. 295-301  conference DOI URL 
Abstract: This paper presents Asm2C++, a tool that automatically generates executable C++ code for Arduino from a formal specification given as Abstract State Machines (ASMs). The code generation process follows the model-driven engineering approach, where the code is obtained from a formal abstract model by applying certain transformation rules. The translation process is highly configurable in order to correctly integrate the underlying hardware. The advantage of the Asm2C++ tool is that it is part of the Asmeta framework that allows to analyze, verify, and validate the correctness of a formal model.
BibTeX: 
@conference{10.1007/978-3-319-57288-8_21,
  author = {Bonfanti, Silvia and Carissoni, Marco and Gargantini, Angelo and Mashkoor, Atif},
  title = {Asm2C++: A Tool for Code Generation from Abstract State Machines to Arduino},
  booktitle = {NASA Formal Methods},
  publisher = {Springer International Publishing},
  year = {2017},
  pages = {295--301},
  url = {https://doi.org/10.1007/978-3-319-57288-8_21},
  doi = {http://doi.org/10.1007/978-3-319-57288-8_21}
}
Bonfanti, S. and Gargantini, A. Amblyopia Rehabilitation by Games for Low-Cost Virtual Reality Visors

[Abstract] [BibTeX]

 2017 ICTs for Improving Patients Rehabilitation Research Techniques, pp. 116-125  conference DOI URL 
Abstract: Amblyopia is the partial or complete loss of vision in one eye (called lazy eye). It can be prevented by adequate treatment during the first years of young age. However, the classical therapy of eye patching suffers from a low compliance that can harm the treatment. To increase compliance, we have devised a system based on the combined use of low cost virtual reality visors, like the Google Cardboard, and ad hoc developed games for smartphones. Our system exploits the visor in order to send to the lazy eye an enhanced version of the gaming image while it sends to the normal eye a weakened version of the same image. In this way, the lazy eye must work more than the normal eye. We present here the principles, some issues we encountered, the integration of the games with a service that collects the data, and two games, namely a car racing and a tetris game.
BibTeX: 
@conference{10.1007/978-3-319-69694-2_11,
  author = {Bonfanti, Silvia and Gargantini, Angelo},
  title = {Amblyopia Rehabilitation by Games for Low-Cost Virtual Reality Visors},
  booktitle = {ICTs for Improving Patients Rehabilitation Research Techniques},
  publisher = {Springer International Publishing},
  year = {2017},
  pages = {116--125},
  url = {https://doi.org/10.1007/978-3-319-69694-2_11},
  doi = {http://doi.org/10.1007/978-3-319-69694-2_11}
}
Bonfanti, S., Centurelli, V., Riccobene, E. and Scandurra, P. The Female Contribution in Architecting a Set of Tools for a Formal Method: Role of Women in Software Architecture (Short Paper)

[Abstract] [BibTeX]

 2017 Proceedings of the 11th European Conference on Software Architecture: Companion Proceedings, pp. 12-15  conference DOI URL 
Abstract: This paper presents the female contribution on engineering a reference software architecture for ASMETA, a framework for an integrated use of tools developed around the Abstract State Machine formal method. Based on our experience in such a development project, we discuss how feminine mindset and skills can bring concrete advantages, but some disadvantages too, in the creative process of metamodeling, architecting and maintaining software.
BibTeX: 
@conference{Bonfanti:2017:FCA:3129790.3129823,
  author = {Bonfanti, Silvia and Centurelli, Valentina and Riccobene, Elvinia and Scandurra, Patrizia},
  title = {The Female Contribution in Architecting a Set of Tools for a Formal Method: Role of Women in Software Architecture (Short Paper)},
  booktitle = {Proceedings of the 11th European Conference on Software Architecture: Companion Proceedings},
  publisher = {ACM},
  year = {2017},
  pages = {12--15},
  url = {http://doi.acm.org/10.1145/3129790.3129823},
  doi = {http://doi.org/10.1145/3129790.3129823}
}
Esposito, G., Facchin, A., Maffioletti, M., Maffioletti, S., Gargantini, A., Bonfanti, S., Bonsignore, F. and Nucci, P. Behind optical factors in anisometropic aniseikonia

[Abstract] [BibTeX]

 2017 40th European Conference on Visual Perception  incollection  
Abstract: Aniseikonia is a binocular condition in which the apparent sizes of the images seen by the eyes are unequal. Aniseikonia is commonly associated with anisometropia, moreover the perceived size can be influenced by other factors such as spacing of retinal elements and some degree of perceptual factors. The aim of this study is to test the degree of aniseikonia in induced anisometropia by ophthalmic lenses (OL) and contact lenses (CL).We have measured aniseikonia using a new instrument in 52 isometropic participants inducing an anisometropia of +1.50,+3.00 and +4.50 dioptre with OL and CL. As expected, the results show that aniseikonia is larger for ophthalmic lenses; however it is different from zero when induced by CL. When induced by OL, the aniseikonia is larger than the value predicted by optical formula. Because there is great variability between subjects at baseline and in aniseikonia induced by lenses, there is some kind of perceptual influence on perceived aniseikonia. These results show that aniseikonia is not only influenced by the optical factor but there are more perceptual aspects as previously hypothesized.
BibTeX: 
@incollection{ECVP2017,
  author = {Gabriele Esposito and  Alessio Facchin and Marta Maffioletti and Silvio Maffioletti and Angelo Gargantini and Silvia Bonfanti and Francesco Bonsignore and Paolo Nucci},
  title = {Behind optical factors in anisometropic aniseikonia},
  booktitle = {40th European Conference on Visual Perception},
  publisher = {SAGE Journals},
  year = {2017}
}
Bonfanti, S. Rigorous Model-based Development of Programmable Electronic Medical Systems (PEMS): from Requirements to Code

[Abstract] [BibTeX]

 2017 School: Ph.D. in Engineering and applied sciences - Dottorato di ricerca in Ingegneria e scienze applicate  phdthesis  
Abstract: Programmable Electronic Medical Systems (PEMS) are safety-critical system. They have effects on people health and, in case of malfunctions, they can seriously compromise human safety. For this reason, the software installed on these devices must be guaranteed through rigorous processes to assure safety and reliability. Moreover, correct operation of a medical device depends upon the controlling software, whose development should adhere to certification standards. The rigorous process presented in this thesis is based on the Abstract State Machines (ASMs) formal method, a mathematically based technique for the specification, analysis and development of software systems. The ASM formal approach proposes an incremental life cycle model for software development based on model refinement. It covers the main software engineering activities (specification, validation, verification, conformance checking), and it is supported by a wide range of tools which are part of the Asmeta (ASM mETAmodeling) framework. In this thesis, the ASM development approach and its supporting Asmeta framework are used to propose a rigorous development process for PEMS. The final goal is to provide a process able to guarantee the development of correct and controllable systems in a correct and controllable way. The definition of this process has leaded to some improvements of the method, mainly regarding the textual and graphical notations, and the automatic code generation from models. A new rigorous notation, Unified Syntax for Abstract State Machine (UASM), has been defined to provide a stable language kernel for ASMs. Formal models are not widely used in practice, since they are considered difficult to develop and understand. For this reason, we here make a proposal of a tool for a graphical representation of ASM models in order to increase the readability. Moreover, we have devised a methodology to generate the desired source code from ASM models. The tool automatically translates the formal specification into the target code (C++ for Arduino in the present case) and it keeps true the system behavior and the properties verified during validation and verification. The hemodialysis machine and the stereoacuity test are used as real case studies to show the applicability and effectiveness of the ASM-based development process in the area of PEMS.
BibTeX: 
@phdthesis{PhdBonfanti,
  author = {Bonfanti, Silvia},
  title = {Rigorous Model-based Development of Programmable Electronic Medical Systems (PEMS): from Requirements to Code},
  school = {Ph.D. in Engineering and applied sciences - Dottorato di ricerca in Ingegneria e scienze applicate},
  year = {2017}
}
Arcaini, P., Bonfanti, S., Dausend, M., Gargantini, A., Mashkoor, A., Raschke, A., Riccobene, E., Scandurra, P. and Stegmaier, M. Unified Syntax for Abstract State Machines

[Abstract] [BibTeX]

 2016 Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 231-236  conference DOI URL 
Abstract: The paper presents our efforts in defining UASM, a unified syntax for Abstract State Machines (ASMs), based on the syntaxes of two of the main ASM frameworks, CoreASM and ASMETA, which have been adapted to accept UASM as input syntax of all their validation and verification tools.
BibTeX: 
@conference{10.1007/978-3-319-33600-8_14,
  author = {Arcaini, Paolo and Bonfanti, Silvia and Dausend, Marcel and Gargantini, Angelo and Mashkoor, Atif and Raschke, Alexander and Riccobene, Elvinia and Scandurra, Patrizia and Stegmaier, Michael},
  title = {Unified Syntax for Abstract State Machines},
  booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and Z},
  publisher = {Springer International Publishing},
  year = {2016},
  pages = {231--236},
  url = {https://doi.org/10.1007/978-3-319-33600-8_14},
  doi = {http://doi.org/10.1007/978-3-319-33600-8_14}
}
Arcaini, P., Bonfanti, S., Gargantini, A. and Riccobene, E. How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study

[Abstract] [BibTeX]

 2016 Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 344-359  conference DOI URL 
Abstract: Medical devices are nowadays more and more software dependent, and software malfunctioning can lead to injuries or death for patients. Several standards have been proposed for the development and the validation of medical devices, but they establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability.
BibTeX: 
@conference{10.1007/978-3-319-33600-8_30,
  author = {Arcaini, Paolo and Bonfanti, Silvia and Gargantini, Angelo and Riccobene, Elvinia},
  title = {How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study},
  booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and Z},
  publisher = {Springer International Publishing},
  year = {2016},
  pages = {344--359},
  url = {https://doi.org/10.1007/978-3-319-33600-8_30},
  doi = {http://doi.org/10.1007/978-3-319-33600-8_30}
}
Arcaini, P., Bonfanti, S., Gargantini, A. and Riccobene, E. Visual Notation and Patterns for Abstract State Machines

[Abstract] [BibTeX]

 2016 Software Technologies: Applications and Foundations, pp. 163-178  conference DOI URL 
Abstract: Formal models are a rigorous way to specify informal system requirements. However, they are not widely used in practice, since they are considered difficult to develop and understand. Visualization is often considered a good means for people to communicate and to get a common understanding. We here make a proposal of a visual notation for Abstract State Machines (ASMs), and we introduce visual trees that visualize ASM transition rules. In addition to these graphical components that are based only on the syntactical structure of the model, we also present visual patterns that permit to visualize part of the behavior of the machine. A tool is also available to graphically represent ASM models using the proposed notation.
BibTeX: 
@conference{10.1007/978-3-319-50230-4_12,
  author = {Arcaini, Paolo and Bonfanti, Silvia and Gargantini, Angelo and Riccobene, Elvinia},
  title = {Visual Notation and Patterns for Abstract State Machines},
  booktitle = {Software Technologies: Applications and Foundations},
  publisher = {Springer International Publishing},
  year = {2016},
  pages = {163--178},
  url = {https://doi.org/10.1007/978-3-319-50230-4_12},
  doi = {http://doi.org/10.1007/978-3-319-50230-4_12}
}
Bonfanti, S., Gargantini, A. and Mashkoor, A. A preliminary systematic literature review of the use of formal methods in medical software systems

[Abstract] [BibTeX]

 2016 European & Asian System, Software & Service Process Improvement & Innovation, EuroAsiaSPI2016  conference  
Abstract: The use of formal methods is often recommended to guarantee the provision of necessary services and to assess the correctness of critical properties, such as safety, security and reli-ability, in medical and healthcare systems. Several research groups have proposed and ap-plied formal methods related techniques to the design and development of medical software and systems. However, a systematic and inclusive survey with some form of analysis is still missing in this domain. For this reason, we have collected the relevant literature on the use of formal methods to the modeling, design, development, verification and validation of medical software systems. We apply the well-known systematic literature review technique and we run several queries in order to obtain information that can be useful for people working in this ar-ea. We present some research questions and the data answering these questions. We also discuss some limitations of the adopted approach and how to address these issues in order to have a comprehensive survey.
BibTeX: 
@conference{bonfanti2016preliminary,
  author = {Bonfanti, Silvia and Gargantini, Angelo and Mashkoor, Atif},
  title = {A preliminary systematic literature review of the use of formal methods in medical software systems},
  booktitle = {European & Asian System, Software & Service Process Improvement & Innovation, EuroAsiaSPI2016},
  year = {2016}
}
Bonfanti, S., Gargantini, A. and Vitali, A. A Mobile Application for the Stereoacuity Test

[Abstract] [BibTeX]

 2015 Digital Human Modeling. Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health, pp. 315-326  conference DOI URL 
Abstract: The research paper concerns the development of a new mobile application emulating measurements of stereoacuity using Google Cardboard. Stereoacuity test is based on binocular vision that is the skill of human beings and most animals to recreate depth sense in visual scene. Google Cardboard is a very low cost device permitting to recreate depth sense of images showed on the screen of a smartphone. Proposed solution exploits Google Cardboard to recreate and manage depth sense through our mobile application that has been developed for Android devices. First, we describe the research context as well as the aim of our research project. Then, we introduce the concept of stereopsis and technology used for emulating stereoacuity test. Finally, we portray preliminary tests made so far and achieved results are discussed.
BibTeX: 
@conference{10.1007/978-3-319-21070-4_32,
  author = {Bonfanti, Silvia and Gargantini, Angelo and Vitali, Andrea},
  title = {A Mobile Application for the Stereoacuity Test},
  booktitle = {Digital Human Modeling. Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health},
  publisher = {Springer International Publishing},
  year = {2015},
  pages = {315--326},
  url = {https://doi.org/10.1007/978-3-319-21070-4_32},
  doi = {http://doi.org/10.1007/978-3-319-21070-4_32}
}
Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A. and Riccobene, E. Formal Validation and Verification of a Medical Software Critical Component

[Abstract] [BibTeX]

 2015 Proceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp. 80-89  conference DOI URL 
Abstract: Medical device software malfunctioning can lead to injuries or death for humans and, therefore, its development should adhere to certification standards. However, these standards establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability. This paper presents a formal development process, based on the Abstract State Machine method, that integrates most of the activities required by the standards. The process permits to obtain, through a sequence of refinements, more detailed models that can be formally validated and verified. Offline and online testing techniques permit to check the conformance of the implementation w.r.t. the specification. The process is applied to the validation of the SAM medical software, that is used to measure the patients' stereoacuity in the diagnosis of amblyopia.
BibTeX: 
@conference{2015:FVV:3041406.3041516,
  author = {Paolo Arcaini and Silvia Bonfanti and Angelo Gargantini and Atif Mashkoor and Elvinia Riccobene},
  title = {Formal Validation and Verification of a Medical Software Critical Component},
  booktitle = {Proceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign},
  publisher = {IEEE Computer Society},
  year = {2015},
  pages = {80--89},
  url = {https://doi.org/10.1109/MEMCOD.2015.7340473},
  doi = {http://doi.org/10.1109/MEMCOD.2015.7340473}
}
Cologni, A., Fasanotti, L., Dovere, E., Previdi, F., Bonfanti, S. and Owen, F. Smartphone based video-telemetry logger for remote maintenance services

[Abstract] [BibTeX]

 2015 IFAC-PapersOnLine
Vol. 48(3)15th IFAC Symposium on Information Control Problems in Manufacturing, pp. 822 - 827 		 conference DOI URL 
Abstract: The strong growth of mobile devices of increasing quality and data transfer rates allows the introduction of these devices in diverse fields. In recent years, with the introduction of the “Smart factory” concept, the use of MIDs (Mobile Internet Devices) in manufacturing and assembly processes is increasingly common. The use of smart devices began at the managerial level, but it is now moving down to the factory floor. This evolution unlocks a large number of high-value services: from the time reduction of normal activities to implementing augmented reality. This research project incorporates a real-world example and defines a first operational paradigm for the acquisition, transmittal, and display of multi-source information. The aim of this paper is to describe, with clear references to a real case, the basic principles which should guide the implementation on a mobile platform of a remote maintenance service based on a hybrid (video and telemetry) logger.
BibTeX: 
@conference{COLOGNI2015822,
  author = {A.L. Cologni and L. Fasanotti and E. Dovere and F. Previdi and S. Bonfanti and F.C. Owen},
  title = {Smartphone based video-telemetry logger for remote maintenance services},
  booktitle = {15th IFAC Symposium on Information Control Problems in Manufacturing},
  journal = {IFAC-PapersOnLine},
  year = {2015},
  volume = {48},
  number = {3},
  pages = {822 - 827},
  url = {http://www.sciencedirect.com/science/article/pii/S2405896315004243},
  doi = {http://doi.org/10.1016/j.ifacol.2015.06.185}
}
Gargantini, A., Terzi, F., Zambelli, M. and Bonfanti, S. A Low-cost Virtual Reality Game for Amblyopia Rehabilitation

[Abstract] [BibTeX]

 2015 Proceedings of the 3rd 2015 Workshop on ICTs for Improving Patients Rehabilitation Research Techniques, pp. 81-84  conference DOI URL 
Abstract: The paper presents the design and development of a mobile application realizing a video game that aims at treating amblyopia by using a Google Cardboard. Google Cardboard is a low cost device able to reproduce virtual reality by means of a smartphone. The proposed video game engaged the patient in a car racing game and it displays the same image to the eyes, but with some differences that stimulate the lazy eye more than the normal eye.
BibTeX: 
@conference{Gargantini:2015:LVR:2838944.2838964,
  author = {Gargantini, Angelo and Terzi, Fabio and Zambelli, Matteo and Bonfanti, Silvia},
  title = {A Low-cost Virtual Reality Game for Amblyopia Rehabilitation},
  booktitle = {Proceedings of the 3rd 2015 Workshop on ICTs for Improving Patients Rehabilitation Research Techniques},
  publisher = {ACM},
  year = {2015},
  pages = {81--84},
  url = {http://doi.acm.org/10.1145/2838944.2838964},
  doi = {http://doi.org/10.1145/2838944.2838964}
}