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. © 2013 IFIP International Federation for Information Processing.
CITATION STYLE
Evrard, H., & Lang, F. (2013). Formal verification of distributed branching multiway synchronization protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7892 LNCS, pp. 146–160). https://doi.org/10.1007/978-3-642-38592-6_11
Mendeley helps you to discover research relevant for your work.