中文摘要：

Web服务作为一种自治、开放和平台无关的网络化构件，使得软件开发技术和分布式应用具有更好的复用性。将已有的服务以静态或动态方式组合成一个新服务的思想，已影响到当今软件产品开发方式。然而，在如何保证服务组合的质量问题上，正面临着一些挑战如何在网络环境中保证独立的服务构件之间互操作行为和数据交换的正确性，如何解决发送方发送的消息可能永远不会被接受方接收，发送方和接收方存在死锁，两个服务进行交互时行为或数据不兼容等问题。所以在Web服务的设计阶段，保证Web服务组合建模的正确性尤为重要。基于形式化方法的Web服务组合建模技术就很有用，因为形式化方法具有清晰的语义，能够使用相应的工具来自动地分析和验证一个系统是否具有想要的属性，或者不具有不想要的属性。本课题从Web服务的动态组合出发，利用形式化和图形化结合的方式，研究如何对Web服务的行为一致性、时态属性、时间属性和概率属性进行建模和验证。

结论摘要：

本项目在充分理解WEB服务组合行为机理的基础上，研究了如何利用相关的形式化机制刻画组合服务的交互行为，研究了如何从用户端对WEB服务进行集成测试和回归测试，研究如何对WEB服务的各种场景进行建模，研究了如何描述服务组合过程中的各种属性描述机制，研究了如何对动态服务组合进行监控和属性验证等，并建立了一套比较完整的面向WEB服务测试、监控和验证的理论框架和试验支撑平台。 通过三年的研究和探索，本项目在理论和实验方面取得了如下主要成果（1）提出一种扩展的层次的有色Petri网（称为EH-CPN）对组合服务的行为进行建模，并在此基础上生成用于集成测试的测试用例；（2） 提出了一种BPEL控制流图（称为XBFG），针对WEB服务的各种演化情况，实现了对组合服务回归测试的测试用例选择和生成；（3）提出了属性序列图（PSC）的理论和方法，针对各种属性（包括安全性、行为一致性、时态属性、实时属性和概率属性等）进行监控和验证，取得良好的效果；（4）提出了一种全路径剖析方法，使得对WEB服务的执行路径的分析和控制得到有效管理；（5）提出了基于形式概念格的修改影响分析方法和基于切片谱的故障定位方法，使得在WEB动态演化过程中修改传播和故障定位更加有效。（6）开发了一个面向WEB服务测试、监控和验证的理论框架和试验支撑平台。 主要成果统计（1）出版专著1部；（2）录用和发表论文60篇，其中SCI国际期刊论文8篇（SCI已检索6篇），EI期刊和国际会议论文58篇（EI已检索40篇），ISTP检索6篇；（3）申报发明专利18项（其中2项已经获得授权）；（4）软件著作权登记11项；（5）培养博士生12名（其中2名已经获得博士学位），培养硕士生25名（其中10人已获得硕士学位），指导本科毕业设计10人；（6）6名青年教师在本项目中获得锻炼和提高。