2011 | OriginalPaper | Chapter
Model Checking for Asynchronous Web Service Composition Based on XYZ/ADL
Authors : Guangquan Zhang, Huijuan Shi, Mei Rong, Haojun Di
Published in: Web Information Systems and Mining
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Concerned with Web service composition, this paper proposes a model checking method of verifying asynchronous communication behaviors and timed properties. Firstly, analyzing Web service composition from software architecture, the interactive behaviors and timed properties are described by XYZ/ADL based on temporal logic language. Secondly, timed asynchronous communication model (TACM) which accords with the specification of model checker UPPAAL is proposed. Finally, based on the transition from XYZ/RE communication commands to TACM, the correctness of asynchronous communication behaviors of the service composition system can be verified by UPPAAL.