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 apply our technique for model checking the root election part of the flooding time synchronisation protocol (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.
CITATION STYLE
Sankur, O., & Talpin, J. P. (2017). An abstraction technique for parameterized model checking of leader election protocols: Application to FTSP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10205 LNCS, pp. 23–40). Springer Verlag. https://doi.org/10.1007/978-3-662-54577-5_2
Mendeley helps you to discover research relevant for your work.