OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Automated Verification of Asynchronous Communicating Systems with TLA+

Chevrou, Florent and Hurault, Aurélie and Quéinnec, Philippe Automated Verification of Asynchronous Communicating Systems with TLA+. (2015) Electronic Communications of the EASST, 72. 1-15. ISSN 1863-2122

(Document in English)

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

Official URL: http://dx.doi.org/10.14279/tuj.eceasst.72.1019.1005


Verifying the compatibility of communicating peers is a crucial issue in critical distributed systems. Unlike the synchronous world, the asynchronous world covers a wide range of message ordering paradigms (e.g. FIFO or causal) that are instrumental to the compatibility of peer compositions. We propose a framework that takes into account the variety of asynchronous communication models and compatibility properties. The notions of peer, communication model, system and compatibility criteria are formalized in TLA+ to benefit from its verification tools. We present an implemented toolchain that generates TLA+ specifications from the behavioral descriptions of peers and checks compatibility of the composition with respect to given communication models and compatibility criteria.

Item Type:Article
Additional Information:This papers appears in Volume 72 of Electronic Communications of the EASST (ISSN 1863-2122) : Proceedings of the 15th International Workshop on Automated Verification of Crit (AVoCS 2015) The original PDF is available at: https://journal.ub.tu-berlin.de/eceasst/article/view/1019
HAL Id:hal-01535957
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (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:
Deposited On:02 Jun 2017 14:48

Repository Staff Only: item control page