A Holistic Model-Based Approach to Design, Verification and Diagnosis of Cyber Physical Systems
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.