A Cyber-physical Systems of Systems (CPSoS) consists of a set of (possibly geographically distributed) networked systems (constituent systems). A constituent system may be itself a Cyber-physical System (CPS), a purely computational system (e.g., software running on a computer), a communication system (e.g., devices supporting wired or wireless communication). Examples of CPSoS are: transport networks (e.g., smart grids, railways, etc), large manufacturing facilities, a swarm of drones or even a single aircraft. In fact, all such systems consists of networked systems controlled by a considerable number of distributed computing elements and, possibly, human users.
Many CPSoS are safety or mission critical system. Accordingly, errors in their design may lead to loss of human life (safety critical systems) or substantial economic losses. The situation is further exacerbated by the ever increasing demand for autonomous behaviour in CPSoS. This state of affairs, together with the never ending aim at decreasing design cost, makes CPSoS design and verification more and more challenging.
This motivates development of methods and software tools to support the design-operation continuum of autonomous CPSoS. Accordingly our project main goal is that of developing algorithms and software tools to improve quality and decrease cost of software development and operations for autonomous CPSoS.
We pursue our project goals through four pillars: 1) Modelling and simulation pillar, aiming at developing our project simulation-based computational infrastructure; 2) Design pillar, aiming at developing software tools to support synthesis and verification of CPSoS coordination software; 3) Operations pillar, aiming at developing software tools to support CPSoS operations; 4) Case studies and evaluation pillar, aiming at assessing our methods and software tools through case studies.
In the following we illustrate how our project methods and software tool will go beyond the state of the art with respect to automatic methods for CPSoS design and verification.
1. Automatic synthesis of functional specifications for CPSoS coordinators from (closed-loop) system-level requirements.
Automatic synthesis of coordination software is an undecidable problem for CPS [A2], so, a fortiori, it is undecidable for CPSoS. Automatic synthesis entails two main steps: first checking if a coordinator satisfying the given requirements exists (realisability); second, synthesise a coordinator (if any).
1.1. Realisability.
Realisability [D9] is rarely addressed in controller synthesis. Non-interference properties [E0] and approximation techniques [D9,E1] reduce synthesis time. As for timed systems, we mention Assume/Guarantee-style reasoning for Input/Output TA [E2] based on modal transition systems [E3] and Lower/Upper-extrapolation [E4]. For other classes of timed systems, constraint-relaxations have shown to be an efficient complete method [E5]. Model-reduction [E6], query-reduction [E7], and partial order-reduction [E6,E8] also improve efficiency, still being complete methods.
Quick and efficient realisability checks via Model-Checking is a significant advancement. Building on modal transition systems, our project will advance not only realisability, but also the synthesis itself, since realisability results could be a performance booster for synthesis.
1.2. Automatic Synthesis of Functional Specification.
Automatic synthesis of correct-by-construction functional specifications that ensure a closed-loop system to meet given safety and/or liveness properties has been widely investigated [E9] by means of symbolic models: the goal is to find a finite abstraction of the system s.t. a controller for the symbolic model defines a controller for the system. Several controllers non-functional requirements have been considered, such as time optimality [F0], code size [F1], and worst case execution time [A5]. To deal with computational complexity of synthesis problems, HPC techniques have been developed [F3]. On-the-fly techniques have been developed to efficiently explore the design space [F4]. Non-linear systems [F5,F6] are usually addressed by imposing restrictions on the system dynamics [F6] or by over-approximating their dynamics by linear systems s.t. controllers for the latter are controllers of the former [F7,A6].
Our project will develop algorithms and tools that: a) can synthesise coordinators accordingly to a given CPSoS architecture (e.g., distributed vs. hierarchical vs. monolithic); b) can handle non-functional requirements (e.g., maximum code size, maximum worst case execution path); and c) enable automatic synthesis for systems that, because of state explosion, cannot be handled by currently available methods and tools.
2. Statistical Model Checking (SMC) based safety and security formal verification.
Despite SMC [F8] aims at finding bugs without too many simulations [F9], often it does not scale-up [G0]. In concurrent systems, the goal of SMC is to optimise the probability to satisfy KPIs: this has been done with learning strategies [G1] even in the case of dynamical systems which requires to re-learn models at execution time [G2]. So far, quantitative objectives have considered Markov chains only [G3]. SMC can be also applied to learn components when only a set of traces is available [G4]. SMC has been used to verify security properties [G5], mainly on homogeneous concurrent systems. SMC on heterogeneous systems [G6] does not consider quantitative aspects so far. Most of current approaches do not consider dynamical aspects, and quantifications over the number of components [G7] have not considered spatial information about components, which is needed for CPSoS.
Our project will advance the state of the art by extending SMC to verify quantitative properties (e.g., Pareto-optimality) with respect to several KPIs, involving spatial information, coordination of heterogenous concurrent systems, dynamic systems, security issues, uncertain environment and learning of partially unknown components.
3. Products and services already available on the market
We note that the currently available code-generation tools (e.g., emmetrix Code Generators, Simulink, Dymola) take as input functional specifications in order to generate code, whereas our synthesis tool chain takes as input models of the CPSoS subsystems, environment and requirements. Closely related to our tool chain are UPPAAL [H1], Pessoa [H2], SCOTS [H3], QKS [H4]. However such tools cannot handle CPSoS: first, none of such tools can automatically target problems where many coordinators have to be synthesised at the same time; second, none of them can handle the complexity entailed by CPSoS; third, none of such tools can take as input non-functional requirements.