An Abstraction Technique for Parameterized Verification of Leader Election Protocols: Application to Flooding Time Synchronization Protocol

We consider distributed timed systems that implement leader election protocols which are at the heart of clock synchronization protocols. We develop abstraction techniques for parameterized model checking of such protocols under arbitrary network topologies, where nodes have independently evolving clocks. We implemented our technique within NuSMV and applied it to model check the root election part of the flooding time synchronisation protocol (FTSP), and obtained significantly improved results compared to previous work. We were able to verify the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter. Joint work with J.-P. Talpin.