Advancing Simulation-Based Verification Techniques to Multi-Models of Cyber-Physical Systems

Cyber-Physical Systems (CPSs) are a combination of physical and computational processes. Larger distributed CPSs, such as those found in the automotive industry, electrical grid or rail networks, have a vast number of physical and computational process. Often larger CPSs often have a collaboration of companies/research groups working together each providing process to the complete CPSs. This introduces challenges with design and verification of the complete CPS. Protection of Intellectual Property (IP) from collaborator to collaborator and the combination of different model types are the 2 main design problems.

Functional Mock-up Interface (FMI) was designed to solve the design issues associated with CPSs. Introducing a framework for sub models as Functional Mock-up Units and how these FMUs can be simulated together as one complete CPS. FMUs are black box models which enables collaborators to share models without giving away their Intellectual Property and their interface is standardised across a multitude of different model types such as Continuous Time, Discrete Event, Hybrid Automata, or other types.

This project aims to address the problems associated with safety Verification of CPSs, addressing those that arise from Co-Simulation frameworks such as FMI. The introduction of black box models and a standard interface for them makes verification of a complete CPS difficult. It's impossible to apply Proof Obligation (PO) when the functions (in this case models) are unknown because PO works by slowly unfolding the functions into smaller solvable proofs. The method of verification that could be applied is a form of Simulation Based Verification. Using a calculated expansion function, it is possible to create an over approximation of a reach set given a central simulation of the initial state space. This over approximation can then be compared against the set of predetermined unsafe sates of the CPS. If the central simulation intersects the bad states, then the CPS is unsafe. If the over approximated reach set intersects then refine the initial state space and produce a smaller over approximation of the reach set. If the over approximation doesn't intersect the bad states, then the CPS is safe. The calculation of expansion function is the primary research goal for this project as complex CPS make it harder to calculate the expansion function.