In the article proposed formalisms for defining rules of Web-services orchestration and choreography that allows to combine elements of a distributed system in a single system. Proposed approach allows to perform formal association of individual system components into a single unit. Proposed verification method for distributed systems based on the model approach. E-networks are models for verification of distributed systems. Web-service’s safety check is performed by finding deadlock conditions or any deviation from the specification process. This method allows taking into account the asynchronous nature of complex services and also performing stateful inspection: check for different Web-service consistency, check orchestration and choreography compatibility requirements for each service.
This study uses new algebraic methods for the analysis of complex Web-services. The novelty is in the use of formal grammars, which solved the problem of validation and evaluation of the behavior of the resource allocation of info communication protocols.
C. Peltz, "Web services orchestration and choreography," IEEE Computer, vol. 36, pp. 6-52, 2003.
G. Alonso, F. Casati, H. Kuno, and Machiraju, Web services—concepts, architectures and applications. Berlin Heidelberg: Springer-Verlag, 2008.
A. Airkin, S. Askary, and W. Fordin, "Web service choreography interface (WSCI) 1.0," W3C Working Group, 2002.
C. Peltz, Web services orchestration — A review of emerging technologies, tools, and standards: Hewlett-Packard Company, 2003.
S. Weerawarana and C. Francisco, "Business process with BPEL4WS: Understanding BPEL4WS," Part 1 // Research Report, IBM Developer Works2002.
M. Y. Vardi, "An automata-theoretic approach to automatic program verification. M.Y. Vardi, P. Wolper," in Proc. of the First Symposium on Logic in Computer Science, 1986, pp. 322-331.
A. Lafuente, "Directed search for the verification of communication protocols," A. Lafuente // Doctorial Thesis, University of Freiburg, Institute of Computer Science. pp: 157, 2009.
C. S. Langdon, "The state of web services," IEEE Computer, vol. 36, pp. 96-99, 2010.
M. Baldoni, C. Baroglio, and A. Martelli, "Verifying the conformance of web services to global interaction protocols: A first step," International Workshop on Web Services and Formal Methods, 2010.
M. Bravetti, C. Guidi, and R. Lucchi, "Supporting e-commerce systems formalization with choreography languages," in SAC ’05: Proceedings of the 2005 ACM Symposium on Applied Computing, New York, USA, 2005, pp. 831–835.
J. Clarke, M. Edmund, and A. Peled, Model checking: MIT Press, 1999.