Cyber-Physical Systems (CPSs), comprising both software and physical components, arise in many industry-relevant domains and are often mission- or safety-critical. System-Level Verification (SLV) of CPSs aims at certifying that given (e.g., safety or liveness) specifications are met, or at estimating the value of some Key Performance Indicators, when the system runs in its operational environment, that is in presence of inputs and/or of additional, uncontrolled disturbances. To enable SLV of complex systems from the early design phases, the currently most adopted approach envisions thesimulationof asystem modelunder the (time bounded)operational scenariosdeemed of interest. Unfortunately, simulation-based SLV can be computationally prohibitive (years of sequential simulation), since system model simulation is computationally intensive and the set of scenarios of interest can be extremely large. In this article, we present a technique that, given a collection of scenarios of interest (extracted from databases or from symbolic structures), computesparallel shortest simulation campaigns, which drive a possibly large number of system model simulators running in parallel in a HPC infrastructure through all (and only) those scenarios in the user-defined (possibly random) order, by wisely avoiding multiple simulations of repeated trajectories, thus minimising completion time. Our experiments on SLV of Modelica/FMU and Simulink models with up to almost200 million scenariosshow that our optimisation yieldsspeedups as high as8$\boldsymbol{\times}$. This, together with the enabledmassive parallelisation, makes practically viable (a few weeks in a HPC infrastructure) verification tasks (both statistical and exhaustive) which would otherwise takeinconceivablylong time.

Model-basedapproaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely onnumerical simulationof the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying givenconstraints. Such constraints typically stem fromrequirements(orassumptions) on the SUV inputs and itsoperational environmentas well as from the enforcement ofadditional conditionsaiming at, e.g.,prioritisingthe (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercisingselectedrequirements, or avoidingvacuityin their satisfaction. In this setting, the possibility toefficiently sample at random(with a known distribution, e.g., uniformly) within, or to efficientlyenumerate(possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in generalfailin extracting scenarios according to a given distribution (e.g., uniformly), and can bevery inefficientto produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiplefinite memory monitors, a data structure (scenario generator) can be synthesised, from whichany-horizon scenariossatisfying the input constraints can beefficientlyextracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enablesseamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking.

In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes. As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variations in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by c onsidering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to (Hardware In the Loop Simulation based) System Level Formal Verification. SyLVaaS takes as input a finite state automaton defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion (i.e., with no communication among the parallel processes) on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. As the actual simulation is carried out at the user premises (e.g., on a private cluster), SyLVaaS allows full Intellectual Property protection of the SUV model as well as of the user verification flow. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on case studies consisting of input operational environments entailing up to 35 641 501 scenarios related to the system level verification of models from the Simulink distribution (namely, Inverted Pendulum on a Cart and Fuel Control System).

The SmartHG project goal is to develop a suite of integrated software services (the SmartHG Platform) aiming at steering residential users energy demand in order to: keep operating conditions of the electrical grid within given healthy bounds, minimize energy costs, and minimize CO2 emissions. This is achieved by exploiting knowledge (demand awareness) of electrical energy prosumption of residential users as gained from SmartHG sensing and communication infrastructure. This paper describes such an infrastructure along with user demand patterns emerging from the data gathered from ~600 sensors installed in ~40 homes participating in SmartHG test-beds.

In order to optimally manage a modern electricity distribution network, peaks in residential users demand should be avoided, as this can reduce energy and network asset management costs. Furthermore, this must be done without compressing residential users demand. To this aim, in a demand response setting, residential users are given a price policy, which economically motivates them to shift their loads in order to achieve this goal. However, if the price policy for all users is similar, this demand response may result in simply shifting the demand peaks (peak rebound), leaving the problem unsolved. In this paper we propose a novel methodology which i) for each network substation s, automatically computes the desired power profile to be kept in order to optimally manage the network itself, ii) for each network substation s, automatically synthesizes individualized price policies for residential users connected to s, so that s is kept at the desired profile. Note that price policies individualization avoids the peak rebound problem, as different users have different low tariff areas. Furthermore, our methodology measures the flexibility of a residential user as the capacity needed by a home energy storage system (e.g., a battery) to always follow the given price policy, thus mitigating residential users discomfort. We show the feasibility of our approach on a realistic scenario taken from an existing medium voltage Danish distribution network.

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to the verification problem outlined above. SyLVaaS takes as input a high-level model defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. As the actual simulation is carried out at the user premises (e.g., in a private cluster), SyLVaaS allows full Intellectual Property protection on the SUV model and the user verification flow. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on industry-scale input related to the verification of the Fuel Control System (FCS) model in the Simulink distribution.

