Smart manufacturing relies on the digitization of all the industrial processes, from production to business operations.It uses Industrial Internet of Things (IIoT) principles to equip devices with smart sensors and actuators, integrating machines and software through data collection, advanced computational methods, and remote control.Our research is motivated by a real digital transition application in the luxury fashion in Italy.The customers wish to update legacy systems, to comply with new Industry 4.0 standards.Due to industrial property requirements, as well as brand secrets, they require the whole architecture to run on-premises.A further requirement is that the system installation must be non-invasive, potentially running on systems with frugal setups in terms of hardware and software.Adhering to such requirements and principles, this paper proposes an architecture for data pipeline in smart manufacturing that runs on-premises, offering support to legacy machines.It is capable of identifying unknown hardware, in terms of semantics of its sensors.The core component of such a concrete architecture is an innovative Extract-Transform-Load (ETL) connector, called sEmantic eXtended ETL (exETL), that manages numerous heterogeneous data sources, and recognizes and configures automatically new machinery sensors.It employs a dedicated Machine Learning (ML) pipeline.The flexibility of the proposed architecture is compared to alternative solutions that exploit existing technologies.Its computational effectiveness is assessed by building an emulated environment, and running extensive experiments on real data.Our results show that our data pipeline is lightweight, more flexible than competitors, and capable of integrating legacy or new machinery seamlessly.

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.

The field of uncertainty quantification and mitigation in software-intensive and self-adaptive systems is garnering increased interest, especially with the rise of statistical inference methodologies like Bayesian reasoning. These methods typically address uncertain quality attributes embedded within system models by adjusting model parameters. However, the uncertainty related to selecting a specific system model over plausible alternatives has received limited attention. Our work focuses on self-adaptation, exploring methods to tackle uncertainty in model selection. This includes scenarios where one model is chosen over competing alternatives to encapsulate the system’s understanding and anticipate future observations. Our proposed solution augments the conventional feedback loop of self-adaptive systems by combining Bayesian model averaging to mitigate uncertainty and many-objective optimization to take into account multiple, possibly many, dependability requirements at the same time. We carry out an empirical evaluation to study the effectiveness, cost, and scalability of the proposed approach using two case studies with increasing structural complexity and number of dependability requirements. Results show that our approach based on model averaging is significantly better than model selection in terms of satisfied requirements after adaptation (adaptation success frequency). We also show that our approach can deal with large model spaces ( \(\sim 10^{19}\) ) using efficient sampling methods rather than exhaustive model space exploration.

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.

Cyber-physical systems often operate in dynamic environments where unexpected events should be managed while guaranteeing acceptable behavior. Providing comprehensive evidence of their dependability under change represents a major open challenge. In this article, we exploit the notion of equilibrium, that is, the ability of the system to maintain an acceptable behavior within its multidimensional viability zone and propose RUNE 2 (RUNtime Equilibrium verification and Enforcement), an approach able to verify at runtime the equilibrium condition and to enforce the system to stay in its viability zone. RUNE 2 includes (i) a system specification that takes into account the uncertainties related to partial knowledge and possible changes; (ii) the computation of the equilibrium condition to define the boundaries of the viability zone; (iii) a runtime equilibrium verification method that leverages Bayesian inference to reason about the ability of the system to remain viable; and (iv) a resilience enforcement mechanism that exploits the posterior knowledge to steer the execution of the system inside the viability zone. We demonstrate both benefits and costs of the proposed approach by conducting an empirical evaluation using two case studies and 24 systems synthetically generated from pseudo-random models with increasing structural complexity.

Self-adaptive systems increasingly rely on machine learning techniques as black-box models to make decisions even when the target world of interest includes uncertainty and unknowns. Because of the lack of transparency, adaptation decisions, as well as their effect on the world, are hard to explain. This often hinders the ability to trace unsuccessful adaptations back to understandable root causes. In this paper, we introduce our vision of explainable self-adaptation. We demonstrate our vision by instantiating our ideas on a running example in the robotics domain and by showing an automated proof-of-concept process providing human-understandable explanations for successful and unsuccessful adaptations in critical scenarios.

Research on uncertainty quantification and mitigation of software-intensive systems and (self-)adaptive systems, is increasingly gaining momentum, especially with the availability of statistical inference techniques (such as Bayesian reasoning) that make it possible to mitigate uncertain (quality) attributes of the system under scrutiny often encoded in the system model in terms of model parameters. However, to the best of our knowledge, the uncertainty about the choice of a specific system model did not receive the deserved attention.

