基于统一过程的UML-B系统转换技术的研究

论文摘要

目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重压力。软件工程的一个主要目标就是在软件复杂性增加的情况下仍能构造正确可靠的系统,达到这一目标的途径之一就是形式化方法。形式化方法是一种用于规范、设计和验证计算机系统的基于数学的方法,包括各种语言、技术和工具等。使用形式化方法采用逐步渐进的方式来开发,可以提高软件可靠性和生产效率,实现软件自动化。统一建模语言UML已成为面向对象软件系统中描述分析和设计阶段模型的标准化记法,但UML在某些方面仍存在不足,首先,UML只是一种建模语言,而不是一种方法,因此在实际的开发和设计中,需要具体的过程技术来支持。其次,复杂系统的建模往往需要进行严格的语义分析,而UML缺乏精确的语义,因此对模型难以进行一致性检查和正确性分析,成为基于UML技术的严重缺陷。针对以上问题,本文提出了基于统一过程的UML到形式化的系统转换思想,将统一过程RUP、UML、形式化方法三者结合用于软件系统建模中。其中UML作为支持建模语言,其图形表示直观易理解;RUP作为建模中的方法指导,它与UML在实际开发过程中的结合,使系统的分析和设计过程变得清晰,降低了系统的开发风险;对UML进行形式化转换研究,可以将UML与形式化语言的的准确性、一致性结合起来,为模型的正确性证明、转换及一致性检查提供有力的理论方法。本文选择形式化方法中一种比较成熟的方法---B方法来描述UML模型图,B方法与其他形式化方法相比具有很多优点:B方法支持从软件需求规格说明、设计到最后实现的整个软件开发过程,并具有B-Toolkit、Atelier B、ProB等工具的全面支持。本文主要针对UML模型图中的用例图、类图、顺序图提出其到形式化B方法的转换机制,并对已存在的状态图的转换机制进行扩充,使其针对于某些特定的事例。对一个复杂的软件系统,软件开发人员可以在统一过程的指导下,通过UML中的各种图对目标系统进行建模,然后根据文中UML-B的转换方法,构建目标系统的B机器,从而建立一种从图形加文字的半形式化模型到具有数学基础的形式化模型的系统映射,在此基础之上,可以进一步地进行模型检测、正确性验证、代码半自动生成等工作。最后,结合了一个免疫系统中细胞免疫的实例,使用并验证了UML模型到B的系统转换方法,并在B方法支持工具（ProB）中对所得到的形式化模型进行了动态分析和模型检测,以保证规格说明的正确性和可靠性。

论文目录

• 摘要
• Abstract
• 第一章 引言
• 1.1 研究背景
• 1.2 国内外研究现状
• 1.3 论文研究意义
• 1.4 章节安排
• 第二章 相关知识介绍
• 2.1 UML
• 2.1.1 UML 的内容及建模机制
• 2.1.2 UML 的优劣
• 2.1.3 基于统一过程的UML 系统建模
• 2.2 形式化方法
• 2.2.1 形式化方法介绍
• 2.2.2 B 方法
• 2.3 UML 与形式化方法的结合
• 2.3.1 直接对UML 模型进行形式化语义定义
• 2.3.2 UML 到形式化方法的转换
• 第三章 UML-B 的系统转换研究
• 3.1 研究背景
• 3.2 UML 模型图的已有形式化工作及比较
• 3.2.1 类图的形式化
• 3.2.2 状态图的形式化
• 3.2.3 用例图的形式化
• 3.2.4 顺序图的形式化
• 3.2.5 活动图的形式化
• 3.3 用例图-B 的形式化转换
• 3.3.1 参与者
• 3.3.2 关系
• 3.3.3 用例
• 3.3.4 系统
• 3.3.5 用例图
• 3.4 UML 状态图-B 形式化转换的改进研究
• 3.4.1 简单状态图
• 3.4.2 层次状态图
• 3.4.3 并发状态图
• 3.5 UML 顺序图-B 形式化转换
• 3.5.1 顺序图中各元素的形式化表示
• 3.5.2 整个顺序图的机器表示
• 3.6 本章小结
• 第四章 UML-B 系统转换的实例研究
• 4.1 免疫系统
• 4.2 基于统一过程RUP 的细胞免疫建模
• 4.2.1 需求描述
• 4.2.2 用例模型
• 4.2.3 静态行为建模——类图模型
• 4.2.4 动态行为建模——状态模型、顺序模型
• 4.3 本章小结
• 第五章 系统精化及正确性证明
• 5.1 精化的定义及一般过程
• 5.2 对 IMMUNERESPONSE 实例机器的精化
• 5.3 实例机器的工具验证
• 5.3.1 类型检查
• 5.3.2 模型检测
• 5.4 本章小结
• 第六章 总结与展望
• 6.1 本文工作总结
• 6.2 进一步工作
• 参考文献
• 致谢
• 论文发表情况及参加科研项目、学术会议