Formalizing of web-services specifications using temporal logics
DOI:
https://doi.org/10.15587/2313-8416.2015.38838Keywords:
Web-service, SOAP, WSDL, OASIS, verification, temporal logics, Computational Tree Logic, contradictionsAbstract
Issues related to improving the design of multiservice SOA networks are discussed. Issue of creation of complex services, their orchestration and choreography are considered. Problem arising when creating an integrated service is discussed. It is shown that the formal description of the service using temporal logics will perform rigorous verification service and eliminate design errors.
References
Stirling, C. P. (1992). Modal and temporal logics. Handbook of Logic in Computer Science. Oxford University Press, 2, 477–563.
Lafuente, A. (2003). Directed Search for the Verification of communication protocols. Institute of computer science, University of Freiburg, 157.
Rosenberg, J., Schulzrinne, H., Columbia, U., Camarillo, G. (2002). SIP: Session Initiation Protocol. RFC 3261. East Hanover, 269.
Rosenberg J., Schulzrinne, H. (2003). An Extension to the Session Initiation Protocol (SIP) for Symmetric Response Routing RFC 3581. Parsippany, 13.
Stirling, C. P. (1996). Modal and temporal logics for processes. LNCS, 149–237. doi: 10.1007/3-540-60915-6_5
Kaivola, R. (1997). Using compositional preorders in the verification of sliding window protocol. Lecture Notes in Computer Science, 48–59. doi: 10.1007/3-540-63166-6_8
Postel, J. (1981). Transmission control protocol. RFC 793. California, 85.
Myers, J., Mellon, C., Rose, M. (1996). Post Office Protocol. Version 3. RFC 1939, Pittsburgh, 23.
Lawrence, S., Prentice, H. (2001). Software Engineering: Theory and Practice (2nd ed.) Upper Saddle River, 630.
Clarke, E. M., Emerson, E. A., Sistla, A. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8 (2), 244–263. doi: 10.1145/5397.5399
ITU-T Recommendation H.248. Series H, Geneva (2000). Audiovisual and Multimedia Systems. Infrastructure of audiovisual services Communication procedures. Gateway control protocol. International Telecommunications Union.
Greene, N., Rayhan, A. (2000). Megaco Protocol Version 1.0. RFC 3015. Ottawa, 179.
Downloads
Published
Issue
Section
License
Copyright (c) 2015 Mohammed Khodayer Hassan Al-Dulaimi, Aymen Mohammed Khodayer Al-Dulaimi
This work is licensed under a Creative Commons Attribution 4.0 International License.
Our journal abides by the Creative Commons CC BY copyright rights and permissions for open access journals.
Authors, who are published in this journal, agree to the following conditions:
1. The authors reserve the right to authorship of the work and pass the first publication right of this work to the journal under the terms of a Creative Commons CC BY, which allows others to freely distribute the published research with the obligatory reference to the authors of the original work and the first publication of the work in this journal.
2. The authors have the right to conclude separate supplement agreements that relate to non-exclusive work distribution in the form in which it has been published by the journal (for example, to upload the work to the online storage of the journal or publish it as part of a monograph), provided that the reference to the first publication of the work in this journal is included.