Integrated Rigorous Analysis in Cyber-Physical Systems Engineering

Rigorous development processes aim to be effective in developing critical systems, especially if failures can have catastrophic consequences for humans and the environment. Such processes generally rely on formal methods, which can guarantee, thanks to their mathematical foundation, model preciseness, and properties assurance. However, they are rarely adopted in practice.

In this talk, I report the experience of my research group in using the Abstract State Machine formal method and the ASMETA framework in developing a prototype of the control software of the MVM (Mechanical Ventilator Milano), a mechanical lung ventilator that has been designed, successfully certified, and deployed during the COVID-19 pandemic.

Although due to time constraints and lack of skills, no formal method was applied for the MVM project, later we wanted to assess the feasibility of developing (part of) the ventilator by using a formal method-based approach. Our development process starts from a high-level formal specification of the system to describe the MVM main operation modes. Then, through a sequence of refined models, all the other requirements are captured, up to a level in which a C++ implementation of a prototype of the MVM controller is automatically generated from the model, and tested.

Along the process, at each refinement level, different model validation and verification activities are performed, and each refined model is proved to be a correct refinement of the previous level. By means of the MVM case study, we evaluate the effectiveness and usability of our formal approach.

CPS is becoming increasingly distributed, where a set of asynchronous agents deal with continuous signals that do not share a global clock. We advocate for runtime verification (RV) of distributed CPS as a complementary method, but a roadmap for enhancing its effectiveness and efficiency is much needed. This brief talk will go over the challenges, recent advances, open problem problems and opportunities in RV for distributed CPS. We will first explain the challenges of verification of a set of continuous signals subject to clock drifts against specifications expressed in the signal temporal logic (STL). We then explain how a practical assumption, namely, an off- the-shelf clock synchronization algorithm such as NTP, can drastically contribute to efficiency and effectiveness of RV. Finally, we show how exploiting special characteristics of CPS such as the knowledge of dynamics of physical processes can reduce the runtime overhead and discuss a roadmap of open problems, applications, and opportunities.

Stochastic hybrid automata (SHA) are a powerful tool to evaluate the dependability and safety of critical infrastructures. However, the resolution of nondeterminism, which is present in many purely hybrid models, is often only implicitly considered in SHA. This paper instead proposes algorithms for computing maximum and minimum reachability probabilities for singular automata with urgent transitions and random clocks which follow arbitrary continuous probability distributions. We borrow a well-known approach from hybrid systems reachability analysis, namely flowpipe construction, which is then extended to optimize nondeterminism in the presence of random variables. Firstly, valuations of random clocks which ensure reachability of specific goal states are extracted from the computed flowpipes and secondly, reachability probabilities are computed by integrating over these valuations. We compute maximum and minimum probabilities for history-dependent prophetic and non-prophetic schedulers using set-based methods. The implementation featuring the library Hypo and the complexity of the approach are discussed in detail. Two case studies featuring nondeterministic choices show the feasibility of the approach.

The performance and reliability of Cyber-Physical Systems are increasingly aided through the use of digital twins, which mirror the static and dynamic behaviour of a Cyber-Physical System (CPS) in software. Digital twins enable the development of self-adaptive CPSs which reconfigure their behaviour in response to novel environments. It is crucial that these self-adaptations are formally verified at runtime, to avoid expensive re-certification of the reconfigured CPS.

In this talk, I discuss formally verified self-adaptation in a digital twinning system, by constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.

This talk provides a summary of experiences in the development of a Systems Engineering Environment using Formal Methods-based tools on the DARPA CASE program, highlighting notable successes, research and development challenges, as well as technology gaps.

In this talk, I will introduce our research for safety of automated driving systems (ADS).

We had our intensive work on automated testing and debugging for the path planning function in ADS via simulation. Multiple requirements need to be satisfied such as safety, comfort, and compliance with traffic rules. Violations may occur in very specific traffic scenarios or simulator configurations such as positions of other cars. Our technical approach is to make use of automated testing and debugging techniques, originally for program code, by adapting them to the continuous and uncertain ADS problems. We employed search-based testing techniques to explore simulation configurations that lead to violations, e.g., [1]. We also applied fault localization techniques to analyze possible causes of detected violations [2]. Our techniques were evaluated with a simulator provided by our partner Mazda.

To complement these heuristics or search-based approaches, we are also working on a formal approach called Responsibility-Sensitive Safety (RSS). Intuitively, RSS is an approach to define rules such that no crash occurs if all the traffic participants obey them. We formulated RSS with Hoare-like pre-post decomposition and made a case study of refinement-based safety verification with the Event-B formalism for ADS that switches between a black-box AI-based controller and a conservative safe controller [4].

