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.

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.

Summary Regular expressions are used to characterize sets of strings (ie, languages) using a pattern‐based syntax. They are applied in different contexts as, for example, data validation in Web forms. However, writing a regular expression that exactly captures the desired set of strings could be particularly difficult, and techniques are sought to validate regular expressions or test their use in applications. A common means to regular expression validation and testing is the generation of a set of labelled strings (ie, strings together with their evaluation). We here propose a fault‐based approach for generating strings usable as tests for regular expressions. We define some fault classes representing mistakes that could be made when writing a regular expression, and we introduce the notion of distinguishing string, ie, a string that is able to expose a fault. Given a regular expression, our approach generates a test suite composed of distinguishing strings that are able to detect possible faults in the regular expression. We present different versions of the approach, which provide different results in terms of test suite size and generation time. Experiments show that the proposed approach can generate compact test suites and that, using suitable optimizations, the generation time is reasonable. Exploiting the proposed fault classes, we use the notion of mutation score to assess the ability of a generic set of strings in exposing possible faults contained in the regular expression under test. A comparison with other test generation tools in terms of mutation score, size, and generation time shows the advantages and limits of our approach.

Model-based test generation by model checking is a well-known testing technique that, however, suffers from the state explosion problem of model checking and it is, therefore, not always applicable. In this paper, we address this issue by decomposing a system model into suitable subsystem models separately analyzable. Our technique consists in decomposing that portion of a system model that is of interest for a given testing requirement, into a tree of subsystems by exploiting information on model variable dependency. The technique generates tests for the whole system model by merging tests built from those subsystems. We measure and report effectiveness and efficiency of the proposed decomposition-based test generation approach, both in terms of coverage and time.

NuSMV is a well-known tool for system verification that permits to verify both CTL and LTL properties. Although the tool is very powerful, it offers a minimal support for the editing and validation (e.g., by simulation) of models and of requirements specified as temporal properties. In this paper, we propose NuSeen, a framework that assists a designer during the modeling and V&V activities when using NuSMV. In addition to an editor furnished with syntax highlighting, autocompletion, and outline, NuSeen also provides some tools for visualizing the variable dependencies, and graphically visualizing the counterexamples. It helps the designer in validating the model by checking certain qualities like minimality and completeness. Moreover, the framework also provides facilities for model-based testing by means of a test suite generator that is able to generate tests achieving value and decision coverage for NuSMV models.

Feedback control loops that monitor and adapt managed parts of a software system are considered crucial for realizing self-adaptation in software systems. The MAPE-K (Monitor-Analyze-Plan-Execute over a shared Knowledge) autonomic control loop is the most influential reference control model for self-adaptive systems. The design of complex distributed self-adaptive systems having decentralized adaptation control by multiple interacting MAPE components is among the major challenges. In particular, formal methods for designing and assuring the functional correctness of the decentralized adaptation logic are highly demanded. This article presents a framework for formal modeling and analyzing self-adaptive systems. We contribute with a formalism, called self-adaptive Abstract State Machines , that exploits the concept of multiagent Abstract State Machines to specify distributed and decentralized adaptation control in terms of MAPE-K control loops, also possible instances of MAPE patterns. We support validation and verification techniques for discovering unexpected interfering MAPE-K loops, and for assuring correctness of MAPE components interaction when performing adaptation.

Abstract The request of formal methods for the specification and analysis of distributed systems is nowadays increasing, especially when considering the development of Cloud systems and Web applications. This is due to the fact that modeling languages currently used in these areas have informal definitions and ambiguous semantics, and therefore their use may be unreliable. Thanks to their mathematical foundation, formal methods can guarantee rigorous system design, leading to precise models where requirements can be validated and properties can be assured, already at the early stages of the system development. In this paper, we present a rigorous engineering process for distributed systems, based on the Abstract State Machines (ASM) formal method. We rely on the foundational notions of ASM ground model and model refinement to obtain a precise model for a client-server application for Cloud systems. This application has been proposed to tackle the problem of making Cloud services usable to different end-devices by adapting on-the-fly the content coming from the Cloud to the different devices contexts. The ASM-based modeling process is supported by a number of validation and verification activities that have been exploited on the component under development to guarantee consistency, correctness, and reliability properties.

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.