We present a parallel random exhaustive Hardware In the Loop Simulation based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on System Level Formal Verification of the Fuel Control System example in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability.

One of the main goals of systems biology models in a health-care context is to individualise models in order to compute patient-specific predictions for the time evolution of species (e.g., hormones) concentrations. In this paper we present a statistical model checking based approach that, given an inter-patient model and a few clinical measurements, computes a value for the model parameter vector (model individualisation) that, with high confidence, is a global minimum for the function evaluating the mismatch between the model predictions and the available measurements. We evaluate effectiveness of the proposed approach by presenting experimental results on using the GynCycle model (describing the feedback mechanisms regulating a number of reproductive hormones) to compute patient-specific predictions for the time evolution of blood concentrations of E2 (Estradiol), P4 (Progesterone), FSH (Follicle-Stimulating Hormone) and LH (Luteinizing Hormone) after a certain number of clinical measurements.

The goal of System Level Formal Verification (SLFV) is to show system correctness notwithstanding uncontrollable events (such as: faults, variation in system parameters, external inputs, etc). Hardware In the Loop Simulation (HILS) based SLFV attains such a goal by considering exhaustively all relevant simulation scenarios. We present a distributed multi-core algorithm for HILS-based SLFV. Our experimental results on the Fuel Control System example in the Simulink distribution show that by using 64 machines with an 8 core processor each we can complete the SLFV activity in about 27 hours whereas a sequential approach would require more than 200 days. To the best of our knowledge this is the first time that a distributed multi-core algorithm for HILS-based SLFV is presented.

Many embedded systems are indeed software-based control systems , that is, control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on formal model-based design approaches for automatic synthesis of embedded systems control software. We present an algorithm, along with a tool QKS implementing it, that from a formal model (as a discrete-time linear hybrid system ) of the controlled system ( plant ), implementation specifications (that is, number of bits in the Analog-to-Digital , AD, conversion) and system-level formal specifications (that is, safety and liveness requirements for the closed loop system ) returns correct-by-construction control software that has a Worst-Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications. We show feasibility of our approach by presenting experimental results on using it to synthesize control software for a buck DC-DC converter, a widely used mixed-mode analog circuit, and for the inverted pendulum.

Many Embedded Systems are indeed Software Based Control Systems (SBCSs), that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for control software. Given the formal model of a plant as a Discrete Time Linear Hybrid System and the implementation specifications (that is, number of bits in the Analog-to-Digital (AD) conversion) correct-by-construction control software can be automatically generated from System Level Formal Specifications of the closed loop system (that is, safety and liveness requirements), by computing a suitable finite abstraction of the plant.

The automation of power grids by means of supervisory control and data acquisition (SCADA) systems has led to an improvement of power grid operations and functionalities but also to pervasive cyber interdependencies between power grids and telecommunication networks. Many power grid services are increasingly depending upon the adequate functionality of SCADA system which in turn strictly depends on the adequate functionality of its communication infrastructure. We propose to tackle the SCADA risk analysis by means of different and heterogeneous modeling techniques and software tools. We demonstrate the applicability of our approach through a case study on an actual SCADA system for an electrical power distribution grid. The modeling techniques we discuss aim at providing a probabilistic dependability analysis, followed by a worst case analysis in presence of malicious attacks and a real-time performance evaluation.

We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling multiple administrative domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms.

One of the most succesfull approach to automatic software verification is SAT based Bounded Model Checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC.