运用形式化B方法进行软件开发

VIP免费
3.0 陈辉 2024-11-20 4 4 495.82KB 79 页 15积分
侵权投诉
目 录
第 1 章 绪论 .......................................................... 1
§1.1 研究形式化方法的必要性 ..................................... 1
§1.2 形式化方法的使用方式及实质 ................................. 2
§1.3 形式化方法和常规方法的比较 ................................. 3
§1.3.1 形式化方法与软件测试的关系 ........................... 4
第 2 章 B 方法 ........................................................ 6
§2.1 形式化方法与 B 方法之间的关系 ............................... 6
§2.2 B 方法的起源和发展 ......................................... 7
§2.3 B 方法的主要特点 ........................................... 7
§2.4 B 方法的抽象机器符号 AMN .................................... 8
§2.4.1 静态行为——描述状态 ................................. 9
§2.4.2 动态行为——描述操作 ................................. 9
§2.4.3 广义代换语言 GSL .................................... 10
§2.5 形式化方法 B 与 UML 表示方法的比较 .......................... 11
第 3 章 B 方法的数学理论基础 ......................................... 13
§3.1 数学推理 .................................................. 13
§3.2 集合论 .................................................... 14
§3.2.1 集合的基本结构 ...................................... 14
§3.2.2 二元关系 ............................................ 15
§3.2.3 函数关系 ............................................ 16
§3.2.4 序列 ................................................ 16
§3.2.5 类型检查 ............................................ 17
§3.3 数学对象 .................................................. 17
§3.4 广义代换与集合论模型 ...................................... 18
第 4 章 利用 B 方法对软件系统进行规范 ................................. 19
§4.1 运用 B 方法进行软件开发的实施方案 .......................... 19
§4.1.1 非形式的规范 ........................................ 19
§4.2 用 B 方法来对一个软件系统进行规范 .......................... 20
§4.2.1 机器 Student ........................................ 21
§4.2.2 机器 Course ......................................... 22
§4.2.3 机器 Elective ....................................... 24
§4.2.4 机器 Elective_System ................................ 28
§4.3 B 方法规范与面向对象程序设计的对照 ........................ 29
§4.4 编码 ...................................................... 32
§4.4.1 类 Student .......................................... 32
§4.4.2 类 Course ........................................... 33
§4.4.3 类 Elective ......................................... 34
§4.4.4 类 ElectiveSystem ................................... 36
§4.5 抽象机与类 ................................................ 39
第 5 章 精化和实现 ................................................... 40
§5.1 精化和实现的定义 .......................................... 40
§5.2 精化和实现的实例 .......................................... 41
§5.2.1 BASIC 机器 .......................................... 42
§5.2.2 主界面 MAIN_INTERFACE 机器 ........................... 44
§5.2.3 功能实现部分 INNER_INTERFACE 机器 .................... 48
§5.2.4 数据库 DATA_BASE 机器 ................................ 51
§5.2.5 查询部分 QUERY 机器 .................................. 54
§5.2.6 有关对象的机器 ...................................... 58
§5.2.7 DATA_BASE 机器的实现 ................................ 63
§5.2.8 文件机器 BASIC_FILE_VAR ............................. 66
§5.2.9 有关对象机器的实现 .................................. 68
§5.3 系统体系结构图 ............................................ 70
§5.4 规范与精化、实现的比较 .................................... 71
第 6 章 总结与展望 ................................................... 72
参考文献 ............................................................ 73
在读期间公开发表论文和承担科研项目及取得成果 ........................ 75
致 谢 ............................................................... 76
第１章 绪论
1
第1章 绪论
本章主要介绍了研究形式化方法的必要性，以及在软件开发中使用形式化方
法的实质和使用方式，并给出了形式化方法与常规方法在开发软件产品方面，以
及和软件测试在保证软件系统正确性方面分别进行了比较，因而进一步指出了形
式化方法对促进今后软件系统的发展有着深远意义。
§1.1 研究形式化方法的必要性
首先来讨论一下为什么要研究软件形式化方法[1]？
随着计算机应用逐步渗透到社会生产生活的各个领域，一方面计算机被看作
是现代科学技术开发出的最强有力的工具，不断改变着我们的工作和生活；另一
方面，促成这种变化的领域本身的情况并不乐观，计算机系统的不可靠也已成为
人所共知的事实。计算机正在越来越多地控制着我们周围的环境，一些系统的失
误可能给人们的生命财产造成巨大损失。因此也就有必要从各种角度研究软件开
发的本质和规律性，进一步提高软件开发水平，来保证我们所开发的软件系统的
质量。软件形式化方法就是这样的一个研究领域，我们研究软件形式化方法总的
目标就是希望改变目前这种基于个人技术，缺乏科学指导的软件开发方式，为将
来的软件开发过程和作为其产品的软件系统提供更坚实的科学基础。
计算机软件系统作为软件开发的最终产品，也是人类有史以来制造出的最复
杂的产品，可具有成百万甚至成千上万行代码的规模，其各个组成部分之间可能
存在错综复杂的直接或间接的交互作用方式，其静态结构与动态行为之间构成了
难以琢磨的关系。形式化方法可以为计算机软件系统建立坚实的理论基础，并将
其规范化和严格化。
形式化方法在软件开发中能够起到的作用是多方面的。
首先是对软件要求的描述。软件要求的描述是软件开发的基础。比如说一般
非形式化的描述很可能导致描述的不明确和不一致。如果描述不明确并且不一致
很容易导致设计、编程的错误，将来的修改所要付出的代价就非常大了。如果导
致的错误没有被发现，则最终会影响到程序使用的可靠性。形式化方法要求描述
明确，因而描述的不一致性也就相对易于发现。
其次是对软件设计的描述。软件设计的描述和软件要求的描述一样重要。形
式化方法的优点对于软件要求的描述同样适用于软件设计的描述。另外由于有了
软件要求的形式化描述，可以检验软件的设计是否满足软件的要求。对于编程来
讲，可以考虑自动代码生成。对于一些简单的系统，形式化的描述有可能直接转
换成可执行程序，这就简化了软件开发过程，节约了资源和减少了出错的可能性。
运用形式化 B 方法进行软件开发
2
另外，形式化方法可以用于程序的验证，以保证程序的正确性。对于测试来
讲，形式化方法可用于测试用例的自动生成，这可以节约许多时间和在一定程度
上保证测试用例的覆盖率。总之，形式化方法是建立在严格的数学基础上的方法，
它是数学上的综合分析技术的应用，用于开发计算机控制的系统，经常有推理工
具的支持，它可提供一个用于设计和分析模型的严格而有效的途径。从而使系统
具有较高的可信度和正确性，并能使系统具有良好的结构，使其易维护，关键是
能较好地满足用户需求。
§1.2 形式化方法的使用方式及实质
形式化方法是一种用于规范、设计和验证计算机系统的基于数学的方法，包
括各种语言、技术和工具等。形式化方法可有两种不同方式来使用，第一种方式，
它们可用于生成规范，然后将此规范作为传统系统开发的基础。这种情况下，数
学将被用作为生成规范的主要工具。形式化规范好处在于：精确、抽象、简明和
可操作。操作可以包括规范的一致性检查、原型的自动生成或通过证明的方法推
导出规范的一些特殊性质。第二种方式，形式化规范以上述方式产生然后将其作
为验证程序正确性的依据。在第二种方式下具有与第一种方式类似的益处，除此
之外，还可以利用形式化方法证明规范及其相应程序的正确性，以表明程序与其
规范的一致性，这样可使软件开发有可能具有与数学证明同样的确定性。
形式化方法原则上就是用数学与逻辑的方法来描述和验证软件。从描述上讲，
一方面是系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语
言来描述。这些语言包括命题逻辑，一阶逻辑、高阶逻辑、代数、状态机、并发
状态机、自动机、计算树逻辑、线性时序逻辑、进程代数、 π-演算、 μ-演算、
特殊的程序语言，以及程序语言的子集等。从验证来讲，主要有两类方法，一类
是以逻辑推理为基础，另一类则以穷尽搜索为基础。逻辑推理有 natural deduction、
sequent calculus、resolution 以及 Hoare-logic 等方法。穷尽搜索方法统称为模型
检测。这类方法与系统或程序以及系统性质的表示有很大的关系，比如说符号模
型检测，其基本原理是用命题逻辑公式表示状态转换关系，用不动点算法计算状
态的可达性以及这些状态是否满足某些性质。
总之，形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式
化开发。形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言)做
描述。形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通
过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。这样的验
证当然得建立在严格的语法语义的基础之上的。在实际应用中，这是不容易做到
第１章 绪论
3
的。形式化方法研究的目的就是希望能够提供更好的理论、方法和工具，扩大形
式化方法的应用范围和使用价值。
§1.3 形式化方法和常规方法的比较
形式化方法和工程界的常规方法相比有明显的区别，它们的开发原则不同，
形式化方法希望能直接构造出尽可能正确的系统，而常规方法主要是通过测试来
发现系统的错误。形式化方法和常规方法开发软件产品的比较[2]图1如下：
需求分析
设计
编码
测试
(a) 常规的软件工程方法开发软件产品图
图1常规方法和形式化方法比较图
开发原则不同决定了开发模式的差别。在使用形式化方法的开发过程中需求
分析和设计阶段投入了很大的工作量，需要的工作量通常占软件开发全部工作量
的55％-65％，而编码和测试阶段的工作量相对较小，只占工作量的 35％- 45％。
而常规的工程开发方法的编码和测试阶段所需的工作量非常大，要占到全部工作
量的 60％-70％。另外下面图（b）所示的形式化开发方法是一种理想情况，一般
的工程项目只是在部分阶段使用形式化方法，或者是把形式化方法和其他软件开
发方法结合起来使用。
用户需求
自然语言、图形等表示的规范说明
常规的精化方法；如总体设计、详细设计等
人工编码，单元测试
模块测试，系统测试
最终产品
摘要：

目录第1章绪论..........................................................1§1.1研究形式化方法的必要性.....................................1§1.2形式化方法的使用方式及实质.................................2§1.3形式化方法和常规方法的比较.................................3§1.3.1形式化方法与软件测试的关系...........................4第2章B方法.............................

展开>> 收起<<
运用形式化B方法进行软件开发.pdf

共79页,预览8页

还剩页未读， 继续阅读

相关推荐

更多
立即下载
作者：陈辉 分类：高等教育资料 价格：15积分 属性：79 页 大小：495.82KB 格式：PDF 时间：2024-11-20

开通VIP享超值会员特权

  • 多端同步记录
  • 高速下载文档
  • 免费文档工具
  • 分享文档赚钱
  • 每日登录抽奖
  • 优质衍生服务

作者详情

相关内容

更多

推荐作者

热门标签

/ 79
评分 收藏
分享
立即下载 VIP免费下载
客服
关注