UML建模的形式化方法研究和应用

论文摘要

统一建模语言(UML)是目前比较成熟的建模语言,运用非常广泛。UML支持面向对象的分析与设计,提供了一批基本的表示模型元素的图形和方法,能简洁明了地表达面向对象的各种概念和模型元素,用于对软件进行描述、可视化处理、构造和建立软件系统制品的文档等。作为一种图形化语言,UML模型图形能清晰地表示系统的逻辑模型或实现模型,其强大表达能力使它可以用于各种复杂类型的软件系统的建模。但是,UML也存在缺乏精确的语义、不够精练、存在二义性及结果的正确性难以验证等问题。形式化方法是建立在严格数学基础上的软件开发方法,能够精确地、无二义地描述系统,并且有严格的证明。B方法是一种较为实用的形式化软件开发方法,覆盖了从抽象规约到可执行代码生成的过程,拥有强有力的支持工具。B方法使用抽象机符号(AMN)来构造模型,并支持规范说明的类型检测和动态验证。B方法的支持工具可用动画等方式模拟运行规范说明,根据需求和测试场景检查获得的规范说明是否符合需求,对提高软件的可靠性有着非常显著的作用。UML与B方法的有机结合,既保留了UML在建模方面的优势,又弥补了UML的不足。B方法为UML模型提供精确的语义参考,有助于消除UML模型的歧义、模型内部及模型之间的不一致性。同时,直观易懂的UML模型图降低了直接使用B方法的难度,加强了形式规约的可理解性和可维护性。二者的有机结合提高了软件开发的精确性和效率。本文首先分析了B方法的数学基础和抽象机理论,简单介绍了UML语言,在此基础上,分别给出了UML的类图和状态图的B方法的形式化描述。软件开发过程中,首先结合UML类图和状态图对目标系统建模,再依据文中所给出的转换方法构建目标系统的B方法形式化描述,然后利用B方法支持工具对规约进行动态分析和验证,得出可靠的形式规约,为进一步的精化和实现提供正确的起点。最后,文章以当前物流管理中最重要的订单管理系统为例,建立订单管理系统UML类图和状态图,实现系统类图和状态图的B方法形式化描述,并完成系统的模型检测。

论文目录

• 摘要
• Abstract
• 目录
• 第一章 绪论
• 1.1 研究背景
• 1.2 研究意义
• 1.3 国内外研究情况
• 1.4 论文的总体结构
• 第二章 B方法
• 2.1 形式化方法综述
• 2.2 B方法简介
• 2.3 B方法数学基础
• 2.4 抽象机
• 2.5 精化和实现
• 2.6 证明义务
• 2.7 ProB工具
• 第三章 统一建模语言UML
• 3.1 UML发展的历史
• 3.2 UML语义的模型框架
• 3.3 UML模型图简介
• 3.4 UML形式化语义研究
• 第四章 UML类图及状态图的B方法形式化描述
• 4.1 UML类图的B方法形式化描述
• 4.2 UML状态图的B方法形式化描述
• 4.3 小结
• 第五章 实例应用
• 5.1 订单管理系统描述
• 5.2 系统需求的UML模型图
• 5.3 系统UML模型图的B方法形式化描述
• 5.4 系统的ProB模型检测
• 5.5 小结
• 第六章 总结
• 参考文献
• 附录
• 发表论文和参加科研说明
• 致谢