Advertisement

Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking

  • Étienne AndréEmail author
  • Laurent Fribourg
  • Jean-Marc Mota
  • Romain Soulat
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

Abstract

The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i. e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number p of processes (\(p=5000\)).

Keywords

Leader election Distributed algorithm Model checking SaveProver Parameterized verification Parametric timed automata 

Notes

Acknowledgment

We thank anonymous reviewers for very useful remarks and suggestions.

References

  1. 1.
    Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: On the verification of timed ad hoc networks. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 256–270. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24310-3_18CrossRefzbMATHGoogle Scholar
  2. 2.
    Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: Parameterized verification of time-sensitive models of ad hoc network protocols. Theor. Comput. Sci. 612, 1–22 (2016)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1), 241–264 (2003)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Arvind, V., Ramanujam, S. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 245–256. Springer, Heidelberg (1998).  https://doi.org/10.1007/978-3-540-49382-2_22CrossRefGoogle Scholar
  5. 5.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) Proceedings of the Twenty-Fifth Annual ACM symposium on Theory of Computing (STOC 1993), pp. 592–601. ACM, New York (1993)Google Scholar
  7. 7.
    André, É.: Observer patterns for real-time systems. In: Liu, Y., Martin, A. (eds.) Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2013), pp. 125–134. IEEE Computer Society, July 2013Google Scholar
  8. 8.
    André, É.: What’s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf. (2019, to appear)Google Scholar
  9. 9.
    André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32759-9_6CrossRefGoogle Scholar
  10. 10.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30080-9_7CrossRefGoogle Scholar
  11. 11.
    Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000).  https://doi.org/10.1007/10722167_31CrossRefGoogle Scholar
  12. 12.
    Conchon, S., Declerck, D., Zaïdi, F.: Compiling parameterized X86-TSO concurrent programs to Cubicle-\(\cal{W}\). In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 88–104. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-68690-5_6CrossRefGoogle Scholar
  13. 13.
    Conchon, S., Declerck, D., Zaïdi, F.: Parameterized model checking modulo explicit weak memory models. In: Laleau, R., Méry, D., Nakajima, S., Troubitsyna, E. (eds.) Proceedings of the Joint Workshop on Handling IMPlicit and EXplicit Knowledge In Formal System Development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD), IMPEX/FM&MDD 2017. EPTCS, vol. 271, pp. 48–63 (2017)Google Scholar
  14. 14.
    Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_55CrossRefGoogle Scholar
  15. 15.
    De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRefGoogle Scholar
  16. 16.
    Étienne, J.F., Juppeaux, É.: SafeProver: a high-performance verification tool. ACM SIGAda Ada Lett. 36(2), 47–48 (2017)CrossRefGoogle Scholar
  17. 17.
    Fribourg, L., Olsén, H.: Reachability sets of parameterized rings as regular languages. Electron. Notes Theor. Comput. Sci. 9, 40 (1997)CrossRefGoogle Scholar
  18. 18.
    García-Molina, H.: Elections in a distributed computing system. IEEE Trans. Comput. 31(1), 48–59 (1982)CrossRefGoogle Scholar
  19. 19.
    Konnov, I.V., Veith, H., Widder, J.: What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: Mazzara, M., Voronkov, A. (eds.) PSI 2015. LNCS, vol. 9609, pp. 6–21. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41579-6_2CrossRefzbMATHGoogle Scholar
  20. 20.
    Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133–169 (1998)CrossRefGoogle Scholar
  21. 21.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)Google Scholar
  22. 22.
    Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)zbMATHGoogle Scholar
  23. 23.
    Sun, Y., André, É., Lipari, G.: Verification of two real-time systems using parametric timed automata. In: Quinton, S., Vardanega, T. (eds.) Proceedings of the 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS 2015), July 2015Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Étienne André
    • 1
    • 2
    • 3
    Email author
  • Laurent Fribourg
    • 4
  • Jean-Marc Mota
    • 5
  • Romain Soulat
    • 5
  1. 1.Université Paris 13, LIPN, CNRS, UMR 7030VilletaneuseFrance
  2. 2.JFLI, CNRSTokyoJapan
  3. 3.National Institute of InformaticsTokyoJapan
  4. 4.LSV, ENS Paris-Saclay & CNRS & INRIA, U. Paris-SaclayParisFrance
  5. 5.Thales Research and TechnologyPalaiseauFrance

Personalised recommendations