Using UPPAAL to model and verify a clock synchronization protocol for the controller area network

A reported liability of the controller area network protocol is that it does not provide a clock synchronization service. Therefore, whenever a CAN-based distributed embedded system requires its nodes to have a common time base, clock synchronization has to be implemented by means of an external mechanism. In a previous work, we proposed a fault-tolerant and high-precision clock synchronization protocol for CAN. This paper shows the first steps towards the formal verification of this protocol. In particular, it presents a formal model that has been built with the UPPAAL model checker and discusses how clock drift and clock correction can be modeled with this tool