In healthcare systems, practitioners are responsible for making decisions when a patient’s health, or even life, are at stake. Real-time data-driven modeling, analysis, and prediction approaches, such as the Digital Shadow (DS) paradigm, inform and support decision-makers in such critical situations. We introduce GENGAR, a DS-based methodology to identify critical scenarios in a patient-device-physician (PDP) triad with human agents and cyber-physical devices interacting under uncertainty. The proposed solution relies on automata-based modeling and formal analysis techniques to predict and inform the practitioner of critical contingencies that may compromise patient safety, enhancing the system’s dependability. In particular, it leverages automata learning to infer and evolve a realistic patient model from clinical logs. GENGAR then exploits mutational and searchbased fuzzing to generate scenarios and detect failure cases, i.e., those violating predefined dependability requirements. Failure scenarios are then filtered using qualitative criteria on clinical plausibility, yielding up to $60 \%$ realistic cases.

ABSTRACT Many of the classical questions reflecting the actionable use of formal methods in the software industry—“do they scale?” or “are they easily integrated?”—remain without a definitive answer, with many potentially adoptable formal notations being exploited in industry, but in a rather stove‐piped and siloed fashion, and with rather few, sometimes anecdotal, success stories to tell. In this article, we strive to provide some more answers to the aforementioned questions on formal methods adoption in industry. We focus our study on a widely adopted formal methods framework in Europe, that is, Verum Dezyne, employed by embedded‐computing and hardware‐programming companies including Thermo‐Fisher, Philips, and more. Results convey a rather interesting story—requiring further study into these matters—but also highlight practical insights for formal practitioners in the field, for example, that formal methods do not disrupt existing processes and scalability issues can be easily addressed by applying mainstream engineering practices, such as decomposition.

The paper addresses the problem of estimating the energy consumed by production resources in manufacturing so that alternative process designs can be compared in terms of energy expenditure. In particular, the proposed methodology focuses on Computer Numerical Controlled (CNC) machining centers. Classical approaches to energy modeling require high expertise and large development effort since, for example, data acquisition is resource-specific and must be repeated frequently to avoid obsolescence. An automated and flexible data-driven methodology is designed in this work. A data-driven method is employed to learn a hybrid and stochastic model of a CNC machining center’s energetic behavior. The learned model is used to provide offline energy consumption estimates of simulated part-programs before the actual execution of the cutting. Numerical results show the performance of the proposed method on a set of case studies. The methodology is also applied to a real industrial application, including data collected during machine production.Note to Practitioners—This article provides a flexible and autonomous data-driven approach to building models representing the energetic behavior of production resources, particularly CNC machining centers. The learned models can predict machine energy consumption while executing complex part-programs. The algorithm uses data that are commonly acquired by contemporary machine monitoring systems and does not require ad-hoc experimental tests for training. Specifically, it requires the spindle rotary speed signal, part load/unload signal, and spindle (or machine) power signal during the learning phase, whilst the estimation phase uses only the load/unload and spindle speed simulated signals.

Abstract Developing robotic applications with human–robot interaction for the service sector raises a plethora of challenges. In these settings, human behavior is essentially unconstrained as they can stray from the plan in numerous ways, constituting a critical source of uncertainty for the outcome of the robotic mission. Application designers require accessible and reliable frameworks to address this issue at an early development stage. We present a model-driven framework for developing interactive service robotic scenarios, allowing designers to model the interactive scenario, estimate its outcome, deploy the application, and smoothly reconfigure it. This article extends the framework compared to previous works by introducing an analysis of the impact of human errors on the mission’s outcome. The core of the framework is a formal model of the agents at play—the humans and the robots—and the robotic mission under analysis, which is subject to statistical model checking to estimate the mission’s outcome. The formal model incorporates a formalization of different human erroneous behaviors’ phenotypes, whose likelihood can be tuned while configuring the scenario. Through scenarios inspired by the healthcare setting, the evaluation highlights how different configurations of erroneous behavior impact the verification results and guide the designer toward the mission design that best suits their needs.

