发表刊物：计算机工程
刊物所在地：华东计算技术研究所;上海市计算机学会
关键字：Web服务组合； 多主体系统； 模型检测； 图状反例； 抽象； 精化；
摘要：Web服务组合现已成为跨组织业务流程集成的关键技术,然而在松耦合开发模式和开放的互联网运行环境下,其正确性、可靠性、安全性等可信性质难以得到保证。为解决该问题,提出一种Web服务组合形式化验证方法,将基于图状反例向导的抽象与精化方法应用于多主体系统(MAS)模型检测工具(MCTK)中,大幅缓解模型检测的状态爆炸问题,从理论上证明该验证方法的正确性。实验通过将银行贷款风险评估系统转换成MCTK描述的MAS,并对比抽象前后的模型检测代价,结果显示,基于抽象的Web服务验证方法明显优于未采用抽象技术的验证方法。
页面范围：26-31
字数：7000
是否译文：否
发表时间：2014-12-03
第一作者：骆翔宇,许兴旺(学)