We propose novel methods and tools to support System Level Formal Verification (SLFV) of Cyber Physical Systems (CPSs).
Our approach has the following features.
First, it takes as input a CPS defined as a network of Functional Mock-up Units (FMUs) and exploits knowledge of the system structure to counteract state explosion. Addressing FMUs is useful since large CPSs (e.g., those found in automotive or avionics) are often defined as a network of FMUs.
Second, it supports at the same time design of system parameters, evaluation of how well the system meets its requirements (verification) and debugging (by identifying the faulty sub-system).
Third, it supports reuse of the computation activity of previous failed verification attempts. Since during the design activity most verifications fail, reuse greatly reduces verification time.
Fourth, it effectively exploits large computer clusters thereby decreasing verification time.
We shortly outline the state of the art for CPS verification.
Simulation-Based Approaches to CPS Falsification - Simulation based falsification methods for Simulink models have been investigated, e.g. [1, 13]. Using a Monte Carlo-style random sampling, such approaches search, among a finite set of system initial states, one that falsifies a given specification. The main differences wrt our envisaged approach are:
1. We exploit knowledge of the system structure to counteract state explosion, whereas the approaches in [1, 13] rest on random sampling.
2. We aim at proving system correctness, thus we focus on generating the set of initial states that satisfies the given specifications, rather than on proving that the system contains a design error.
3. When specifications are not satisfied, we provide the set of sub-systems containing a design error.
4. When initial states model also system parameters, our approach supports system design by computing a set of system parameters satisfying the given specifications.
Simulation-Based Approaches to CPS Verification - Simulation based formal verification for Simulink models have been investigated, e.g. [5, 6, 7, 8]. Such research work presents a simulation-based parallel approach to SLFV for CPSs, realized by decoupling the computation of the set of system runs (scenarios) from their actual simulation. This enables optimisation of the simulation activity by:
1. identifying prefixes of scenarios occurring more than once within the set of scenarios;
2. saving the simulation state reached after any such prefix;
3. restoring the simulation state when such a prefix occurs again to avoid to carry out the same computation. Since, within such HILS setting, simulation takes about 99% of the verification time, such an optimisation substantially reduces the overall time.
Formal verification of Discrete Time Simulink Models - Formal verification of Simulink models has been investigated, e.g. [10, 9, 11]. Such methods focus on discrete time models with small domain variables. Therefore, they are well-suited to analyse critical sub-systems, but cannot handle complex system level verification tasks (which is our goal). This is the motivation for the development of statistical model checking methods as those in [3, 12], as well as for the exhaustive HILS based approach.
Formal verification of Annotated Simulink Models - Annotated models comprising both discrete and continuous variables can be analysed with simulation based tools like C2E2 [4]. We differ from C2E2 by providing a black-box approach that does not require model annotations.
Summing up, the main differences of the above approaches wrt our approach are:
- We address formal verification as well synthesis of system parameters, instead of focusing only on falsification or formal verification;
- We handle any class of systems, instead of focusing only on discrete time models;
- We handle black-box models instead of requiring annotated white-box models,
- Our diagnostic information consists of counter-examples as well as identification of faulty sub-systems, instead of only counter-examples.
[1] H. Abbas, G. Fainekos, S. Sankaranarayanan, F. Ivancic, A. Gupta. Probabilistic temporal logic falsification of cyber-physical systems. ACM TECS, 2013
[2] R. Alur. Formal verification of hybrid systems. Proc. EMSOFT 2011
[3] E.M. Clarke, A. Donzé, A. Legay. On simulation-based probabilistic model checking of mixed-analog circuits. Form. Meth. Sys. Des., 2010
[4] P.S. Duggirala, S. Mitra, M. Viswanathan, M. Potok. C2E2: A verification tool for stateflow models. Proc. TACAS 2015
[5] T. Mancini, F. Mari, A. Massini, I. Melatti, F. Merli, E. Tronci. System level formal verification via model checking driven simulation. Proc. CAV 2013
[6] T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci. System level formal verification via distributed multi-core hardware in the loop simulation. Proc. PDP 2014
[7] T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci. Anytime system level verification via parallel random exhaustive hardware in the loop simulation. MicPro, 2016
[8] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. SyLVaaS: System level formal verification as a service. Fundam. Inform., 2016
[9] B. Meenakshi, A. Bhatnagar, S. Roy. Tool for translating Simulink models into input language of a model checker. Proc. ICFEM 2006
[10] S. Tripakis, C. Sofronis, P. Caspi, A. Curic. Translating discrete-time Simulink to Lustre. ACM TECS, 4(4): 2005
[11] M.W. Whalen, D.D. Cofer, S.P. Miller, B.H. Krogh, W. Storm. Integration of formal analysis into a model-based software development process. Proc. FMICS 2007
[12] P. Zuliani, A. Platzer, and E.M. Clarke. Bayesian statistical model checking with application to Stateflow/Simulink verification. Form. Meth. Sys. Des., 2013
[13] A. Zutshi, S. Sankaranarayanan, J.V. Deshmukh, and X. Jin. Symbolic-numeric reachability analysis of closed-loop control software. Proc. HSCC 2016