Description and Verification of Asynchronous Web Service Composition Based on XYZ/ADL
Jihan Zhu · 2011
Concerned with Web service composition,this paper especially emphasized the formal description and verification of asynchronous communication behaviors and timed properties.Firstly,analyzing Web service composition from software architecture,the interactive behaviors and timed properties were described by XYZ/ADL based on temporal logic language.Secondly,timed asynchronous communication model(TACM) which accords with the specification of model checker UPPAAL was proposed.Finally,based on the transition from XYZ/RE communication command sentences to TACM,the correctness of asynchronous communication behaviors of the service composition system was verified by UPPAAL.