实时服务构件的语义特征和行为组装形式化技术研究

论文摘要

在面向服务的架构中,如何根据系统资源环境的变化以及构件的功能和实时性等QoS属性动态组合已有的功能构件以满足应用需求,成为当前此领域的一个研究热点。由于采用非形式化（自然语言）和半形式化（图表）方法描述实时服务系统均存在不精确、歧义的及不易验证等缺陷,而形式化方法能较好地克服上述不足,可充分表述系统的各种特性,并为系统的验证、实现等提供良好的基础。本文提出了一种结合OCL与HTA的实时服务构件（Real-Time ServiceComponent）形式化描述方法:用OCL描述构件的静态语义特征,用HTA描述构件的动态抽象行为;前者为后者的正确性提供属性约束,后者提供前者所描述需求的具体实现,两者语义互补。主要内容及其贡献包括:（1）提出一种基于特征的构件语义描述模型,首先分别给出特征、特征空间和构件特征空间表示模型的定义。接着将构件特征间的各种关联和依赖关系分成自身约束、父子关系约束、显性约束和隐性约束四类,并采用对象约束语言对这些关系进行形式化描述,从而为模型提供了精确的语义支持。面向电子商务的构件特征子树的实例研究及其模型验证和实验结果证明了该模型的正确性与有效性。（2）采用HTA形式化描述实时服务构件的动态抽象行为。给出实时服务构件的HTA模型,系统阐述构件间的各种组装方式及其形式模型,分析构件组装的语法可组合性和语义可组合性问题。采用HTA可层次地构造实时系统集成框架,较高层次的实时服务构件的行为可通过由较低层次的构件组成的HTA来定义。该模型的显著特点是简单容易理解,能在一个统一的框架中表示构件的组装、行为和分析系统性能,适用于不同粒度的实时服务构件集成,有效降低了实时服务系统的复杂度,从而使模型验证工具能够处理更为复杂的服务系统。（3）提出一种基于MLTS的实时服务构件HTA模型组装验证算法。给出（层次）自动机到标号迁移系统的转换过程,在标号迁移系统的扩展模型—多集标号迁移系统基础上,给出其组装算法,利用共享动作是否转换为内部动作来判定模型的组装兼容性。该算法能够有效降低状态空间爆炸给模型实例检测带来的难度,同时利用了MLTS能够描述系统同步、异步动作的特点,不仅可以跟踪构件组装前后的状态变化,而且能够刻画构件的接口行为动作变化,因此,它在基于HTA的实时服务构件模型组装兼容性验证方面具有较强的表达能力。（4）描述一个较简单但又具有典型实时服务系统特征的小额支付视频点播实例应用系统。首先采用自顶向下的方法构建系统,接着采用本文的描述方法对系统级的构件及其组装进行建模、分析和验证,并简单分析了系统的时间属性。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 研究背景与意义
• 1.2 主要研究内容
• 1.3 本文篇章结构
• 1.4 本章小结
• 第2章 实时服务构件研究综述
• 2.1 概述
• 2.2 实时服务构件
• 2.2.1 服务构件的概念
• 2.2.2 实时服务构件的基本特征
• 2.2.3 服务构件组合
• 2.3 形式化方法
• 2.4 模型验证技术
• 2.4.1 模型检测
• 2.4.2 模型检测工具
• 2.5 本章小结
• 第3章 基于OCL的实时服务构件语义特征描述模型
• 3.1 问题背景
• 3.2 对象约束语言OCL简介
• 3.2.1 OCL的特性
• 3.2.2 OCL的构成
• 3.2.3 OCL应用讨论
• 3.3 实时服务构件特征语义表示模型
• 3.3.1 构件特征表示模型
• 3.3.2 构件特征约束
• 3.4 实例分析
• 3.4.1 面向电子商务的构件特征树
• 3.4.2 模型的正确性
• 3.4.3 模型的有效性
• 3.4.4 模型的扩展性
• 3.5 相关工作比较
• 3.6 本章小结
• 第4章 基于HTA的实时服务构件形式化模型
• 4.1 问题背景
• 4.2 TA和HTA
• 4.3 实时服务构件的层次时间自动机模型
• 4.4 构件组装
• 4.4.1 绑定组装
• 4.4.2 连接组装
• 4.5 组装分析
• 4.5.1 非法状态
• 4.5.2 构件语义可组合
• 4.5.3 实例分析
• 4.6 相关工作比较
• 4.7 本章小结
• 第5章 基于HTA的实时服务构件组装模型验证算法
• 5.1 问题背景
• 5.2 LTS和MLTS
• 5.3 验证算法
• 5.3.1 算法的基本思想
• 5.3.2 算法描述
• 5.4 实例分析
• 5.5 相关工作比较
• 5.6 本章小结
• 第6章 实例分析:移动小额支付视频点播系统
• 6.1 引言
• 6.2 系统概况
• 6.2.1 系统体系结构
• 6.2.2 系统层次框架
• 6.2.3 系统业务流程
• 6.3 系统建模
• 6.3.1 构件的静态语义特征描述
• 6.3.2 动态行为建模
• 6.4 验证分析
• 6.5 本章小结
• 第7章 总结及展望
• 7.1 论文工作总结
• 7.2 进一步工作
• 参考文献
• 附录
• 攻读博士学位期间发表和录用的文章
• 参加的科研项目
• 致谢