Abstract
This paper presents a novel formal method to describe contracrt-regulated service composition components using abstract concepts and (semi-) automatically verify the specification. We model web service component behaviours and the contracts based on Tecton language expressed using “concept descriptions”, to be used with Violet verification system to prove properties of service composition component. The verified generic contract-regulated composition specification at an abstract level will be used in a variety of instances as BPEL specification without repeating the proof. The main advantage of this method is to improve the reusability of specification and seamlessly integrate behaviour descriptions with contacts.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Musser DR, Shao Z (2002) Concept use or concept refinement: an important distinction in building generic specifications. In Proceedings of the 4th international conference on formal engineering methods. Volume of LNCS 2495, Springer. New York, pp 132–143)
Jie Zhai Z, Shao (2011) Specification and verification of generic web service composition. Comput Appl Softw 28(11):64–68 (in Chinese)
Musser DR, Shao Z (2003) The Tecton concept description language (revised version). http://www.cs.rpi.edu/~zshao
Jie Zhai Z, Shao (2005) The Proof System based on Tecton—Violet. J ECUST 31(2):198–202 (in Chinese)
Zhai J, Shao Z (2011) Generic web sevices composition verification based on batch proof method. In ICCIS 2011(3):843–846
Lomuscio A, Qu H, Solanki M (2012) Towards verifying contract regulated service compositions. Auton Agent Multi-agent Syst 24:345–373
Lomuscio A, Qu H, Raimondi F (2009) MCMAS: a model checker for the verification of multi-agent systems. In: Proceedings of CAV 2009. LNCS (vol 5643). Springer, New York, pp 682–688
Acknowledgments
The research described in this paper was supported by the National Natural Science Foundation of China under Grant No. 61003126 and the Shanghai Natural Science Foundation of China under Grant No. 09ZR1408400.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhai, J., Shao, Z., Guo, Y., Zhang, H. (2013). Generic Contract-Regulated Web Service Composition Specification and Verification. In: Lu, W., Cai, G., Liu, W., Xing, W. (eds) Proceedings of the 2012 International Conference on Information Technology and Software Engineering. Lecture Notes in Electrical Engineering, vol 212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34531-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-34531-9_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34530-2
Online ISBN: 978-3-642-34531-9
eBook Packages: EngineeringEngineering (R0)