摘要: 面向服务的体系结构的出现和发展使得Web服务成为当今服务及软件开发的发展趋势。由于功能有限的单一的Web服务在多数情况下不能满足用户的需求,出现了将多种 web服务按某种特定的组合集成一个面向具有不同需求用户的有统一接口的服务的技术。然而,服... 展开 面向服务的体系结构的出现和发展使得Web服务成为当今服务及软件开发的发展趋势。由于功能有限的单一的Web服务在多数情况下不能满足用户的需求,出现了将多种 web服务按某种特定的组合集成一个面向具有不同需求用户的有统一接口的服务的技术。然而,服务组合的可信性质受到了来自于服务本身或者其运行环境各个因素的威胁。针对服务的可信性质,研究者们在不断地寻求对验证web服务组合的方法。 目前验证Web服务组合方法多是形式化方法。相对于传统的形式化方法,模型检测的优点是验证的全自动化和验证所给出的证据和反例。其另一个不太易见的优点是,它不需要在验证所涉及逻辑的全体论域中推理待验证公式是否成立,而只需将待检测系统的形式化模型作为论域。在众多用模型检测检验Web服务组合性质的技术中,多智能体系统模型检测的优势在于,它不但能验证时态公式,还能验证认知公式。状态爆炸问题是模型检测面临的主要的问题之一,也当在模型检测多智能体系统的主要瓶颈之列。抽象作为解决状态爆炸问题的一种优化手段,受到了许多研究者的青睐,其研究成果也不断出现。 本文探索一种多智能体系统模型检测图状反例向导的抽象,并将之应用于Web服务组合验证中,这是任何以往的Web服务组合验证工作都没有做到的。另外,以往的反例向导的抽象或者未针对多智能体系统,或者所用形式化模型的形式化程度较本文的 Kripke结构形式化程度低。本文的方法论在文中获得了数学上严格证明。并且,通过实验证明了该方法论在性能上的优越性。论文的主要研究工作概括如下: (1)提出多智能体系统的Kripke结构,提出并证明了其抽象模型和一种获得初始抽象系统的近似方法。 (2)提出了多智能体系统模型检测的一种图状反例,给出并证明了图状反例的某些性质。 (3)提出一种图状反例向导的多智能体系统模型检测抽象精化方法。 (4)根据我们的分析,Web服务组合中常用的规范是BPEL。采用了以往的将BPEL描述的Web服务组合业务流程转化多智能体系统的一种方法。 (5)形成一个基于多智能体系统模型检测及其图状反例向导的抽象与精化技术的Web服务组合验证方法论。 收起