Vol.62, No.2, 2020, pp.893-904, doi:10.32604/cmc.2020.06216
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: zhangtings@sohu.com.
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.
Service choreography, WS-CDL, meta-concept model, description logic, formal verification.
Cite This Article
Zhang, T., Lan, Y., Yu, M., Zheng, C., Liu, K. (2020). A Formal Method for Service Choreography Verification Based on Description Logic. CMC-Computers, Materials & Continua, 62(2), 893–904.
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.