Modern software systems operate in complex and changing environments and are exposed to multiple sources of uncertainty. Testing methods shall be tailored to uncertainty as a first-class concern in order to quantify it and deliver increased confidence in the level of assurance of the final product. In this paper, we introduce novel model-based exploration strategies that generate test cases targeting uncertain components of the system under test. Our testing framework leverages Markov Decision Processes as modeling formalism of choice. The tester explicitly specifies uncertainty by means of beliefs attached to transition probabilities. The structural properties of the model and the uncertainty specification are then exploited to drive the test case generation process. Bayesian inference is used to achieve this objective by updating the initial beliefs through the evidence collected by testing. The proposed uncertainty-aware test selection strategies have been systematically evaluated on three realistic benchmarks and nine synthetic systems exhibiting up to 10k model transitions. We demonstrate the effectiveness of the novel strategies with well-established metrics. Results show they outperform existing testing methods with a gain up to 2.65× in terms of accuracy of the inference process.

Summary Nowadays, there exists an increasing demand for reliable software systems able to fulfill their requirements in different operational environments and to cope with uncertainty that can be introduced both at design‐time and at runtime because of the lack of control over third‐party system components and complex interactions among software, hardware infrastructures and physical phenomena. This article addresses the problem of the discrepancy between measured data at runtime and the design‐time formal specification by using aninverse uncertainty quantificationapproach. Namely, we introduce a methodology calledMETRICand its supporting toolchain to quantify and mitigate software system uncertainty during testing by combining (on‐the‐fly)model‐based testingandBayesian inference. Our approach connects probabilistic input/output conformance theory with statistical hypothesis testing in order to assess if the behaviour of the system under test corresponds to its probabilistic formal specification provided in terms of aMarkov decision process. An uncertainty‐aware model‐based test case generation strategy is used as a means to collect evidence from software components affected by sources of uncertainty. Test results serve as input to a Bayesian inference process that updates beliefs on model parameters encoding uncertain quality attributes of the system under test. This article describes our approach from both theoretical and practical perspectives. An extensive empirical evaluation activity has been conducted in order to assess the cost‐effectiveness of our approach. We show that, under same effort constraints, our uncertainty‐aware testing strategy increases the accuracy of the uncertainty quantification process up to 50 times with respect to traditional model‐based testing methods.

Modern software systems are required to operate in a highly uncertain and changing environment. They have to control the satisfaction of their requirements at run-time, and possibly adapt and cope with situations that have not been completely addressed at design-time. Software engineering methods and techniques are, more than ever, forced to deal with change and uncertainty (lack of knowledge) explicitly. For tackling the challenge posed by uncertainty in delivering more reliable systems, this paper proposes a novel online Model-based Testing technique that complements classic test case generation based on pseudo-random sampling strategies with an uncertainty-aware sampling strategy. To deal with system uncertainty during testing, the proposed strategy builds on an Inverse Uncertainty Quantification approach that is related to the discrepancy between the measured data at run-time (while the system executes) and a Markov Decision Process model describing the behavior of the system under test. To this purpose, a conformance game approach is adopted in which tests feed a Bayesian inference calibrator that continuously learns from test data to tune the system model and the system itself. A comparative evaluation between the proposed uncertainty-aware sampling policy and classical pseudo-random sampling policies is also presented using the Tele Assistance System running example, showing the differences in achieved accuracy and efficiency.

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.

Due to the on-demand and dynamic nature of Cloud, there is an increasing interest for automated management of adaptation and (possibly) re-deployment of cloud applications to realize quality requirements and evolution needs autonomously at run-time. This paper proposes a fast and automated approach for adapting and redeploying a cloud application at run-time as dictated by evolution needs and sudden changes in the operating environment conditions. The proposed approach exploits a graph-based model and an algorithm that extracts a sub-graph identifying the adaptation processes to be executed according to evolution changes. The approach is general enough to be implemented by any cloud application management framework. A TOSCA-based description of the structure and management aspects of the cloud application may be updated according to the above mentioned sub-graph. Then, this description may be processed by a TOSCA-compliant runtime environment to effectively adapt and possibly re-deploy the cloud application in an automated manner. The paper also illustrates the instantiation of this generic approach for adapting an e-commerce cloud application.

Self-adaptive systems autonomously adapt their behavior at run-time to react to internal dynamics and to uncertain and changing environment conditions. Specification and verification of self-adaptive systems are generally very difficult to carry out due to their high complexity, especially when involving time constraints. In the last case, in fact, the correctness of systems depends also on the time associated with events. This paper introduces a formal approach to specify and verify the self-adaptive behavior of real-time systems. Our specification formalism is based on Time-Basic Petri nets, a particular timed extension of Petri nets. We propose adaptation models to realize self-adaptation with temporal constraints and we adopt a zone-based modeling approach to support separation of concerns during the modeling phase. Zones identified during the modeling phase can be then used as modules (TB Petri subnets) either in isolation, to verify intra-zone properties, or all together, to verify inter-zone properties over the entire system model and check that all the temporal deadlines are met. We illustrate our approach by modeling and verifying a time-critical Gas Burner system that exhibits a self-healing behavior.

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.

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.