One of the well-known techniques for model-based test generation exploits the capability of model checkers to return counterexamples upon property violations. However, this approach is not always optimal in practice due to the required time and memory, or even not feasible due to the state explosion problem of model checking. A way to mitigate these limitations consists in decomposing a system model into suitable subsystem models separately analyzable. In this paper, we show a technique to decompose a system model into subsystems by exploiting the model variables dependency, and then we propose a test generation approach which builds tests for the single subsystems and combines them later in order to obtain tests for the system as a whole. Such approach mitigates the exponential increase of the test generation time and memory consumption, and, compared with the same model-based test generation technique applied to the whole system, shows to be more efficient. We prove that, although not complete, the approach is sound.

In the context of automatic test generation, the use of propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers is becoming an attractive alternative to traditional algorithmic test generation methods, especially when testing Boolean expressions. The main advantages are the capability to deal with constraints over the inputs, the generation of compact test suites and the support for fault-detecting test generation methods. However, these solvers normally require more time and a greater amount of memory than classical test generation algorithms, making their applicability not always feasible in practice. In this paper, we propose several ways to optimize the SAT/SMT-based process of test generation for Boolean expressions and we compare several solving tools and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.

Summary Among validation techniques,model reviewis a static analysis approach that can be performed at the early stages of software development, at the specification level, and aims at determining if a model owns certain quality attributes (like completeness, consistency and minimality). However, the model review capability to detect behavioural faults has never been measured. In this paper, a methodology and a supporting tool for evaluating the fault detection capability of a NuSMV model advisor are presented, which performs an automatic static model review of NuSMV models. The approach is based on the use ofmutationin a similar way as in mutation testing: several mutation operators for NuSMV models are defined, and the model advisor is used to detect behavioural faults by statically analysing mutated specifications. In this way, it is possible to measure the model advisor ability to discover faults. To improve the quality of the analysis, the equivalence between a NuSMV model and any of its mutants must be checked. To perform this task, this paper proposes a technique based on the concept of equivalent Kripke structures, as NuSMV models are Kripke structures. A number of experiments assess the fault‐detecting capability, precision and accuracy of the proposed approach. Analysis of variance is used to check if the results are statistically significant. Some relationships among mutation operators and model quality attributes are also established. Copyright © 2014 John Wiley & Sons, Ltd.

Abstract Service-oriented Computing is rapidly gaining importance across several application domains due to its capability of composing autonomous and loosely-coupled services. In order to support the engineering of service-oriented software applications, foundational theories, service modeling notations, evaluation techniques fully integrated in a pragmatic software engineering approach are required. This article introduces a framework for modeling and prototyping service-oriented applications. The framework consists of a precise and executable language, SCA-ASM , for model-based design, and of a tool for early and quick design evaluation of service assemblies. The language combines the OASIS/OSOA standard Service Component Architecture (SCA) capability of modeling and assembling heterogeneous service-oriented components in a technology agnostic way, with the rigor of the Abstract State Machine (ASM) formal method able to model notions of service behavior, interactions, orchestration, compensation and context-awareness in an abstract but executable way. The tool is based on existing execution environments for ASM models and SCA applications. An SCA-ASM model of a service-oriented component, possibly not yet implemented in code or available as off-the-shelf, can be (i) simulated and evaluated offline , i.e. in isolation from the other components; or (ii) executed as abstract implementation (or prototype ) together with the other components implementations according to the chosen SCA assembly. As proof of concept, a case study taken from EU research projects has been considered to show the functionalities and potentialities of the proposed framework.

Recent advances in propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers are increasingly rendering SAT and SMT-based automatic test generation an attractive alternative to traditional algorithmic test generation methods. The use of SAT/SMT solvers is particularly appealing when testing Boolean expressions: These tools are able to deal with constraints over the models, generate compact test suites, and they support fault-based test generation methods. However, these solvers normally require more time and greater amount of memory than classical test generation algorithms, limiting their applicability. In this paper we propose several ways to optimize the process of test generation and we compare several SAT/SMT solvers and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.