These studies have considered the control aspect of ADS while the emerging difficulties lie in the perception aspect, especially using deep neural networks (DNN). After interviews with industrial partners, our “Engineerable AI” project tackles the problem of safety-aware DNN update. We may want to “fix” our DNN component to mitigate the risk by specific errors, e.g., misclassifying pedestrian to something else. However, re-training with additional dataset can shuffle the millions of DNN parameters. We may not have intended improvement or even have unintended degradation for other error types. We defined benchmarks with our industry partners that evaluate many (10+) of fine-grained safety metrics for the prediction performance. We are tackling them by unique techniques to apply fault localization techniques to identify “suspicious neurons” in DNN for safety-aware, regression controlled update, e.g., [3].

We believe integrating these heterogeneous approaches is essential to deal with complexity and uncertainty of safety-critical CPS such as ADS.

Capturing both aleatoric and epistemic uncertainty in models of robotic systems is crucial to designing safe controllers. Most existing approaches for synthesizing certifiably safe controllers exclusively consider aleatoric but not epistemic uncertainty, thus requiring that model parameters and disturbances are known precisely. We present a novel abstraction-based controller synthesis method for continuous-state models with stochastic noise, uncertain parameters, and external disturbances. By sampling techniques and robust analysis, we capture both aleatoric and epistemic uncertainty, with a user-specified confidence level, in the transition probability intervals of a so-called interval Markov decision process (iMDP). We then synthesize an optimal policy on this abstract iMDP, which translates (with the specified confidence level) to a feedback controller for the continuous model, with the same performance guarantees. Our experimental benchmarks confirm that accounting for epistemic uncertainty leads to controllers that are more robust against variations in parameter values.

Digital twins are currently revolutionizing industry [9] and are entering into the world of medicine (e.g., [7]) and natural science (e.g., [1]). A digital twin is an information system that analyzes the behavior of a physical or cyber-physical system by connecting streams of observations of this twinned system to dynamic (e.g., simulation) and static (e.g., asset management) models. In complex settings, the digital twin will often need to manage several models that reflect different subsystems or different aspects of the twinned system. To analyze such complex systems, digital twins must ensure the correct composition of these models. However, the composition problem for models in digital twins remains unresolved [8]; e.g., models may be at different levels of abstraction, at different granularities or scales, and use different modeling concepts.

In this talk, we discuss this problem for digital twins, with a focus on the composition of heterogeneous dynamic models. For the integration and transfer of information between sub-systems, digital twins may profit from a formalization of domain knowledge using ontologies, which has proven effective to unify data models. We have started to explore this approach to correctness and compositionality in digital twins by combining formalized asset models [2] with dynamic behavioral models [4, 6]. This has been done in the context of SMOL [5], a small object-oriented orchestration language⁶⁶6https://smolang.org/ which can (a) dynamically create models and integrate them into a program and (b) lift the runtime configuration of a program into a static asset model which can be queried from inside the programs using semantic technologies [3].

Cyber-Physical Systems (CPS) are increasingly incorporating what one can call Learning- Enabled Components (LEC) to implement complex functions. By LEC we mean a component (typically, but not exclusively, implemented in software) that is realized with the help of data-driven techniques, like machine learning. For example, an LEC in an autonomous car can implement a lane follower function such that one trains an appropriate convolutional neural network with a stream of images of the road as input and the observed actions of a human driver as output. The claim is that such LEC built via supervised learning is easier to implement than building a very complex, image processing driven control system that steers the car such that it stays on the road. In other words, if the straightforward design and engineering is too difficult, a neural network can do the job – after sufficient amount of training. For high-consequence systems the challenge is to prove that the resulting system is safe: it does no harm, and it is live: it accomplishes its goals. Safety is perhaps the foremost problem in autonomous vehicles, especially for ones that operate in a less-regulated environment, like the road network. The traditional technology for proving the safety of systems is based on extensively documented but often informal arguments – that are very hard to apply to CPS with LEC. The talk will focus on a recent project that aims at changing this paradigm by introducing (1) verification techniques whenever possible (including proving properties of the “learned” component), (2) monitoring technology for assurance to indicate when the LEC is not peforming well, and (3) formalizing the safety case argumentation process so that it can be dynamically evaluated. The application target is autonomous vehicles, with significant, but not exclusively used LECs. The goal is to construct an engineering process and a supporting toolchain that can be used for the systematic assurance of CPS with LECs.

