学位论文 > 优秀研究生学位论文题录展示

UML模型图到B方法形式规约的转换研究与应用

作　者: 吴帅
导　师: 杨庆红
学　校: 江西师范大学
专　业: 计算机软件与理论
关键词: 形式化方法 B方法抽象机 UML 类图状态图 ProB
分类号: TP311.52
类　型: 硕士论文
年　份: 2007年
下　载: 227次
引　用: 6次
阅　读: 论文下载

内容摘要

形式化方法(Formal Method)基于严格的数学理论,能产生精确、无二义性的形式规约,为软件开发提供了严格的数学基础,对提高软件的可靠性有着非常显著的作用。形式化方法要求开发者具有良好的数学基础,并使用严格的数学符号去编写规约,这使得很多软件开发者难以接受。同时,形式规约不够直观,可读性较差,不便于与用户进行交流。因此,形式化方法的研究和应用仍然局限在较小的范围之内。UML是一种可视化的图形建模语言,采用直观的图形表示法为系统进行建模,能得到图形化的软件规约,已在面向对象分析和设计中成为事实上的工业标准。但是,UML的许多概念都基于非形式化语义,对模型的描述不够准确,容易产生模糊或歧义,缺乏精确的语义,不便于使用工具对其描述的规约进行动态分析和验证。形式化方法和UML存在很大的互补性,形式化方法恰好能在精确语义方面弥补UML的不足,能够对UML建模结果进行一致性检查和正确性分析。同时,UML可以降低直接使用形式化方法的难度,增加形式化方法在软件开发中的实际作用。二者的结合研究将对提高软件的可靠性有着非常重要的意义。在分析UML模型图特点的基础上,本文选择B方法作为UML模型图的形式规约方法,一是因为B方法具有面向对象的类似特征,可以使UML模型图到B方法形式规约的转换过程直观易懂;二是因为B方法有一整套严格的理论分析方法和工具,弥补了UML模型图缺乏验证工具的不足;三是因为B方法支持软件开发的几乎全过程,包括规约、精化、代码生成、正确性验证等。本文中,我们主要针对UML模型图的类图和状态图,分别给出二者到B方法形式规约的转换方法。软件开发人员可以首先结合UML类图和状态图对目标系统进行建模,然后根据文中所给出的转换方法,构建目标系统的B方法形式规约,再利用B方法支持工具对规约进行动态分析和验证,得出可靠的形式规约,并为在此基础上进行的形式推导和精化提供了正确的起点。最后,结合了一个电梯实例,说明了UML模型图到B方法形式规约的转换方法及过程,并在B方法支持工具(ProB)中对所得到的形式化模型进行了动态分析和模型检测。

全文目录

摘要  2-3
ABSTRACT  3-6
第一章绪论  6-9
  1.1 研究背景  6-7
  1.2 论文的研究内容及主要工作  7-8
  1.3 论文的内容组织  8-9
第二章形式化方法和B 方法  9-22
  2.1 形式化方法  9-12
  2.2 B 方法  12-22
第三章统一建模语言UML  22-27
  3.1 UML 基本概述  22-23
  3.2 UML 的框架  23
  3.3 UML 模型图  23-26
  3.4 UML 存在的问题  26-27
第四章 UML 模型图到B 方法形式规约的转换  27-41
  4.1 UML 类图到B 方法形式规约的转换  27-34
  4.2 UML 状态图到B 方法形式规约的转换  34-40
  4.3 小结  40-41
第五章实例分析  41-51
  5.1 系统描述  41
  5.2 系统的UML 模型图  41-43
  5.3 系统UML 模型图的B 方法描述  43-47
  5.4 系统形式规约的模型检测  47-50
  5.5 小结  50-51
第六章总结与展望  51-52
参考文献  52-55
附录  55-64
致谢  64-65

UML模型图到B方法形式规约的转换研究与应用

内容摘要

全文目录

相似论文