An UPPAAL Model for Formal Verification of Master/Slave Clock Synchronization over the Controller Area Network

Many distributed applications require a clock synchro-nization service. We have previously proposed a clock synchronization service for the Controller Area Network (CAN), which we have claimed to provide highly synchro-nized clocks even in the occurrence of faults in the system. In this paper we substantiate this claim by providing a for-mal model and verification of our fault tolerant clock syn-chronization mechanism. We base our modeling and ver-ification on timed automata theory as implemented by the model checking tool UPPAAL. In the modeling we intro-duce a novel technique for modeling drifting clocks. The verification shows that a precision in the order of 2 µs is guaranteed despite node’s faults as well as consistent channel faults. It also shows that inconsistent channel faults may significantly worsen the achievable precision, but that this effect can be reduced by choosing a suitable resynchronization period. 1