CPS: Breakthrough: Safe Protocols in Cyber-Physical Systems (CPS)

本研究的目的是证明网络物理系统在部署之前是安全的。本研究调查的方法是用于测试通信协议的方法的扩展。网络物理系统的问题是：1)它们比通信协议复杂得多；2)时间是这些系统的一个更关键的组成部分；3)在竞争环境中，可能有许多必须互操作的实现。通过使用分层体系结构，降低了通信协议的复杂性。每一层为下一层提供定义良好的服务。这项研究正在开发反映网络物理系统与物理世界相互作用的不同方式的多维体系结构。这些技术在驾驶员辅助合并协议上进行了评估。合并协议的体系结构有四个维度，组织为通信、外部传感器、车辆监视和控制以及定时的堆栈。这个体系结构在标准化过程中也很有用。定时通过增加潜在执行路径的数量来增加验证的复杂性。本课题的研究探讨了如何通过同步时钟和使用同步操作来减少路径的数量。这种方法是合理的，因为现在GPS的定时精度是可用的。使用两步验证过程来创建网络物理系统的明确模型，首先证明模型是安全的，然后检查每个实现是否符合模型。这减少了三方合并协议的测试数量和成本。具体来说，假设不同的制造商和型号有N个实现版本，这种方法减少了必要的交互测试的数量，这将是N个立方，到一个模型验证和N个一致性测试。

The objective of this research is to prove that cyber-physical systems are safe before they are deployed. The approaches the research investigates are extensions of approaches used to test communications protocols. The problems with cyber-physical systems are that 1) they are much more complicated than communications protocols, 2) time is a more critical component of these systems, and 3) in a competitive environment there are likely to be many implementations that must interoperate.The complexity of communications protocols is reduced by using a layered architecture. Each layer provides a well defined service to the next layer. This research is developing multi-dimensional architectures that reflect the different ways that the cyber-physical system interacts with the physical world. The techniques are evaluated on a driver-assisted merge protocol. An architecture for the merge protocol has four dimensions organized as stacks for communications, external sensors, vehicle monitoring and control, and timing. This architecture will also be useful during standardization.Timing increases verification complexity by increasing the number of potential execution paths. The research conducted in this project explores how to reduce the number of paths by synchronizing clocks and using simultaneous operations. This approach is reasonable because of the timing accuracy now available with GPS. A two step verification process is used that creates an unambiguous model of the cyber-physical system, first proving that the model is safe, then checking that each implementation conforms to the model. This reduces the number and cost of tests for a three-party merge protocol. Specifically, assuming there are N implementation versions for different manufacturers and models, this approach reduces the number of necessary interaction tests, which would be cubic in N, to a single model verification and N conformance tests.