Synchronizability and Realizability of Asynchronous Systems

Organisation:	Iowa State University (USA) University of California at Santa Barbara (USA) University of Málaga (SPAIN)
Functionality:	Check synchronizability and realizability of asynchronously communicating systems.
Tools used:	Web Service Analysis Tool CADP (Construction and Analysis of Distributed Processes)
Period:	2012
Description:	Message-based communication is an increasingly common interaction mechanism used in concurrent and distributed systems where components interact with each other by sending and receiving messages. It is well-known that verification of systems that use asynchronous message-based communication with unbounded FIFO queues is undecidable even when the component behaviors are expressed using finite state machines. This work shows that there is a sub-class of such systems, called synchronizable systems, for which certain reachability properties (over send actions and over states with no pending receives) remain unchanged when asynchronous communication is replaced with synchronous communication. Hence, if a system is synchronizable, then the verification of these reachability properties can be done on the synchronous version of the system and the results hold for the asynchronous case. A system is synchronizable if and only if the behaviors for the synchronous version of the system and the 1-bounded-asynchronous version of the system are equivalent with respect to sent messages and reachable configurations with empty message queues. Since both synchronous and 1-bounded-asynchronous versions of a system have finite state space, the equivalence check of their behavior, and therefore, synchronizability check, can be done automatically. Moreover, a system is realizable (i.e., there is a way to implement a set of that components interact asynchronously and conform to the global description of the system) if the 1-bounded system satisfies a specific temporal property, called well-formedness condition. The approach for checking synchronizability and realizability has been implemented for analyzing various classes of systems, such as Web service choreographies, channel contracts in Singularity OS, and UML collaboration diagrams. In the service-oriented computing domain such communication contracts are called "choreography" specifications. A choreography specification is a state machine that identifies the allowable ordering of message exchanges in a distributed system. The tool takes as input a choreography specification and generates two LOTOS specifications that correspond to the synchronous and 1-bounded-asynchronous versions of the input choreography. Then, the CADP toolbox is used to check the equivalence of the synchronous and 1-bounded-asynchronous versions. The construction of LTSs from LOTOS specifications, the reduction of the LTSs and their equivalence checking are performed automatically using SVL scripts and by using the REDUCTOR and the BISIMULATOR tools of CADP.
Conclusions:	The new decision procedure for realizability is applicable to a variety of domains including verification and analysis of interactions among processes at the OS level, coordination in service-oriented computing, and interactions among distributed programs.
Publications:	[Basu-Bultan-Ouederni-12-a] Samik Basu, Tevfik Bultan, and Meriem Ouederni. "Synchronizability for Verification of Asynchronously Communicating Systems". Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI'2012 (Philadelphia, Pennsylvania, USA), Lecture Notes in Computer Science vol. 7148, pages 56-71. Springer Verlag, January 2012. Available on-line at: http://www.cs.ucsb.edu/~bultan/publications/vmcai12.pdf or from the CADP Web site in PDF or PostScript [Basu-Bultan-Ouederni-12-b] Samik Basu, Tevfik Bultan, and Meriem Ouederni. "Deciding Choreography Realizability". Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL'2012 (Philadelphia, Pennsylvania, USA), pages 191-202. ACM Computer Society Press, January 2012. Available on-line at: http://www.cs.ucsb.edu/~bultan/publications/popl12.pdf or from the CADP Web site in PDF or PostScript
Contact:	Prof. Tevfik Bultan Department of Computer Science University of California Santa Barbara, CA 93106-5110 USA Tel: (805) 893 3735 Fax: (805) 893 8553 Email: bultan@cs.ucsb.edu
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page