Table of Content

Open AccessOpen Access


A Formal Method for Service Choreography Verification Based on Description Logic

Tingting Zhang1, 2, 3, *, Yushi Lan2, Minggang Yu1, Changyou Zheng1, Kun Liu1

1 PLA Army Engineering University, Nanjing, China.
2 The 28th Research Institute of China Electronics Technology Group Corporation, Nanjing, China.
3 Southeast University, Nanjing, China.

* Corresponding Author: Tingting Zhang. Email: .

Computers, Materials & Continua 2020, 62(2), 893-904.


Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model. This paper presents a new approach of choreography model verification based on Description Logic. A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography. Based on the framework, a set of rules and constraints are defined in Description Logic for choreography model verification. To automate model verification, the UML-based service choreography model will be transformed, by the given algorithms, into the DL-based ontology, and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned. A case study is given to demonstrate applicability of the method. Furthermore, the work will be compared with other related research.


Cite This Article

T. Zhang, Y. Lan, M. Yu, C. Zheng and K. Liu, "A formal method for service choreography verification based on description logic," Computers, Materials & Continua, vol. 62, no.2, pp. 893–904, 2020.

This work is licensed under a Creative Commons Attribution 4.0 International License , which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
  • 3446


  • 1798


  • 0


Related articles

Share Link