Automated Verification of Asynchronous Communicating Systems with TLA+
DOI:
https://doi.org/10.14279/tuj.eceasst.72.1019Abstract
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
How to Cite
Issue
Section
License
Copyright (c) 2015 Electronic Communications of the EASST
This work is licensed under a Creative Commons Attribution 4.0 International License.