OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Modular Framework for Verifying Versatile Distributed Systems

Chevrou, Florent and Hurault, Aurélie and Quéinnec, Philippe A Modular Framework for Verifying Versatile Distributed Systems. (2019) Journal of Logical and Algebraic Methods in Programming, 108. 24-46. ISSN 2352-2208

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
1MB

Official URL: https://doi.org/10.1016/j.jlamp.2019.05.008

Abstract

Putting independent components together is a common design practice of distributed systems. Besides, there exists a wide range of interaction protocols that dictate how these components interact, which impacts their compatibility. However, the communication model itself always consists in a monolithic description of the rules and properties of the communication. In this paper, we propose a mechanized framework for the compatibility checking of compositions of peers where the interaction protocol can be fine tuned through assembly of basic properties on the communication. These include whether the communication is point-to-point, multicast or convergecast, which ordering-policies are to be applied, applicative priorities, bounds on the number of messages in transit, and so on. Among these properties, we focus on a generic description of multicast communication that encompasses point-to-point and one-to-all communication as special cases. The components that form the communication model are specified in TLA+, and a system, composed of a communication model and a specification of the behavior of the peers (also in TLA+ ), is checked with the TLA+ model checker. Eventually we provide theoretical views on the relations between ordering-policies through the lenses of multicast and convergecast communication.

Item Type:Article
Additional Information:https://www.sciencedirect.com/science/article/pii/S2352220818301317
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Funders:
ANR : Agence nationale de la recherche (France)
Statistics:download
Deposited By: IRIT IRIT
Deposited On:09 Jan 2020 11:08

Repository Staff Only: item control page