Abstract The speeding growth of the IT market and the spreading of disruptive technologies are leading towards more and more risky operations in need of constant upkeep, monitoring as well as proactive orchestration. On the one hand, the property allowing a system to be catered by automated monitoring and healing technology is defined as observability . On the other hand, appropriate design principles to manifest observability were originally referred as event sourcing by its inventor Martin Fowler and warrant for the aforementioned sustainable software operations. Both event sourcing and observability are complex to leverage on and design for. In an effort to understand more on both concepts, we offer an experience report on their practical use, featuring: (1) a rigorous definition of software architecture observability and a set of principles to design for observability using augmented forms of well‐known design patterns in line with event sourcing; and (2) an impact analysis in the context of a case study. Our study reveals several interesting notions around the concept of observability but our findings also make explicit new architecture trade‐offs that software architects and stakeholders need to consider as first‐class architecture‐level concerns.

Complex distributed systems such as the ones induced by Internet of Things (IoT) deployments, are expected to operate in compliance to their requirements. This can be checked by inspecting events flowing throughout the system, typically originating from end-devices and reflecting arbitrary actions, changes in state or sensing. Such events typically reflect the behavior of the overall IoT system – they may indicate executions which satisfy or violate its requirements. This article presents a service-based software architecture and technical framework supporting runtime verification for widely deployed, volatile IoT systems. At the lowest level, systems we consider are comprised of resource-constrained devices connected over wide area networks generating events. In our approach, monitors are deployed on edge components, receiving events originating from end-devices or other edge nodes. Temporal logic properties expressing desired requirements are then evaluated on each edge monitor in a runtime fashion. The system exhibits decentralization since evaluation occurs locally on edge nodes, and verdicts possibly affecting satisfaction of properties on other edge nodes are propagated accordingly. This reduces dependence on cloud infrastructures for IoT data collection and centralized processing. We illustrate how specification and runtime verification can be achieved in practice on a characteristic case study of smart parking. Finally, we demonstrate the feasibility of our design over a testbed instantiation, whereupon we evaluate performance and capacity limits of different hardware classes under monitoring workloads of varying intensity using state-of-the-art LPWAN technology.

Complex distributed systems such as the ones induced by Internet of Things (IoT) deployments, are expected to operate in compliance to their requirements. This can be checked by inspecting events flowing throughout the system, typically originating from end-devices and reflecting arbitrary actions, changes in state or sensing. Such events typically reflect the behavior of the overall IoT system – they may indicate executions which satisfy or violate its requirements.

Robots are currently mostly found in industrial settings. In the future, a wider range of environments will benefit from their inclusion. This calls for the development of tools that allow professionals to set up dependable robotic applications in which people productively interact with robots aware of their needs. Given the co-existence of humans and robots, the precise analysis-e.g., through formal verification techniques-of properties related to aspects such as human needs and physiology is of paramount importance. In this paper, we present a formally-based, model-driven approach to design and verify scenarios involving human-robot interactions. Some of the features of our approach are tailored to the healthcare domain, from which our case studies are derived. In our approach, the designer specifies the main parameters of the mission to generate the model of the application, which includes mobile robots, the humans to be served, including some of their physiological features, and the decision-maker that orchestrates the execution. All components are modeled through hybrid automata to capture variables with complex dynamics. The model is verified through Statistical Model Checking (SMC), using the Uppaal tool, to determine the probability of success of the mission. The results are examined by the developer, who iteratively refines the design until the probability of success is satisfactory.

