Formal Verification of Distributed Branching Multiway Synchronization Protocols

Hugues Evrard 1, * Frédéric Lang 1
* Corresponding author
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : 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.
Document type :
Conference papers
Dirk Beyer; Michele Boreale. 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), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.146-160, 2013, Formal Techniques for Distributed Systems
Liste complète des métadonnées


https://hal.inria.fr/hal-00818788
Contributor : Hugues Evrard <>
Submitted on : Monday, April 29, 2013 - 10:57:50 AM
Last modification on : Friday, April 28, 2017 - 1:06:25 AM
Document(s) archivé(s) le : Tuesday, July 30, 2013 - 4:45:10 AM

File

Evrard-Lang-13.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

  • HAL Id : hal-00818788, version 1

Citation

Hugues Evrard, Frédéric Lang. Formal Verification of Distributed Branching Multiway Synchronization Protocols. Dirk Beyer; Michele Boreale. 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), Jun 2013, Florence, Italy. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.146-160, 2013, Formal Techniques for Distributed Systems. <hal-00818788>

Share

Metrics

Record views

350

Document downloads

169