@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} }