November 14, 2016Ocan Sankur (IRISA CNRS)
We consider distributed timed systems that implement leader
election protocols which are at the heart of clock synchronization proto-
cols. We develop abstraction techniques for parameterized model check-
ing of such protocols under arbitrary network topologies, where nodes
have independently evolving clocks. We apply our technique for model
checking the root election part of the flooding time synchronisation pro-
tocol (FTSP), and obtain improved results compared to previous work.
We model check the protocol for all topologies in which the distance to
the node to be elected leader is bounded by a given parameter.