Abstract This paper presents a model‐driven software process suitable to develop a set of integrated tools around a formal method. This process exploits concepts and technologies of the Model‐driven Engineering (MDE) approach, such as metamodelling and automatic generation of software artifacts from models. We describe the requirements to fulfill and the development steps of this model‐driven process. As a proof‐of‐concept, we apply it to the Finite State Machines and we report our experience in engineering a metamodel‐based language and a toolset for the Abstract State Machine formal method. Copyright © 2011 John Wiley & Sons, Ltd.

In this paper, we present our position and experience on integrating formal methods with the model-driven engineering (MDE) approach to software development. Both these two approaches have advantages and disadvantages, and we here show how the advantages of one can be exploited to cover or weaken the disadvantages of the other. We also propose an in-the-loop integration which allows the development of a general framework for software engineering where rigorousness and preciseness of formal methods are combined with flexibility and automation of the MDE. We discuss the feasibility of unifying these two separate worlds, referring to our experience on integrating the abstract state machine formal method with the Eclipse modeling framework supporting MDE facilities.

This article summarizes our effort, since 2004 up to the present time, for improving the current industrial Systems-on-Chip and Embedded Systems design by joining the capabilities of the unified modeling language (UML) and SystemC/C programming languages to operate at system-level. The proposed approach exploits the OMG model-driven architecture—a framework for Model-driven Engineering—capabilities of reducing abstract, coarse-grained and platform-independent system models to fine-grained and platform-specific models. We first defined a design methodology and a development flow for the hardware, based on a SystemC UML profile and encompassing different levels of abstraction. We then included a multithread C UML profile for modelling software applications. Both SystemC/C profiles are consistent sets of modelling constructs designed to lift the programming features (both structural and behavioral) of the two coding languages to the UML modeling level. The new codesign flow is supported by an environment, which allows system modeling at higher abstraction levels (from a functional executable level to a register transfer level) and supports automatic code-generation/back-annotation from/to UML models.

This paper describes a scenario-based methodology for system-level design validation based on the Abstract State Machines formal method. This scenario-based approach complements an existing model-driven design methodology for embedded systems based on the SystemC UML profile. It allows the designer to functionally validate system components from SystemC UML designs early at high levels of abstraction and without requiring strong skills and expertise on formal methods. A validation tool integrated into an existing model-driven co-design environment to support the proposed scenario-based validation flow is also presented.

This paper reports our experience in exploiting the metamodelling approach of model-driven language engineering to define a standard modelling language for the Abstract State Machines (ASMs) formal method, and develop a general framework (ASMETA) for a wide interoperability of ASM tools in a model-driven development context. We describe the requirements to fulfill and the design, implementation, validation, and tools development steps necessary to support such a language engineering life cycle. We finally discuss the benefits/limits of a model-driven language engineering approach with respect to traditional techniques primarily used for the same goal.

This paper presents a prototype environment for HW/SW co--design of embedded systems based on the Unified Modeling Language (UML) and SystemC. The environment supports a model-driven SoC design methodology which provides a graphical high-level representation of hardware and software components, and allows either C/C++/SystemC code generation from models and a reverse engineering process from code to graphical UML models.

This paper starts with a brief introduction to the UML 2.0 and application-specific UML customizations via profiles. After a discussion of UML design tools with focus on EDA support, we present a HW/SW co-design approach and demonstrate how HW architectures are described together with application SW in a unique UML based environment. Using a dedicated profile providing support for SystemC in UML, and a SystemC wrapper for the SimIt instruction set simulator of a StrongARM, an executable model of the complete architecture is generated which can be simulated by the SystemC kernel. The physical layer of an 802.11a system is used as an application example.

In this paper, we present a SoC design methodology joining the capabilities of UML and SystemC to operate at system-level. We present a UML 2.0 profile of the SystemC language, exploiting the MDA capabilities of defining modeling languages, platform independent and reducible to platform dependent languages. The UML profile captures both the structural and the behavioral features of the SystemC language, and allows high level modeling of system-on-a-chip with straightforward translation to SystemC code.

In this paper we present a UML 2.0 profile for the SystemC language, which is a consistent set of modeling constructs designed to lift both structural and behavioral features (including events and time features) of the SystemC language to UML level. The main target of this profile is to provide a means for software and hardware engineers to improve the current industrial Systems-on-a-Chip (SoC) design methodology joining the capabilities of UML and SystemC to operate at system-level.