新型网络下可信服务协同的建模与验证技术研究

随着传感器、移动设备、电子控制设备的成熟和广泛应用，Internet与这些物理设备通过互联将形成新型网络，如物联网、CPS等。面向新型网络的软件系统需解决自主适应、在线演化、可信保障等方面的技术挑战。针对新型网络环境的高动态性、网络化软件的高灵活性和高复杂性、构成服务的自治性等特征及安全攸关的高可信要求，以面向新型网络为1个重点目标，从服务协同系统的结构和行为2个层次，开展系统建模、验证和模型转换3个方面的基础理论和关键技术研究，具体包括：协同结构的可信约束与满足性判定方法，支持演化的协同行为描述语言及验证方法，面向自主适应的模型转换方法。最终形成支持可信演化的服务协同框架体系，为新型网络下面向服务软件系统的设计和分析提供可用的关键技术。

围绕支持自主适应、在线演化和可信保障的面向服务软件建模与验证的基础理论与关键技术为核心，本课题从服务协同的结构和行为两个层面开展研究，基本解决了新型网络下面向服务软件系统的设计和分析技术问题，形成了支持自主适应、在线演化和可信保障的面向服务软件建模与验证的关键技术，取得了创新性研究成果，并达到了项目预期的研究目标。取得的主要成果包括：（1）在协同结构层面上，研究了服务协同结构的基本模型，为未来新型网络环境中服务系统的结构设计和自治管理提供了一种系统架构层面的形式模型；研究了服务协同结构可信约束的分解与满足性判定技术，为自治式复杂服务系统的运行提供了结构约束和运行机制，并保证系统相关质量属性；（2）在协同行为层面上，研究了支持演化的协同行为规约与验证方法，提出了模式扩展的线性时序逻辑，解决了复杂服务系统的动态演化中服务协同行为规约和关键性质难以刻画的问题，并提出了形式验证的算法；研究了协同服务的可信执行与安全机制，为服务可信执行的运行平台中服务协议处理正确性提供了一种验证方法，为服务可信执行中多安全协议的灵活集成提供了一种策略框架。（3）在可信服务协同机制方面，研究了基于 QoS 的服务协同动态重构方法，为新型网络环境下大规模组合服务动态重构提供了高效的实现机制；研究了面向数据的轻量级协同服务封装技术，为新型网络环境下大规模、异构数据的共享及封装服务的高效协同提供了一种轻量级的实现技术；研究了基于 QoS的分布启发式服务选择方法，为新型网络环境下保证QoS的动态服务协同提供了一种服务搜索方法。相关研究成果发表在International Journal of Web and Grid Services、Computing、Earth Science Informatics、Computer Methods and Programs in Biomedicine等期刊以及SCC、APSCC、ICEBE等国际会议上，共发表高质量论文15篇，其中SCI检索6篇。申请国家发明专利3项，国际发明专利1项。培养博士生6名，硕士生1名。