The Safety and Liveness Properties of Composite E-Services Based on Activity Chain

Abstract:

E-service composition is most impressing method for development and deployment of e-business. Description and modeling the behavior requirements of composite E-services for users and verifying composite E-service compliance to specific requirements is an important step in design of services. But most work does not address the issue of how to model the requirements that the BPEL4WS processes are supposed to satisfy. The specifications in verification works are general temporal relation based on activity or scenario in essence. Distinguish with these work, we propose a novel concept of behavior specification based on activity chain in which granularity is between activity and scenario. Chain existence mode, chain absence mode are designed to express such behavioral requirements based on activity chain that is similar with safety or liveness property based on activity respectively. Encode them on Labeled Transition System LTS and then give them exact operation semantics. Finally, an example is illustrated.

• Periodical: Advanced Materials Research (Volumes 219-220)
• Pages: 842-845
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.219-220.842
• Online since: March 2011
• Authors: Bo Chen, Xiao Mei Huang
• Keywords: Activity Chain, Behavior Mode, Composite E-Service, Liveness Property, Safety Property

References

[1] M.Tarek, C. Boutrous-Saab. Verifying correctness of Webservices choreography. Proceedings of the European Conference on Web Services, 2006, pp.306-318.

DOI: 10.1109/ecows.2006.38

[2] C.Ouyanga,_E. Verbeekb, V.D. Aalsta. Formal semantics and analysis of control flow in WS-BPEL. Science of Computer Programming, 2007, 67(4):162–198.

DOI: 10.1016/j.scico.2007.03.002

[3] S.Nakajima. Model-checking behavioral specification of BPEL application. Electronic Notes in Theoretical Computer Science, 2006, 151(2):89-105.

DOI: 10.1016/j.entcs.2005.07.038

[4] Z.Qiu, S.Wang, G.Pu, X.Zhao. Semantics of BPEL4WS-like fault and compensation handling. Lecture Notes in Computer Science, 2005, v3582, pp.350-365.

DOI: 10.1007/11526841_24

[5] X.Fu, T. Bultan, J.Su. Analysis of interacting BPEL Web services. Proceedings of the 13th International Conference on World Wide Web, 2004, pp.624-630.

DOI: 10.1145/988672.988756

[6] A.B. Can, T.Bultan, X.Fu. Design for verification for asynchronously communicating Web services. Proceedings of the 14th International Conference on World Wide Web, 2005, pp.750-759.

DOI: 10.1145/1060745.1060853

[7] V.D. Aalst. Conformance checking of service behavior. ACM Transactions on Internet Technology, 2008, 8(3):1-13.

[8] M. Pistore, M. Roveri, P.Busetta. Requirements-driven verification of Web services. Electronic Notes in Theoretical Computer Science, 2004, 105(3):95–108.

DOI: 10.1016/j.entcs.2004.05.005

[9] M.Rouached, C. Godart. Requirements-driven verification of WSBPEL processes. IEEE International Conference on Web Services, 2007, p.354–363.

DOI: 10.1109/icws.2007.153

[10] D. Giannakopoulou. Model checking for concurrent software architectures. Imperial College of Science, Technology and Medicine University of London. Ph.D.thesis, (1999).

[11] M.B. Dwyer, G.S. Avrunin, J.C. Corbett. Patterns in property specifications for finite-state verification. Proceedings of the 1999 International Conference on Software Engineering, 1999, pp.411-420.

DOI: 10.1145/302405.302672

[12] J. Yu, T.P. Manh, J. Han, U. Jin, Y. Han, J.W. Wang. Pattern based property specification and verification for service composition. Lecture Notes in Computer Science, 2006, v4255, pp.156-168.

DOI: 10.1007/11912873_18