基于MAS模型检测与抽象的Web服务验证

摘要

Web services composition is a key technology to solve cross-organizational business process integrations. However, it is hard to ensure its trusted properties ( including correctness, reliability, safety ) , because of the loosely coupled development paradigm and open Internet running environment. To solve this problem, this paper proposes a formal verification and abstraction method for Web services composition based on model checking Multi-Agent Systems ( MAS) and refinement. By applying the method of the graph-like counterexample guided abstraction and refinement on MCTK,it greatly reduces the state explosion problem of model checking. The correctness of the method is proved theoretically. Recording to the experimental results of which translates a credit risk assessment Web services to a MAS programmed by input language of MCTK then model checks both abstracted and un-abstracted MAS,the Web services verification based on proposed method works much more efficiently than the normal verification based on MAS model checking.%Web服务组合现已成为跨组织业务流程集成的关键技术,然而在松耦合开发模式和开放的互联网运行环境下,其正确性、可靠性、安全性等可信性质难以得到保证。为解决该问题,提出一种Web服务组合形式化验证方法,将基于图状反例向导的抽象与精化方法应用于多主体系统( MAS)模型检测工具( MCTK)中,大幅缓解模型检测的状态爆炸问题,从理论上证明该验证方法的正确性。实验通过将银行贷款风险评估系统转换成MCTK描述的MAS,并对比抽象前后的模型检测代价,结果显示,基于抽象的Web服务验证方法明显优于未采用抽象技术的验证方法。