Automated Verification of Asynchronous Communicating Systems with TLA+

Florent Chevrou (1) , Aurélie Hurault (1, 2) , Philippe Quéinnec (1, 2)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 Toulouse INP - Institut National Polytechnique (Toulouse)

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.

Mots clés: Compatibility checking; Peer composition; Aynchronous communication; TLA+

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Florent Chevrou, Aurélie Hurault, Philippe Quéinnec. Automated Verification of Asynchronous Communicating Systems with TLA+. 15th International Workshop on Automated Verification of Critical Systems (AVOCS 2015), Sep 2015, Edinburgh, Scotland, United Kingdom. pp.135-150. ⟨hal-01592022⟩