×

An abstraction technique for parameterized model checking of leader election protocols: application to FTSP. (English) Zbl 1452.68026

Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 23-40 (2017).
Summary: 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.
For the entire collection see [Zbl 1360.68015].

MSC:

68M14 Distributed systems
68M12 Network protocols
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183-235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[2] Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307-309 (1986) · doi:10.1016/0020-0190(86)90071-2
[3] Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT press, Cambridge (2008) · Zbl 1179.68076
[4] Bakhshi, R., Bonnet, F., Fokkink, W., Haverkort, B.: Formal analysis techniques for gossiping protocols. ACM SIGOPS Oper. Syst. Rev. 41(5), 28-36 (2007) · doi:10.1145/1317379.1317385
[5] Bingham, J.: Automatic non-interference lemmas for parameterized model checking. In: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, FMCAD 2008, Piscataway, NJ, USA, pp. 11:1-11:8. IEEE Press (2008)
[6] Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281-283 (1979) · Zbl 0394.68023 · doi:10.1145/359104.359108
[7] Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382-398. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30494-4_27 · Zbl 1117.68423 · doi:10.1007/978-3-540-30494-4_27
[8] Clarke, E., Talupur, M., Veith, H.: Proving ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 33-47. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_4 · Zbl 1134.68403 · doi:10.1007/978-3-540-78800-3_4
[9] Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512-1542 (1994) · doi:10.1145/186025.186051
[10] Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
[11] Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 109-121. Springer, Heidelberg (2013). doi:10.1007/978-3-642-41036-9_11 · Zbl 1355.68175 · doi:10.1007/978-3-642-41036-9_11
[12] Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.C.: Approximate synchrony: an abstraction for distributed almost-synchronous systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 429-448. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_25 · doi:10.1007/978-3-319-21668-3_25
[13] Dolev, D., Klawe, M., Rodeh, M.: An o (n log n) unidirectional distributed algorithm for extrema finding in a circle. J. Algorithms 3(3), 245-260 (1982) · Zbl 0493.68074 · doi:10.1016/0196-6774(82)90023-2
[14] Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1995, pp. 85-94. ACM, New York (1995)
[15] Garavel, H., Mounier, L.: Specification and verification of various distributed leader election algorithms for unidirectional ring networks. Sci. Comput. Program. 29(1), 171-197 (1997) · doi:10.1016/S0167-6423(96)00034-2
[16] John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp. 201-209 (2013)
[17] Fredlund, L., Groote, J.F., Korver, V.: Formal verification of a leader election protocol in process algebra. Theoret. Comput. Sci. 177(2), 459-486 (1997) · Zbl 0911.68057 · doi:10.1016/S0304-3975(96)00256-3
[18] Krstic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: Automated Verification of Infinite State Systems (2005)
[19] Kusy, B., Abdelwahed, S.: FTSP protocol verification using SPIN, May 2006
[20] Maróti, M., Kusy, B., Simon, G., Lédeczi, A.: The flooding time synchronization protocol. In: Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004, pp. 39-49. ACM, New York (2004)
[21] McInnes, A.I.: Model-checking the flooding time synchronization protocol. In: IEEE International Conference on Control and Automation, ICCA 2009, pp. 422-429, December 2009
[22] McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179-195. Springer, Heidelberg (2001). doi:10.1007/3-540-44798-9_17 · Zbl 1002.68674 · doi:10.1007/3-540-44798-9_17
[23] Milner, R.: A Calculus of Communicating Systems. Springer, New York (1982) · Zbl 0452.68027
[24] Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46-57, October 1977
[25] Pnueli, A., Xu, J., Zuck, L.: Liveness with \((0,1, \infty )\)- counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107-122. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_9 · Zbl 1010.68095 · doi:10.1007/3-540-45657-0_9
[26] Sugihara, R., Gupta, R.K.: Clock synchronization with deterministic accuracy guarantee. In: Marrón, P.J., Whitehouse, K. (eds.) EWSN 2011. LNCS, vol. 6567, pp. 130-146. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19186-2_9 · doi:10.1007/978-3-642-19186-2_9
[27] Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: Formal Methods in Computer-Aided Design, FMCAD 2008, pp. 1-8, November 2008
[28] Tan, L., Bu, L., Zhao, J., Wang, L.: Analyzing the robustness of FTSP with timed automata. In: Proceedings of the Second Asia-Pacific Symposium on Internetware, Internetware 2010, pp. 21:1-21:4. ACM, New York (2010)
[29] Vasudevan, S.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.