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

网络物理系统（CPS）是物理和计算过程的组合。较大的分布式 CPS，例如汽车行业、电网或铁路网络中的 CPS，具有大量的物理和计算过程。通常较大的 CPS 经常有公司/研究小组合作，每个人都为完整的 CPS 提供流程。这给整个 CPS 的设计和验证带来了挑战。合作者之间的知识产权（IP）保护以及不同模型类型的组合是两个主要的设计问题。功能模型接口 (FMI) 旨在解决与 CPS 相关的设计问题。介绍作为功能模型单元的子模型框架，以及如何将这些 FMU 一起模拟为一个完整的 CPS。 FMU 是黑盒模型，使协作者能够在不泄露其知识产权的情况下共享模型，并且其接口在多种不同模型类型（例如连续时间、离散事件、混合自动机或其他类型）中实现标准化。该项目旨在解决与 CPS 安全验证相关的问题，以及 FMI 等联合仿真框架产生的问题。黑盒模型及其标准接口的引入使得验证完整的 CPS 变得困难。当函数（在本例中为模型）未知时，不可能应用证明义务 (PO)，因为 PO 的工作原理是将函数慢慢展开为更小的可解证明。可以应用的验证方法是基于模拟的验证的一种形式。使用计算的扩展函数，可以在给定初始状态空间的中心模拟的情况下创建范围集的过近似。然后可以将该过近似与 CPS 的一组预定不安全状态进行比较。如果中央模拟与不良状态相交，则 CPS 是不安全的。如果过近似的到达集相交，则细化初始状态空间并产生较小的过近似的到达集。如果过近似不与不良状态相交，则 CPS 是安全的。展开函数的计算是本项目的首要研究目标，因为复杂的CPS使得展开函数的计算变得更加困难。

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.