由于传统的形式化方法不能保证带时间约束的组合Web服务安全可靠地运行,为了有效地分析并确保带时间约束的组合Web服务的正确性,利用时间自动机验证工具UPPAAL将带时间约束的组合Web服务的每个原子服务建立自动机模型,给出ASEHA语义描述,并用模拟器模拟带时间约束的Web服务的运行过程,对带有时间约束的Web服务的属性进行分析。最后,以旅行预订票组合系统为例,验证其死锁、活性和安全性。实例证明此方法有效。
科研之友
微信
新浪微博
Facebook
分享链接
