基于概率模型检验的Web服务动态自适应配置

Web service dynamic self-adaption reconfiguration is one of effective approaches to handling service failures. Probabilistic model checking is used to guarantee the correctness and reliability. The main contents of this project proposal include Web service monitoring, dynamic reconfiguration, formal verification and failed services forecast. The probabilistic timed automaton is employed to modeling run-time service behavior. The extended LSC is used to formalize the threat model, from which the correctness and reliability property are generated. The Web service monitoring is executed using probabilistic model checker. The service instance pool is formally specified for management automation. The QoS based inverted index is employed to speed up service retrieval. The single-source service dynamic reconfiguration method and multi-source service dynamic reconfiguration method are proposed to cope with the failed service at local level. The two-stage compatibility checking is proposed to check the service software behaviors after carrying out a dynamic reconfiguration at global level, where the abstract refinement and compositional verification method will be introduced to relieve state space explosion. The service dependency graph (SDG) is constructed to give the service reputation, and the regression analysis is used to forecast services reliability. Finally, some supporting tools will be developed and integrated for practical applications. Our research will enhance the trustworthy and the quality of Web service.

以动态自适应配置作为处理服务失效的手段，采用概率模型检验方法保证配置的正确性和可靠性，研究Web服务软件的监控、动态配置、形式验证以及失效服务预测等问题。主要包括：在概率时间自动机模型框架下对运行时服务进行建模。采用扩展的LSC分类描述威胁模型，从威胁模型自动抽取满足足够正确性和可靠性的性质。用概率模型检验器检验服务模型，实现服务监控。研究服务实例池的形式化描述，实现服务实例管理和服务依赖关系管理自动化。研究基于QoS的倒排索引方法实现服务快速检索。研究基于单源服务的动态配置方法和基于多源服务的动态配置方法局部地处理失效服务。研究两阶段概率相容性检验方法，采用抽象精化手段优化和组合验证技术缓减状态空间爆炸问题。构造服务依赖图，给出服务信誉，采用回归分析方法预测服务可靠性；研究分层式预测方法。开发与集成相应的支持工具。该项研究对于提高Web服务的可信性和质量有重大意义。

可信的Web服务软件不仅需要满足预期用户对服务软件的功能性需求，而且在受到干扰(外部攻击、错误操作或环境影响)时，还需要具有连续提供服务的能力，不会出现用户需求以外的错误行为。定量模型检验方法作为模型检验技术的扩展，可以对计算机网络系统的时间约束，通信系统引起的不可靠、不可预测性行为进行建模和检验，实现性能评估。本课题针对Web服务软件的动态配置及可信性保障，以动态自适应配置作为处理服务失效的手段，采用概率模型检验方法保证配置的正确性和可靠性，研究Web服务软件的监控、动态配置、形式验证以及失效服务预测等问题。项目在Web服务组合可靠性建模与验证、服务系统可靠性分析与服务质量验证、服务流程的动态替换与验证、基于反例引导的抽象精化验证方法、使用概率模型检验的服务推荐、基于服务的系统设计的自动化定量验证支持工具以及移动计算与服务软件的测试验证方法等方面取得了研究成果。公开发表了期刊论文14篇、学术会议论文18篇，合计学术论文32篇，其中SCI检索6篇，EI检索22篇。获得授权发明专利2项、软件著作权1项。培养了研究生10多名，2名获博士学位，9名获硕士学位。承办了2个国际学术会议。该项目研究对于提高Web服务的可信性和质量有重要意义。