A well-known rule says that the sooner a problem is identified in the development process, the better it is for the success of a project, its costs, time delivery and residual default rate. That is why requirements engineering (RE) is getting higher responsibility in the development of systems. RE, always, has to manage some tradeoffs between methods, languages, models and tools to capture well the initial goals defined in a natural language and the need to produce a clear, complete, unambiguous model of the specification for design and implementation phases. On the other hand, when developing critical systems, formal methods are used to strengthen the development process and to increase the level of confidence of the final product. In the last decade, several research works have been developed to combine requirements engineering and formal methods, mainly for software or embedded systems. Cyber-Physical Systems (CPS) combine interconnected computational and physical elements, possibly including human interactions. They are most often critical systems, especially in industrial domains like automotive, aeronautics, space, energy, medical, etc. Clearly, RE for CPS is more complex than RE for traditional embedded or software systems. Indeed, CPS design necessarily involves different engineering disciplines, such as mechanical, electrical, software engineering, relying on different sets of modeling languages. Similarly, different kinds of formal methods (e.g. logic for computational components, differential calculus for physical components) are essential to verify critical requirements such as consistency, safety, security, reliability, performance, while taking into account requirements involved by human interactions. In this talk I will introduce some of the challenges surrounding the modeling and verification of requirements for CPS through an illustrative example of a road transportation system.

This presentation demonstrated the personal journey moving from formal modelling to using such models to realise digital twins for Cyber-Physical Systems (CPSs). There are many considerations that needs to be considered in order to make such a journey successful and many of these involve interdisciplinary engineering and research. Coupling models together with different mathematical backgrounds we are conducting using co-simulation. Here it is important to note that many mathematically-based models of the physical phenomena does not just have an anlytic solution and thus when simulating such models we get approximations, and these are not necessarily refinements of each other (and many of them need to be calibrated to be close to what happens in reality). Another challenge that needs to be overcome is the fact that receiving data from the physical system can be a complicated process and this will also result in discretations with approximations of the real values (e.g. due to noise). In case data is received wirelessly there will also be a time delay and this matters in a digital twin setting, in particular if one wish to control the physical twin from the digital side. Being able to estimate the state (and state transitions) of a physical twin can also be challenging when it needs to be done purely on the data that is accessible from the outside. Finally, since the models of a CPS will never be having a behaviour which will be identical to the physical system, so it is likely that there will be drifting and thus one will need to calibrate the models once in a while and determining when and how to do this is also not obvious.

This presentation reports on the return of experience collected during the last two decades, while applying formal methods for software-based safety critical systems, from design to exploitation. These systems, legacy or brand new, are in close contact with people. Forthcoming systems have to be analysed through a huge number of dimensions (safety, security, cybersecurity, AI, autonomy, etc.). Who is going to specify, design, V&V, certify, qualify them ? We need tools, standards, and people to achieve this – people from the 30% of the population, able to use abstraction, are required. Target customers are those who do not sleep well at night – the financial argument (FM are going to save money) is quite usually ignored.

ProB has been developed over around 20 years and was initially developed in SICStus Prolog. In this talk I will discuss various lessons learned over this period, touching development, maintenance, certification and reaching industrial users.

This talk discusses a range of verification and validation approaches employed by the research team at NASA Langley for the analysis of new automated navigation systems for general aviation. Concrete examples will be given based on Detect-And-Avoid (DAA) systems. DAA is the capability of an aircraft to remain well clear of other aircraft and avoid collisions. The idea behind DAA is to define a safe region around the aircraft and use the current position and velocity vector of the aircraft to compute possible route conflicts with other aircraft flying nearby. DAA was originally created for Unmanned Aerial Vehicles (UAVs). The research team at NASA Langley has created a reference implementation of a DAA system [1], and is now adapting the DAA concept to manned aircraft. The ultimate goal is to create a technology that can be used by pilots in the cockpit to enhance traffic awareness and support maneuver guidance when required to comply with see and avoid regulations [2]. This research is carried out within NASA’s Air Traffic Management Exploration (ATM-X) project [3], which is looking into the future of airspace operations and services.

Generative engineering is a new paradigm for developing cyber-physical systems. Rather than developing, increasingly more detailed model of a system, multiple architectural system variants are computationally generated and evaluated, which would be prohibitively expensive to do by hand. The components and parameters that make up this system model optionally maps to library components in various simulations and analytics tools, with architectural models for those tools then automatically generated. This methodology was successfully applied to different use cases, from vehicle transmission design and hybrid vehicles to safety in avionics.

This talk highlights some of the most fascinating aspects of the logic of dynamical systems which constitute the foundation for developing cyber-physical systems (CPS) such as robots, cars and aircraft with the mathematical rigor that their safety-critical nature demands. Differential dynamic logic (dL) provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. In dL, properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics.

