基于符号模型检测的Web服务组合形式化验证  

Formal Verification of Web Service Composition Based on Symbolic Model Checking

作　　者：张世杰 徐鹏[1,2] 刘沛瑶 ZHANG Shijie;XU Peng;LIU Peiyao(School of Mathematics,Southwest Jiaotong University,Chengdu 610031;National-Local Joint Engineering Lab of System Credibility Automatic Verification,Chengdu 610031)

机构地区：[1]西南交通大学数学学院,成都610031 [2]系统可信性自动验证国家地方联合工程实验室,成都610031

出　　处：《计算机与数字工程》2021年第3期496-501,520,共7页Computer & Digital Engineering

基　　金：国家自然科学基金项目“基于矛盾体分离的动态自动演绎推理研究”(编号:61673320);四川省教育厅项目(编号:18ZB0589)资助。

摘　　要：随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求。Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题。针对此问题,提出了一种基于符号模型检测器NuSMV对Web服务组合进行验证的方法,并提出了基于消息会话的Web服务有限状态自动机的形式化定义。最后实例验证了Web服务组合交互的正确性和有无死锁状态现象,进一步证明了方法的可行性。As the economy develops and market competition intensifies,companies must be able to quickly and accurately meet the needs of the market and users.Web service composition is a technology that arises from the inability of a single Web ser⁃vice to meet the needs of enterprises and users.How to ensure the correctness of the combination to realize value-added services is a problem that has not been completely solved.Aiming at this problem,this paper proposes a method based on the symbol model checker NuSMV to verify the Web service composition,and proposes a formal definition of the Web service finite state automaton based on message session.Finally,the example verifies the correctness of Web service composition interaction and the phenomenon of deadlock status,which further proves the feasibility of this method.

关 键 词：WEB服务组合 符号模型检测 有限状态自动机 形式化定义 NUSMV 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]