基于时间扩展的Web服务模型检测
王雪红
刘柯威
陈冠萍
胡元闯
1.贺州学院计算机科学与信息工程学院,广西贺州,5428992.贺州学院计算机科学与信息工程学院,广西贺州,5428993.贺州学院计算机科学与信息工程学院,广西贺州,5428994.贺州学院计算机科学与信息工程学院,广西贺州,542899
摘要：由于传统的形式化方法不能保证带时间约束的组合Web服务安全可靠地运行,为了有效地分析并确保带时间约束的组合Web服务的正确性,利用时间自动机验证工具UPPAAL将带时间约束的组合Web服务的每个原子服务建立自动机模型,给出ASEHA语义描述,并用模拟器模拟带时间约束的Web服务的运行过程,对带有时间约束的Web服务的属性进行分析.最后,以旅行预订票组合系统为例,验证其死锁、活性和安全性.实例证明此方法有效.
关键词：Web服务ASEHA时钟约束UPPAAL
分类号：TP393.09(计算技术、计算机技术)
资助基金：广西自然科学基金资助项目(2014jjBA70066)贺州学院校级科研项目(2014ZC22)贺州学院校级教改项目(hzxyjg201514)贺州学院校级教改项目(hzxyjg201515)
论文发表日期：2017-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：4( 14-17 )
英文信息