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