@Article{cmc.2020.06216,
AUTHOR = {Tingting Zhang, Yushi Lan, Minggang Yu, Changyou Zheng, Kun Liu},
TITLE = {A Formal Method for Service Choreography Verification Based on Description Logic},
JOURNAL = {Computers, Materials \& Continua},
VOLUME = {62},
YEAR = {2020},
NUMBER = {2},
PAGES = {893--904},
URL = {http://www.techscience.com/cmc/v62n2/38283},
ISSN = {1546-2226},
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.},
DOI = {10.32604/cmc.2020.06216}
}