A Formal Method for Service Choreography Verification Based on Description Logic  

作　　者：Tingting Zhang Yushi Lan Minggang Yu Changyou Zheng Kun Liu 

机构地区：[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

出　　处：《Computers, Materials & Continua》2020年第2期893-904,共12页计算机、材料和连续体（英文）

基　　金：This work is supported by the National Natural Science Fund number 61802428.

摘　　要：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 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]