Abstract Apache Spark is probably the most widely adopted framework for developing big-data batch applications and for executing them on a cluster of (virtual) machines. In general, the more resources (machines) one uses, the faster applications execute, but there is currently no adequate means to determine the proper size of a Spark cluster given time constraints, or to foresee execution times given the number of employed machines. One can only run these applications and use her/his experience to size the cluster and predict expected execution times. Wrong estimation of execution times can lead to costly overruns and overly long executions, thus calling for analytic sizing/prediction techniques that provide precise time guarantees. This paper addresses this problem by proposing a solution based on model-checking. The approach exploits a directed acyclic graph (DAG) to abstract the structure of the execution flows of Spark programs, annotates each node (Spark stage) with execution-related data, and formulates the identification of the global execution time as a reachability problem. To avoid the well-known state space explosion problem, the paper also proposes a technique to reduce the size of generated abstract models. This results in a significant decrease in used memory and/or verification time making our approach feasible for predicting the execution time of Spark applications given the resources available. The benefits of the proposed reduction technique are evaluated by using both timed automata and constraint LTL over clocks logic to formally encode and analyze generated models. The approach is also successfully validated on some realistic case studies. Since the optimization is not Spark-specific, we claim that it can be applied to a wide range of applications whose underlying model can be abstracted as a DAG.

Abstract Developing robotic applications is a complex task, which requires skills that are usually only possessed by highly-qualified robotic developers. While formal methods that help developers in the creation and design of robotic applications exist, they must be explicitly customized to be impactful in the robotics domain and to support effectively the growth of the robotic market. Specifically, the robotic market is asking for techniques that: (i) enable a systematic and rigorous design of robotic applications though high-level languages; and (ii) enable the automatic synthesis of low-level controllers, which allow robots to achieve their missions. To address these problems we present the PuRSUE (Planner for RobotS in Uncontrollable Environments) approach, which aims to support developers in the rigorous and systematic design of high-level run-time control strategies for robotic applications. The approach includes PuRSUE-ML a high-level language that allows for modeling the environment, the agents deployed therein, and their missions. PuRSUE is able to check automatically whether a controller that allows robots to achieve their missions might exist and, then, it synthesizes a controller. We evaluated how PuRSUE helps designers in modeling robotic applications, the effectiveness of its automatic computation of controllers, and how the approach supports the deployment of controllers on actual robots. The evaluation is based on 13 scenarios derived from 3 different robotic applications presented in the literature. The results show that: (i) PuRSUE-ML is effective in supporting designers in the formal modeling of robotic applications compared to a direct encoding of robotic applications in low-level modeling formalisms; (ii) PuRSUE enables the automatic generation of controllers that are difficult to create manually; and (iii) the plans generated with PuRSUE are indeed effective when deployed on actual robots.

Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for checking whether the behaviours of a system satisfy a set of properties of interest. Even if efficient model-checkers for Timed Automata exist, these tools are not easily configurable. First, they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures, but they assume a fixed set of Timed Automata constructs. Second, they usually do not support the Metric Interval Temporal Logic (MITL) and rely on a precise semantics for the logic in which the property of interest is specified, which cannot be easily modified and customized. Finally, they do not easily allow using different solvers that may speed up verification in different contexts. This article presents a novel technique to perform model checking of Metric Interval Temporal Logic (MITL) properties on TA. The technique relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula, which is verified through an available decision procedure. The technique is flexible, since the intermediate logic allows the encoding of new semantics as well as new TA constructs, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures.

Abstract Cyber‐physical systems (CPS) are highly dynamic and large scale systems integrated with the physical environment that they monitor and actuate on. CPS have to adapt online to the changing nature of the physical environment; this may require the online modification of their system model, but any change should preserve correct operation. Correctness by construction relies on using formal tools, which suffer from a considerable computational overhead. As the current system model of a CPS may adapt to the environment, the new system model must be verified before its execution to ensure that the properties are preserved. However, CPS development has mainly concentrated on the design‐time aspects, existing only few contributions that address their online adaptation. We research on the pros and cons of formal tools to support dynamic changes at runtime. We formalize the semantics of the adaptation logic of an autonomic manager (OLIVE) that performs online verification for a specific application, a dynamic virtualized server system. We explore the use of formal tools based on CLTLoc to express functional and nonfunctional properties of the system. We provide empirical results showing the temporal costs of our approach.

