基于符号模型检测的Web服务组合形式化验证
张世杰
徐鹏
刘沛瑶
西南交通大学数学学院 成都 610031;系统可信性自动验证国家地方联合工程实验室 成都 610031
摘要：随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求.Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题.针对此问题,提出了一种基于符号模型检测器NuSMV对Web服务组合进行验证的方法,并提出了基于消息会话的Web服务有限状态自动机的形式化定义.最后实例验证了Web服务组合交互的正确性和有无死锁状态现象,进一步证明了方法的可行性.
关键词：Web服务组合符号模型检测有限状态自动机形式化定义NuSMV
分类号：TP181(自动化基础理论)
资助基金：国家自然科学基金(61673320)四川省教育厅项目(18ZB0589)
论文发表日期：2021-03-20
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：7( 496-501,520 )
英文信息