Automated Verification of Asynchronous Communicating Systems with TLA+

Authors

  • Florent Chevrou Institut de Recherche en Informatique de Toulouse
  • Aurélie Hurault Institut de Recherche en Informatique de Toulouse
  • Philippe Quéinnec Institut de Recherche en Informatique de Toulouse

DOI:

https://doi.org/10.14279/tuj.eceasst.72.1019

Abstract

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.

Downloads

Published

2015-11-25

How to Cite

[1]
F. Chevrou, A. Hurault, and P. Quéinnec, “Automated Verification of Asynchronous Communicating Systems with TLA+”, eceasst, vol. 72, Nov. 2015.