Titolo della tesi: Methods and tools for design and verification of Intelligent Systems
Model-based approaches promote a revolutionary and radical turn to reduce the time and cost of verifying and designing Intelligent Systems (ISs). Real-world systems are represented through accurate models usually defined by easily thousands of equations, making them not amenable to mathematical solutions or techniques based on exhaustive exploration of the state space.
Such complexity can be mitigated by means of computer simulations, with system models available as black boxes. Despite that, simulation-based verification and design of ISs remain challenging. Both tasks are based on evaluating all operational scenarios, i.e., all time sequences of disturbances which can possibly materialise. Simulation-based verification aims to formally guarantee that the system specifications are met for all scenarios, whilst simulation-based design focuses on exploring all possible system design configurations to be considered and, in turn, formally verified, leading to combinatorial explosions in the number of scenarios and the number of system design configurations.
Statistical Model Checking (SMC) and Black-Box Optimisation (BBO) are potential solutions to scale up simulation-based verification and design. SMC enables the random evaluation of operational scenarios until given statistical assurances are achieved. BBO is based on the objective function and/or constraints given as black boxes and is particularly suitable when a simulator guides optimisation.
In this thesis, we advance the state of the art of orchestrating simulation, Statistical Model Checking and Black-Box Optimisation in the following directions.
First, we present a method and tool to scale up SMC-driven formal verification of Cyber-Physical Systems (CPSs). Our methodology is based on a novel SMC algorithm that concurrently advances a finite set of approximation algorithms so that the approximation provided by the algorithm requiring the minimum number of samples can be output. Thus, we developed a highly parallel infrastructure that uses High-Performance Computing (HPC) platforms and our novel algorithm to minimise and effectively scale up all computer simulations.
Second, in the context of industrial control systems, we show an algorithm to carry out the simulation-based design with formal guarantees. Our algorithm iteratively alternates BBO and SMC phases to output system controls as formally certified Quality Guaranteed (QG) solutions. The design algorithm ensures that, with probability 1 − δ, the probability that a scenario for which the system exhibits an error materialises with a QG control is less than ε.
Finally, in the context of personalised medicine, we present a method and tool to design personalised therapies for a given human subject on the patient’s Digital Twin (DT) with formal guarantees. Our tool orchestrates a two-level nested BBO search with an SMC therapy verifier to output Pareto-optimal personalised therapies. Our method is interested in tolerating a certain probability of failure when the treatment is administered.