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.
