Formalizing of web-services specifications using temporal logics

Authors

  • 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

Keywords:

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

Abstract

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.

Author Biographies

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

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

2015-03-24

Issue

Section

Technical Sciences