%0 Conference Proceedings
%T Formal Verification of Distributed Branching Multiway Synchronization Protocols
%+ Construction of verified concurrent systems (CONVECS)
%A Evrard, Hugues
%A Lang, Frédéric
%Z This work was partly funded by the French Fonds national pour la Société Numérique (FSN), Pôles Minalogic, Systematic and SCS (project OpenCloudware).
%Z Part 6: Session 5: Model Checking
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE)
%C Florence, Italy
%Y Dirk Beyer
%Y Michele Boreale
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-7892
%P 146-160
%8 2013-06-03
%D 2013
%Z Computer Science [cs]/Software Engineering [cs.SE]Conference papers
%X Distributed systems are hard to design, and formal methods help to find bugs early. Yet, there may still remain a semantic gap between a formal model and the actual distributed implementation, which is generally hand-written. Automated generation of distributed implementations requires an elaborate multiway synchronization protocol. In this paper, we explore how to verify correctness of such protocols. We generate formal models, written in the LNT language, of synchronization scenarios for three protocols and we use the CADP toolbox for automated formal verifications. We expose a bug leading to a deadlock in one protocol, and we discuss protocol extensions.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-00818788/document
%2 https://inria.hal.science/hal-00818788/file/Evrard-Lang-13.pdf
%L hal-00818788
%U https://inria.hal.science/hal-00818788
%~ UGA
%~ CNRS
%~ INRIA
%~ UNIV-GRENOBLE1
%~ UNIV-PMF_GRENOBLE
%~ INPG
%~ INRIA-RHA
%~ LIG
%~ INRIA_TEST
%~ LIG_MFML
%~ LIG_MFML_CONVECS
%~ CONVECS
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-7892
%~ IFIP-FMOODS
%~ INRIA-RENGRE
%~ LIG_SIDCH