Modeling complex system requirements often requires specifying system components in separate models, which can be validated and verified in isolation from each other, and then integrating all components’ behavior in order to validate the operation of the whole system. If models are executable, as for state-based formal specifications, engines to orchestrate the simulation of separate component operational models are extremely useful. This paper presents an approach for the co-simulation, according to predefined orchestration schemas, of state-based models of separate components of a Discrete Event System. More precisely, we exploit the Abstract State Machine (ASM) formal method as state-based formalism, and we (i) define a set of operators to compose ASMs that communicate with each other through I/O events, and (ii) present an engine to execute the compositional simulation of the ASMs as a whole assembly. As proof of concepts, we use a set of model examples of Discrete Event Systems of increasing complexity to show the application of our approach and to evaluate its effectiveness in co-simulating models of real systems.

To face complexity and scalability, the design of software-intensive systems requires the decomposition of the system into components, each modeled and analyzed separately from the others, and the composition of their analysis. Moreover, compositional model simulation is recognized as the only alternative available in practice when systems are large and complex, like in the cyber-physical domain, and intrinsically require combining the specification of ensembles of different parts (subsystems). Therefore, the need for simulation engines for composed model execution is getting a growing interest. Along this research line, this paper presents the results of the compositional modeling and validation by scenarios of an industrial medical system, called MVM-Adapt, that we designed as an adaptive version of an existing mechanical lung ventilator deployed and certified to treat pneumonia during the COVID-19 pandemic. We exploit the I/O Abstract State Machine formalism to model the device components as separate and interacting sub-systems that communicate through I/O events and adapt the device ventilation mode at run-time based on the health parameters of the patient. An orchestrated simulation coordinates the overall execution of these communicating I/O ASMs by exploiting suitable workflow patterns. This compositional simulation technique has proved to be useful in practice to validate the new adaptive MVM's behavior and thus to support architects in better understanding this new mode of operation of the prototyped system.

Abstract This tutorial paper introduces ASMETA, a comprehensive suite of integrated tools around the formal method Abstract State Machines to specify and analyze the executable behavior of discrete event systems. ASMETA supports the entire system development life-cycle, from the specification of the functional requirements to the implementation of the code, in a systematic and incremental way. This tutorial provides an overview of ASMETA through an illustrative case study, the Pill-Box, related to the design of a smart pillbox device. It illustrates the practical use of the range of modeling and V&V techniques available in ASMETA and C++ code generation from models, to increase the quality and reliability of behavioral system models and source code.

Abstract Modern automotive systems with adaptive control features require rigorous analysis to guarantee correct operation. We report our experience in modeling the automotive case study from the ABZ2020 conference using the ASMETA toolset, based on the Abstract State Machine formal method. We adopted a seamless system engineering method: from an incremental formal specification of high-level requirements to increasingly refined ASMETA models, to the C++ code generation from the model. Along this process, different validation and verification activities were performed. We explored modeling styles and idioms to face the modeling complexity and ensure that the ASMETA models can best capture and reflect specific behavioral patterns. Through this realistic automotive case study, we evaluated the applicability and usability of our formal modeling approach.

This paper proposes an evaluation framework for autonomous systems, called LENS. It is an instrument to make an assessment of a system through the lens of abilities related to adaptation and smartness. The assessment can then help engineers understand in which direction it is worth investing to make their system smarter. It also helps to identify possible improvement directions and to plan for concrete activities. Finally, it helps to make a re-assessment when the improvement has been performed in order to check whether the activity plan has been accomplished.Given the high variability in the various domains in which autonomous systems are and can be used, LENS is defined in abstract terms and instantiated to a specific and important class of medical devices, i.e., Programmable Electronic Medical Systems (PEMS). The instantiation, called LENSPEMS, is validated in terms ofapplicability, i.e., how it is applicable to real PEMS,generalizability, i.e., to what extent LENSPEMSis generalizable to the PEMS class of systems, andusefulness, i.e., how it is useful in making an assessment and identifying possible directions of improvement towards smartness.

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

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.

Classification using Artificial Neural Networks (ANNs) is widely applied in critical domains, such as autonomous driving and in the medical practice; therefore, their validation is extremely important. A common approach consists in assessing the network robustness, i.e., its ability to correctly classify input data that is particularly challenging for classification. We recently proposed a robustness definition that considers input data degraded by alterations that may occur in reality; the approach was originally devised for image classification in the medical domain. In this paper, we extend the definition of robustness to any type of input for which some alterations can be defined. Then, we present ROBY, a tool for ROBustness analYsis of ANNs. The tool accepts different types of data (images, sounds, text, etc.) stored either locally or on Google Drive. The user can use some alterations provided by the tool, or define their own. The robustness computation can be performed either locally or remotely on Google Colab. The tool has been experimented for robustness computation of image and sound classifiers, used in the medical and automotive domains.

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 re-engineering 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.

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.

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.

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.