In addition to providing a strong theoretical foundation for CPS, differential dynamic logics as implemented in the KeYmaera X prover have been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robotic system for skull-base surgery. dL is the foundation to provable safety transfer from models to CPS implementations and is also the key ingredient behind autonomous dynamical systems for Safe AI in CPS.

This invited talk offers inspiration from the significant history of successful integration of formal methods into NASA projects. We highlight the differences between software and flight software, overview lessons learned from practical experience, and identify the limits of, and future challenges for, formal verification of aerospace systems. After drawing on examples from design-time verification of automated Air Traffic Control and runtime verification on-board Robonaut2, we visit the current full-system-lifecycle verification plans published for the NASA Lunar Gateway. We conclude with a collection of real-life, full-scale, open-source resources for the formal methods research community.

Our world has become a network of connected software systems, communicating with each other, and controlling physical systems. We have autonomous cars driving around, interoperable medical devices monitoring and controlling the health of patients and collaborating robots interacting with humans without separating fences. These systems are generally concurrent, distributed, and dynamic, with critical timing properties.

I will present our approach for analysis of timing properties of interoperable systems, using actor models and formal verification. Rebeca was designed more than 20 years ago as an imperative actor-based language with the goal of providing an easy-to-use language for modelling concurrent and distributed systems, with formal verification support. It was extended a few years later to support modelling real-time network and computational delays, periodic events, and required deadlines; and then extended to Hybrid Rebeca to support hybrid systems.

At the dagstuhl, I will briefly present our work that may be of interest for the audience. I will reflect on how we used Rebeca, its extensions, and its toolset for timing analysis and safety assurance of different systems, for example sensor network applications, and medical interoperable systems. I will present Hybrid Rebeca and our design decisions in extending Rebeca to support hybrid systems. I will present our work on model checking CPS by connecting Timed Rebeca and Lingua Franca (of Edward Lee from UC Berkeley). I will also explain our work on anomaly detection of CPS using formal verification at design time, and runtime monitoring during operation using an abstract digital twin that we call Tiny Twin.

The talk tackled the question “Can we achieve the safety & dependability we need for extremely complex systems of systems that combine hardware & software, and may even include machine learning components?” I presented my personal wish list for techniques and approaches that I believe can help us answer the question in the affirmative.

Top of my wish list is “Incremental Product Family Assurance” to complement “Incremental Product Family Development”, which I think is already well established. To support this we need effective and practical “Change Impact Analysis & Bi-directional traceability”. I presented our work on the Workflow+ modeling framework as one approach that can help in this regard.

I also presented 8 Support Wishes ranging from “Systematic Methods To Explore Emergent Behaviour” to “Integrated Methods”, with an emphasis on Model Driven Engineering. I ended the presentation with 5 Foundational Wishes ranging from “Separation Of Concerns” to “[building the] Assurance Case Before Start [of development]”.

There are many challenges to the satisfactory operation of cyber-physical systems (CPSs). They include architectural issues, real-time properties, human interaction, autonomy, privacy, safety, security, and uncertainty. Researchers who have analysed CPSs cite problems linked to security and uncertainty as the most common causes of failure [1]. We focus on uncertainty, a lack of knowledge about a system’s state.

Computer scientists have proposed several formalisms for dealing with uncertainty. Probabilistic and statistical model checkers, such as Prism [5] and Storm [4], analyse a range of semantic models for these formalisms. These include discrete and continuous-time Markov chains and their nondeterministic extensions. These tools are good at interoperability. Verification-oriented formalisms include the following: Hehner’s probabilistic predicative programming [3], the conditional probabilistic guarded command language [7], probabilistic Hoare logic [2], and partially observable Markov decision processes [6].

Research on describing and analysing uncertainty raises many questions. What does a unifying theory for uncertainty look like? What are the connections between semantics and tools that support the different approaches? Can we establish more connections? Can we support probabilistic and statistical model checking with theorem proving? Contrariwise, can we support theorem proving with probabilistic and statistical model checking? Can we establish uncertainty properties using correctness by construction? What about probabilistic refinement-based model checking? Can we qualify one analysis tool (as in DO-178C) and then map soundly into that tool for high assurance? What is the formal testing theory for a CPS with (say) unknown MDP semantics? What are the testability hypotheses (in Gaudel’s sense)? How do we exploit the interplay between testing, proof, and model checking? What about uncertainty modelling and runtime verification? What role can unifying uncertainty formalisms and tools play in the development, application, and evaluation of CPSs?

We describe some preliminary work towards answering these questions.