We present our efforts on the formalization and automated formal verification of data-intensive applications based on the Storm technology, a well known and pioneering framework for developing streaming applications. The approach is based on the so-called array-based systems formalism, introduced by Ghilardi et al., a suitable abstraction of infinite-state systems that we used to model the runtime behavior of Storm-based applications. The formalization consists of quantified formulae belonging to a certain fragment of first-order logic to symbolically represent array-based systems.The formalization consists of quantified first-order formulae symbolically representing array-based systems. The verification consists in checking whether some safety property holds or not for the system. Both formalization and verification are performed in the same framework, namely the state-of-the-art Cubicle model checker.

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval of the formula to be checked. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches.

Big data architectures have been gaining momentum in recent years. For instance, Twitter uses stream processing frameworks like Storm to analyse billions of tweets per minute and learn the trending topics. However, architectures that process big data involve many different components interconnected via semantically different connectors making it a difficult task for software architects to refactor the initial designs. As an aid to designers and developers, we developed OSTIA (On-the-fly Static Topology Inference Analysis) that allows: (a) visualising big data architectures for the purpose of design-time refactoring while maintaining constraints that would only be evaluated at later stages such as deployment and run-time, (b) detecting the occurrence of common anti-patterns across big data architectures, (c) exploiting software verification techniques on the elicited architectural models. This paper illustrates OSTIA and evaluates its uses and benefits on three industrial-scale case studies.

Constraint LTL-over-clocks is a variant of CLTL, an extension of linear-time temporal logic allowing atomic assertions in a concrete constraint system. Satisfiability of CLTL-over-clocks is here shown to be decidable by means of a reduction to a decidable SMT (Satisfiability Modulo Theories) problem. The result is a complete Bounded Satisfiability Checking procedure, which has been implemented by using standard SMT solvers. The importance of this technique derives from the possibility of translating various continuous-time metric temporal logics, such as MITL and QTL, into CLTL-over-clocks itself. Although standard decision procedures of these logics do exist, they have never been realized in practice. Suitable translations into CLTL-over-clocks have instead allowed us the development of the first prototype tool for deciding MITL and QTL. The paper also reports preliminary, but encouraging, experiments on some significant examples of MITL and QTL formulae.

An important problem that arises during the execution of service-based applications concerns the ability to determine whether a running service can be substituted with one with a different interface, for example if the former is no longer available. Standard Bounded Model Checking techniques can be used to perform this check, but they must be able to provide answers very quickly, to avoid that the check may affect the operativeness of the application, instead of aiding it. The problem becomes even more complex when conversational services are considered, i.e., services that expose operations that have Input/Output data dependencies among them. In this paper we introduce a formal verification technique for an extension of Linear Temporal Logic that allows users to include in formulae constraints on integer variables. This technique applied to the substitutability problem for conversational services is shown to be considerably faster and with smaller memory footprint than existing ones.

This paper defines CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. The paper introduces suitable restrictions and assumptions that make the satisfiability problem decidable in many cases, although the problem is undecidable in the general case. Decidability is shown for a large class of constraint systems, and an encoding into Boolean logic is defined. This paves the way for applying existing SMT-solvers for checking the Bounded Reachability problem, as shown by various experimental results.

A core problem in formal methods is the transition from informal requirements to formal specifications. Especially when specifying reactive systems, many formalisms require the user to either understand a complex mathematical theory and notation or to derive details not given in the requirements, such as the state space of the problem. While formalizing a real-world requirements document, we developed a technique where not states but signal patterns are the main elements. We argue that it supports a formalization that is often closer to the informal requirements and thus provides a smoother transition to formal methods. As only tables of regular expressions are used for notation, the technique can easily be understood by non-mathematicians. Many properties, such as consistency, can be checked automatically on these specifications. Besides the formal foundation of our approach, this paper presents prototypical tool support and first results from an industrial case study.