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.
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).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bagrodia, R.: Process synchronization: Design and performance evaluation of distributed algorithms. IEEE Trans. on Software Engineering 15(9), 1053–1065 (1989)
Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: From high-level component-based models to distributed implementations. In: Proc. of the 10th ACM International Conference on Embedded Software, pp. 209–218 (2010)
Bouajjani, A., Fernandez, J.C., Graf, S., Rodríguez, C., Sifakis, J.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 76–92. Springer, Heidelberg (1991)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. Journal of the ACM 31(3), 560–599 (1984)
Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.8). Inria/CONVECS (2013)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)
Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten Years of Performance Evaluation for Concurrent Systems Using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 128–142. Springer, Heidelberg (2010)
Dijkstra, E.W.: The Structure of the “THE”-Multiprogramming System. Comm. of the ACM (1968)
Garavel, H.: OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)
Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Verification. In: Proc. of FORTE. Kluwer (2001)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. STTT 15(2), 89–107 (2013)
Garavel, H., Sighireanu, M.: A Graphical Parallel Composition Operator for Process Algebras. In: Proc. of FORTE/PSTV. Kluwer (1999)
Garavel, H., Viho, C., Zendri, M.: System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation. STTT 3(3), 314–331 (2001)
Havender, J.W.: Avoiding deadlock in multitasking systems. IBM Systems Journal 7(2), 74–84 (1968)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
ISO/IEC. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization (1989)
ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization (2001)
Lang, F.: EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70–88. Springer, Heidelberg (2005)
Mateescu, R., Oudot, E.: Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems. In: Proc. of MEMOCODE. IEEE (2008)
Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)
Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Parrow, J., Sjödin, P.: Designing a multiway synchronization protocol. Computer Communications 19(14), 1151–1160 (1996)
Parrow, J., Sjödin, P.: Multiway synchronization verified with coupled simulation. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 518–533. Springer, Heidelberg (1992)
Pérez, J.A., Corchuelo, R., Toro, M.: An order-based algorithm for implementing multiparty synchronization. Concurrency and Computation: Practice and Experience 16(12), 1173–1206 (2004)
Sisto, R., Ciminiera, L., Valenzano, A.: A protocol for multirendezvous of LOTOS processes. IEEE Trans. on Computers 40(4), 437–447 (1991)
Sjödin, P.: From LOTOS Specifications to Distributed Implementations. PhD thesis, Department of Computer Science, University of Uppsala, Sweden (1991)
Stöcker, J., Lang, F., Garavel, H.: Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 88–102. Springer, Heidelberg (2009)
van Glabbeek, R.J., Weijland, W.P.: Branching-Time and Abstraction in Bisimulation Semantics. In: Proc. of IFIP (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Evrard, H., Lang, F. (2013). Formal Verification of Distributed Branching Multiway Synchronization Protocols. In: Beyer, D., Boreale, M. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2013 2013. Lecture Notes in Computer Science, vol 7892. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38592-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-38592-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38591-9
Online ISBN: 978-3-642-38592-6
eBook Packages: Computer ScienceComputer Science (R0)