可信的自治式服务协同系统验证

论文摘要

XML标准和面向服务的计算模式（Service-Oriented Computing,SOC）大大降低了跨域协同（Cross Organizational Cooperation,COC）系统的实现难度和实施成本,使多主体协同系统（Multi-Agent Cooperation System,MACS）、虚拟组织（Virtual Organization,VO）和E机构（E Institution）等跨域协同系统的大规模应用成为可能。但是跨域协同系统体系结构的复杂性,组件的分布性和异构性,以及执行过程的异步性使系统验证颇为困难。如何检验实现的系统能否达到预期目标,是否满足一致性、完备性等属性要求是此类系统设计和实现过程中面临的主要挑战之一。测试和形式验证是目前实现系统验证的主要途径。相比之下,传统测试方法由于无法保证测试过程覆盖系统全部执行路径而无法满足要求。基于形式化方法的自动形式验证理论和技术,凭借其严格性、精确性的特征和验证过程自动化的优势,成为目前COC系统验证的最佳选择。由于体系结构上的差异,我们无法设计通用的COC系统验证方案,但是对典型系统验证的研究能够为类似系统验证工作提供方法论上的指导,从而降低验证的实现难度。可信自治式服务协同系统（Trusted and Autonomic Service CooperationSystem,TASCS）是SOC计算模式下的新型可信跨域服务协同平台,涵盖了COC系统研究领域的主要理论和技术,因此其验证研究对于实现其他跨域协同系统验证有很大的参考价值。本文对跨域服务协同和自动形式验证理论和技术进行了深入的研究和探讨,提出了一种基于自动形式验证技术的TASCS验证方案,初步解决了它的验证问题,也为其他COC系统验证提供了有益的借鉴。论文的内容主要包括以下几个方面:首先,论文介绍了模型检验和形式语句判定过程这两种自动形式验证方法体系。讨论了自动形式验证的基本概念、理论、技术和主要验证工具,分析了这两种方法体系的适用性以及应用的约束和限制。其次,论文介绍了ebXML分布式协同理论和规范调控的多主体协同系统理论这两个TASCS的理论基础。前者是TASCS分布式业务流程的参考模型,后者则是TASCS可信机制的理论基础。提出了一种规范调控的多主体协同系统动态模型和基于模型检验的动态属性验证机制,为TASCS验证的实现提供了借鉴和参考。接着,论文提出了一种基于符号模型检验技术的TASCS动态属性验证方案。该方案建立了基于道义逻辑和命题逻辑的形式化规范语言及其状态集语义,通过与系统Kripke结构的结合实现了规范和协同系统动态模型之间的无缝衔接。在此基础上实现的系统动态属性符号模型检验算法解决了TASCS的动态属性验证问题。再次,论文对TASCS分布式业务流程设计和实现过程中面临的一致性问题进行了分析和归类,提出了一种基于形式语句判定过程的分布式业务流程一致性验证方案。该方案用命题逻辑或带未解释函数的等式逻辑语句描述待验证的一致性问题,借助形式语句有效性判定算法实现了对TASCS分布式业务流程一致性问题的验证。最后,论文介绍了医疗卫生领域人体器官/生理组织移植跨域协同系统体系结构,叙述了验证方案在在该系统中的实现过程,讨论了该方案的优点和不足,以及它对类似模型验证的指导意义。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 引言
• 1.2 研究背景与动机
• 1.3 相关领域研究概述
• 1.3.1 基于XML的电子商务模型概述
• 1.3.1.1 电子商务技术的演变
• 1.3.1.2 ebXML电子商务模型
• 1.3.1.3 ebXML和其他基于XML的电子商务标准的比较
• 1.3.2 规范调控的多主体协同系统概述
• 1.3.3 形式验证方法概述
• 1.4 研究目标和内容
• 1.5 论文组织结构
• 第2章 自动形式验证理论和技术
• 2.1 引言
• 2.2 自动形式验证理论和技术简介
• 2.3 基于模型检验自动形式验证技术
• 2.3.1 模型检验方法概述
• 2.3.2 Kripke结构
• 2.3.3 时态逻辑
• 2.3.4 显式状态模型检验
• 2.4 基于判定过程的自动形式验证技术
• 2.4.1 判定过程简介
• 2.4.2 基本概念和定义
• 2.4.3 命题逻辑判定过程
• 2.5 本章小结
• 第3章 规范调控的可信自治式服务协同系统模型
• 3.1 引言
• 3.2 ebXML分布式服务协同模型
• 3.2.1 ebXML分布式服务协同模型简介
• 3.2.2 业务处置
• 3.2.3 商务协同
• 3.2.4 ebXML服务协同模型中存在的问题
• 3.3 规范调控的多主体协同系统模型
• 3.3.1 规范的特征和形式
• 3.3.1.1 规范及其特性
• 3.3.1.2 规范的形式
• 3.3.1.3 形式化的规范和规范集
• 3.3.2 规范调控的多主体协同系统模型
• 3.3.2.1 主体模型
• 3.3.2.2 系统抽象模型及其语义
• 3.3.3 系统推理和动态属性验证
• 3.4 可信自治式服务协同系统模型
• 3.5 本章小结
• 第4章 可信自治式服务协同系统动态属性验证
• 4.1 引言
• 4.2 验证问题分析
• 4.3 符号模型检验
• 4.3.1 模型的符号化表示
• 4.3.2 二分决策图
• 4.3.3 系统CTL属性验证方法
• 4.4 服务协同系统的形式化描述及其语义建模
• 4.4.1 协同行为规范的形式化描述
• 4.4.2 规范Kripke结构及其CTL语义
• 4.5 服务协同系统动态属性验证
• 4.6 本章小结
• 第5章 可信自治式服务协同系统流程一致性验证
• 5.1 引言
• 5.2 E机构分布式业务流程一致性问题分析
• 5.3 基于命题逻辑判定过程的编排一致性验证
• 5.4 基于EUF的角色承担关系一致性验证
• 5.4.1 等式逻辑和未解释函数
• 5.4.2 基于EUF的角色承担关系判定过程
• 5.5 直运销售模式服务协同过程验证
• 5.6 本章小结
• 第6章 可信自治式服务协同系统验证实例分析
• 6.1 引言
• 6.2 器官/生理组织移植多方协同过程介绍
• 6.2.1 协同系统体系结构
• 6.2.2 协同系统核心分布式业务流程简介
• 6.3 器官/生理组织移植应用域E机构实现
• 6.3.1 E机构协同行为规范的实现
• 6.3.2 E机构社交结构标准的实现
• 6.4 器官/生理组织移植服务协同系统验证
• 6.5 本章小结
• 第7章 总结与展望
• 7.1 本文工作总结
• 7.2 未来工作展望
• 参考文献
• 攻读博士学位期间主要的研究成果
• 致谢