This project focuses on the formal design of semi-autonomous automotive Cyber Physical Systems (CPS). Rather than disconnecting the driver from the vehicle, the goal is to obtain a vehicle where the degree of autonomy is continuously changed in real-time as a function of certified uncertainty ranges for driver behavior and environment reconstruction. The highly integrated research plan will advance the science and engineering for CPS by developing methods for (1) reconstructing 3D scenes which incorporate high-level topological and low-level metric information, (2) extracting driver behavioral models from large datasets using geometry, reasoning and inferences, (3) designing provably-safe control schemes which trade-off real-time feasibility and conservatism by using the evidence collected during actual driving. Assisting humans in controlling complex and safety-critical systems is a global challenge. In order to improve the safety of human-operated CPS we need to provide guarantees in the reconstruction of the environment where the humans and the CPS operate, and to develop control systems that use predictive cognitive models of the human when interacting with the CPS. A successful and integrated research in both areas will impact not only the automotive sector but many other human-operated systems. These include telesurgery, homeland security, assisted rehabilitation, power networks, environmental monitoring, and all transportation CPS. Graduate, undergraduate and underrepresented engineering students will benefit through classroom instruction, involvement in the research and a continuous interaction with industrial partners who are leaders in the field of assisted driving.

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.