Ing. Silvia Bonfanti, PhD

Matching entries: 0
settings...
AuthorTitleYearJournal/ProceedingsReftypeDOI/URL
Bonfanti, S., Gargantini, A. and Mashkoor, A. AsmetaA: Animator for Abstract State Machines 2018 International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z  inproceedings 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.<\td>
BibTeX:
@inproceedings{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 2018 14th Workshop on Advances in Model Based Testing (A-MOST), ICST 2018, Vasteras, Sweden  inproceedings 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:
@inproceedings{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 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 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 2017 NASA Formal Methods, pp. 295-301  inproceedings 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:
@inproceedings{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 2017 ICTs for Improving Patients Rehabilitation Research Techniques, pp. 116-125  inproceedings 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:
@inproceedings{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) 2017 Proceedings of the 11th European Conference on Software Architecture: Companion Proceedings, pp. 12-15  inproceedings 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:
@inproceedings{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 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 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 2016 Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 231-236  inproceedings 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:
@inproceedings{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 2016 Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 344-359  inproceedings 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:
@inproceedings{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 2016 Software Technologies: Applications and Foundations, pp. 163-178  inproceedings 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:
@inproceedings{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 2016 European & Asian System, Software & Service Process Improvement & Innovation, EuroAsiaSPI2016  inproceedings  
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:
@inproceedings{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 2015 Digital Human Modeling. Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health, pp. 315-326  inproceedings 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:
@inproceedings{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 2015 Proceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp. 80-89  inproceedings 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:
@inproceedings{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 2015 IFAC-PapersOnLine
Vol. 48(3)15th IFAC Symposium on Information Control Problems in Manufacturing, pp. 822 - 827 
inproceedings 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:
@inproceedings{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 2015 Proceedings of the 3rd 2015 Workshop on ICTs for Improving Patients Rehabilitation Research Techniques, pp. 81-84  inproceedings 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:
@inproceedings{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}
}