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

Formalizing of web-services specifications using temporal logics

Mohammed Khodayer Hassan Al-Dulaimi, Aymen Mohammed Khodayer Al-Dulaimi

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.


Keywords


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

Full Text:

PDF

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.


GOST Style Citations


1. Stirling, C. P. Modal and temporal logics [Text] / C. P. Stirling. – Handbook of Logic in Computer Science. – Oxford University Press. – 1992. – Vol. 2. – P. 477–563.

2. Lafuente, A. Directed Search for the Verification of communication protocols [Text] : Doctorial thesis/ A. Lafuente. – Institute of computer science, University of Freiburg, 2003. – 157 p.

3. Rosenberg, J. SIP: Session Initiation Protocol. RFC 3261 [Text] / J. Rosenberg, H. Schulzrinne, U. Columbia, G. Camarillo. – East Hanover, 2002. – 269 p.

4. Rosenberg, J. An Extension to the Session Initiation Protocol (SIP) for Symmetric Response Routing RFC 3581 [Text] / J. Rosenberg, H. Schulzrinne. – Parsippany, 2003. – 13 p.

5. Stirling C. P. Modal and temporal logics for processes [Text] / C. P. Stirling. – LNCS 1043, 1996. –P. 149–237. doi: 10.1007/3-540-60915-6_5 

6. Kaivola, R. Using compositional preorders in the verification of sliding window protocol [Text] / R. Kaivola. – Lecture Notes in Computer Science, 1997. – P. 48–59. doi: 10.1007/3-540-63166-6_8 

7. Postel, J. Transmission control protocol. RFC 793 [Text] / J. Postel. – California, 1981. – 85 p.

8. Myers, J. Post Office Protocol. Version 3. RFC 1939 [Text] / J. Myers, C. Mellon, M. Rose. – Pittsburgh, 1996. – 23 p.

9. Lawrence, S. Software Engineering: Theory and Practice (2nd ed.) [Text] / S. Lawrence. – Upper Saddle River, NJ: Prentice Hall, 2001. – 630 p.

10. Clarke, E. M. Automatic verification of finite-state concurrent systems using temporal logic specifications [Text] / E. M. Clarke, E. A. Emerson, A. P. Sistla // ACM Transactions on Programming Languages and Systems. – 1986. – Vol. 8, Issue 2. – P. 244–263. doi: 10.1145/5397.5399 

11. ITU-T Recommendation H.248. Series H: Audiovisual and Multimedia Systems: Infrastructure of audiovisual services – Communication procedures: Gateway control protocol [Text] / Geneva: International Telecommunications Union, 2000.

12. Greene, N. Megaco Protocol Version 1.0. RFC 3015 [Text] / N. Greene, A. Rayhan. – Ottawa, November, 2000. – 179 p.







Copyright (c) 2015 Mohammed Khodayer Hassan Al-Dulaimi, Aymen Mohammed Khodayer Al-Dulaimi

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.

ISSN 2313-8416 (Online), ISSN 2313-6286 (Print)