Formalizing of web-services specifications using temporal logics

Auteurs-es

  • Mohammed Khodayer Hassan Al-Dulaimi Instructor at Al-Rafidain University College Iraq, Bagdad, Hay Al Mustansurya, Iraq
  • Aymen Mohammed Khodayer Al-Dulaimi Odessa National Academy of Telecommunications. A.S. Popova. Odessa region, st. Kovalska1, 65000, ONAS, Ukraine

DOI :

https://doi.org/10.15587/2313-8416.2015.38838

Mots-clés :

Web-service, SOAP, WSDL, OASIS, verification, temporal logics, Computational Tree Logic, contradictions

Résumé

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.

Bibliographies de l'auteur-e

Mohammed Khodayer Hassan Al-Dulaimi, Instructor at Al-Rafidain University College Iraq, Bagdad, Hay Al Mustansurya

PhD

Department of Software Engineering

Aymen Mohammed Khodayer Al-Dulaimi, Odessa National Academy of Telecommunications. A.S. Popova. Odessa region, st. Kovalska1, 65000, ONAS

Graduate student

Department of Telecommunication Systems

Références

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.

Téléchargements

Publié-e

2015-03-24

Numéro

Vol. 3 No. 2 (8) (2015)

Rubrique

Technical Sciences

Licence

(c) Tous droits réservés Mohammed Khodayer Hassan Al-Dulaimi, Aymen Mohammed Khodayer Al-Dulaimi 2015

Licence Creative Commons

Cette œuvre est sous licence Creative Commons Attribution 4.0 International.

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.