Software Engineering Institute

Cyber-physical systems (CPS) are becoming widespread in many safety-critical real-time applications, such as autonomous driving, robotics systems, and unmanned aircraft. However, verifying these complex real-time systems remains an open challenge because traditional verification techniques are unable to verify all components.

One approach to address this challenge is to use the framework for mixed-trust computing for real-time systems where unverified (untrusted) components are constrained not to exhibit unsafe behavior by verified (trusted) components. This framework increases assurance in the CPS by verifying the timing and functional properties of the trusted components. However, even though the trusted components are verified, formal verification of the synchronization protocol between trusted and untrusted components has been an open problem. If the synchronization protocol between the untrusted and trusted components is incorrect then the behavior of the entire system can be compromised.

In this paper, we present a formal model of a synchronization protocol between trusted and untrusted components using timed automata. We use temporal logic to prove the protocol satisfies properties that guarantee its correctness. The verification was used to identify and correct a critical flaw in the previous protocol implementation and increases confidence in the mixed-trust framework.