Iowa State University (USA)
University of California at Santa Barbara (USA)
University of Málaga (SPAIN)
Check synchronizability and realizability of asynchronously
Web Service Analysis Tool
CADP (Construction and Analysis of Distributed Processes)
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.
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.
Samik Basu, Tevfik Bultan, and Meriem Ouederni.
"Synchronizability for Verification of Asynchronously Communicating
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 our FTP 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 our FTP site in PDF or PostScript
Prof. Tevfik Bultan
Department of Computer Science
University of California
Santa Barbara, CA 93106-5110
Tel: (805) 893 3735
Fax: (805) 893 8553
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|