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

信息物理系统（cps）是物理和计算过程的结合。较大的分布式cps，例如在汽车工业、电网或铁路网络中发现的cps，具有大量的物理和计算过程。通常较大的cps通常有公司/研究小组的协作，每个公司/研究小组共同为完整的cps提供流程。这给整个CPS的设计和验证带来了挑战。合作伙伴之间的知识产权保护和不同模式类型的组合是两个主要的设计问题。功能模型接口（FMI）的设计是为了解决与cps相关的设计问题。介绍了子模型作为功能模型单元的框架，以及如何将这些fmu作为一个完整的CPS进行模拟。fmu是黑盒模型，它使协作者能够在不泄露其知识产权的情况下共享模型，并且它们的接口在许多不同的模型类型（如连续时间、离散事件、混合自动机或其他类型）之间进行了标准化。该项目旨在解决与cps安全验证相关的问题，解决由FMI等联合仿真框架产生的问题。黑盒模型及其标准接口的引入使得验证完整的CPS变得困难。当函数（在本例中是模型）未知时，不可能应用证明义务（Proof Obligation， 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.