基于时间扩展的Web服务模型检测  

Model checking Web services based on timed extension

作　　者：王雪红[1] 刘柯威 陈冠萍[1] 胡元闯[1] 

机构地区：[1]贺州学院计算机科学与信息工程学院

出　　处：《佛山科学技术学院学报（自然科学版）》2017年第2期14-17,共4页Journal of Foshan University(Natural Science Edition)

基　　金：广西自然科学基金资助项目(2014jj BA70066);贺州学院校级科研项目(2014ZC22);贺州学院校级教改项目(hzxyjg201514;hzxyjg201515)

摘　　要：由于传统的形式化方法不能保证带时间约束的组合Web服务安全可靠地运行,为了有效地分析并确保带时间约束的组合Web服务的正确性,利用时间自动机验证工具UPPAAL将带时间约束的组合Web服务的每个原子服务建立自动机模型,给出ASEHA语义描述,并用模拟器模拟带时间约束的Web服务的运行过程,对带有时间约束的Web服务的属性进行分析。最后,以旅行预订票组合系统为例,验证其死锁、活性和安全性。实例证明此方法有效。As the traditional formal methods can not guarantee safe and reliable operation of Web services composition with timed constraints, each atom service of Web services composition with timed constraints built automata model using the model checker UPPAAL, and gave ASEHA semantic description in order to analyze and ensure the correctness of Web services composition with timed constraints. Running process of Web services composition with timed constraints was simulated by simulator of UPPAAL. We analyzed the properties of Web services composition with timed constraints. Finally, we verified properties of deadlock, liveness and security such as the travel reservation system. An example was provided to demonstrate the modeling process and formal verification.

关 键 词：WEB服务 ASEHA 时钟约束 UPPAAL 

分 类 号：TP393.09[自动化与计算机技术—计算机应用技术]