Compatibility Checking for Asynchronous Communication

Organisation:	Toulouse INP, IRIT (FRANCE) Grenoble INP (FRANCE) Inria Grenoble - Rhône-Alpes / CONVECS project-team (FRANCE) University of California at Santa Barbara (USA)
Method:	LOTOS CADP (Construction and Analysis of Distributed Processes)
Domain:	Component-based Systems
Period:	2013
Size:	160 examples of communicating systems (10 case studies taken from the literature, 86 examples of Singularity channel contracts, 64 hand-crafted examples)
Description:	Recent trends in computing technology promote the development of software applications by reusing and composing existing pieces of code. Moreover, many modern applications (e.g., service-oriented computing, cyber-physical systems, pervasive systems, etc.) involve the concurrent execution of distributed components that are required to interact with each other to achieve a shared goal. A central problem in composing distributed components is checking their compatibility, which means to identify if composed components can interoperate without errors. This verification is crucial for ensuring correct execution of a distributed system at runtime. Compatibility errors that are not identified during the design phase can make a distributed system malfunction or deadlock during its execution, which can result in delays, financial loss, and even physical damage in the case of cyber-physical systems. This work focuses on the compatibility checking problem for closed systems involving composition of distributed components, called peers. A set of peers is compatible if, when they are composed, they satisfy a certain property, called compatibility notion. Peer behaviors are described using Labeled Transition Systems (LTSs). The communication between peers is asynchronous and pairwise, which corresponds to message-based communication via FIFO buffers, each individual message being exchanged between two peers (no broadcast communication). Two widely used compatibility notions are considered, namely deadlock-freedom (DF) and unspecified receptions (UR). A set of peers is DF compatible if their composition does not contain any deadlock, i.e., starting from their initial states peers can either progress by following transitions in their respective LTSs or terminate if they are in final states. A set of peers is UR compatible if they do not deadlock and for each message that is sent there is a peer that can receive that message. The compatibility checking proposed relies on synchronizability, which ensures that the synchronous system (i.e., with buffers of size 0) behaves like the asynchronous one for any buffer size. Thus, compatibility can be checked on the synchronous version of the system and the results hold for its asynchronous versions. A branching notion of synchronizability is proposed to take into account the internal actions present in the peer models. It is also required to check that the system is well-formed, meaning that every message sent to a buffer will be eventually consumed. This approach can be used to check DF and UR compatibility for many systems involving loops and respecting the synchronizability property. The approach has been fully automated through an encoding of the peer model into the process algebra LOTOS, one of the input languages of the CADP verification toolbox. By doing so, one can reuse all CADP tools, and particularly state space exploration tools for generating synchronous and asynchronous systems, equivalence checking tools for verifying synchronizability, and model checking tools for searching deadlocks.
Conclusions:	This approach for checking the compatibility of asynchronously communicating systems does not impose any restrictions on the number of participants, on the presence of communication cycles in behavioral models, or on the buffer sizes. Instead, it is focused on the class of synchronizable systems and proposes a sufficient condition for analyzing asynchronous compatibility. This results in a generic framework for verifying whether a set of peers respect some property such as deadlock-freedom or unspecified receptions. Peer models involving internal behaviors are handled by generalizing the synchronizability results to the branching time setting. A new prototype tool enables the designers to automatically check the asynchronous compatibility using the CADP toolbox. Using this tool chain, the approach has been validated on many case studies, most of them borrowed from real-world scenarios found in the literature. The evaluation shows that (i) most systems are synchronizable and can be analyzed using the proposed approach, and (ii) this check is achieved in a reasonable time (seconds for examples involving up to ten peers, and minutes for systems up to 18 peers).
Publications:	[Ouederni-Salaun-Bultan-13] Meriem Ouederni, Gwen Salaün, and Tevfik Bultan. Compatibility Checking for Asynchronously Communicating Software. Proceedings of the 10th International Symposium on Formal Aspects of Component Software FACS'2013 (Nanchang, China), October 2013. Available on-line at: http://hal.inria.fr/hal-00913665/en or from the CADP Web site in PDF and PostScript [Ouederni-21] Meriem Ouederni. Compatibility Checking for Asynchronously Communicating Software. Science of Computer Programming 205, January 2021. Available on-line at: https://doi.org/10.1016/j.scico.2020.102569
Contact:	Gwen Salaün Inria and LIG - CONVECS project-team 655, av. de l'Europe F-38330 Montbonnot Saint Martin France Tel: +33 (0)4 76 61 54 28 Fax: +33 (0)4 76 61 52 52 Email: gwen.salaun@inria.fr
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page