Formal Verification of a Clock Synchronization Method in a Distributed Automotive System
Peter Böhm
Abstract
This thesis presents the formal verification of a clock synchronization algorithm in a distributed communication system. The communication system is inspired by the demands of the automotive industry and based on the FlexRay standard. The work is part of the Verisoft automotive subproject. The distributed system consists of hosts interconnected via a communication bus. We introduce a schedule that provides deterministic communication delays based on a clock synchronization algorithm which deals with clock drift. We present the hardware specification of the bus controller parts related to the scheduling correctness. Furthermore, we extend the formalism from knapppaul to state the correctness theorem in a clean mathematical way. This formalism also involves theories about asynchronous communication. Finally, we present a mathematical-style proof for the correctness of the clock synchronization mechanism and introduce the principles behind the straight forward formalization of this proof which we have carried out in the Isabelle/HOL theorem prover.