Open Access
ARTICLE
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. https://doi.org/10.32604/cmc.2020.06216
Abstract
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.
Keywords
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. https://doi.org/10.32604/cmc.2020.06216