对软件需求的描述：非形式化的描述很可能导致描述的不 明确和不一致；形式化方法则要求描述的明确性，而描述的 不一致性也就相对易于发现。 对软件设计的描述：软件设计的描述和软件需求的描述一 样重要。 对于编程：自动代码生成。 对于测试：测试用例的自动生成。
20
软件开发中为什么使用形式化方法
• 保证质量的需要
➢ 模型验证：是否满足需求及具有所期望的特性； ➢ 模型变换：从模型表示向计算机系统变换的过程。
• 这些任务对应三方面的活动：形式化规约、形式化验证、 程序求精
25
形式化方法的发展
• 20世纪60年代：程序正确性证明研究 • 20世纪80年代：硬件电路设计的形式化方
法应用（时序逻辑和模型检验的诞生） • 20世纪90年代：通信协议和智能控制系统
正错误代价高昂 发布运行软件时常崩溃，维护代价依然很高
正如许多软件工程方法所指出的，即使遵
循了很多优秀设计准则和优良编码规范，
程序仍可能包含很多错误，因此，使用一
些方法来消除程序中的人为错误就变得更
加重要了。
19
软件开发中为什么使用形式化方 法
形式化方法的目的是为开发过程提供一些技术和 工具，用于发现并指出软件实现中潜在的缺陷问 题。
经典案例及应用
• Praxis公司于1992年交付给英国民航局的信息显示 系统是伦敦机场新空中交通管理系统的一部分。 在该系统的需求分析阶段，形式化描述和非形式 结构化的需求概念相结合；在系统规格阶段，采 用了抽象的VDM模型；在设计阶段，抽象VDM细 化为更为具体的规格。项目开发的生产效率和采 用非形式化技术相当，甚至更好。同时，软件质 量得到了很大的提高，软件的故障率仅为0.75每 千行代码，大大低于采用非形式化技术所提供的 软件的故障率（约为2~20每千行代码）。
• 软件危机主要表现如下几个方面
① 开发成本昂贵 ② 项目进度难控 ③ 修改维护困难 ④ 质量无法保证
11
项目进度难控
•为软件开发制定进度是很困难的事 情。如有10人月的工作量，则由一 个人完成需要10个月，由10个入完 成则需要一个月。但这种工作量估计 方式仅对各部分工作互下干扰的情况 下才适用，但作为整体，尚需讨论合 作，这种讨论交流活动就增加了工作
– 为了得到高质量的软件，企业要采用最好的实 践，使他们的软件过程变得成熟起来。形式化 方法是一种前沿技术，研究表明，这种技术非 常有助于那些希望把软件产品的缺陷出现率减 到最小的公司。
• 节约成本的需要
– 有证据显示，形式方法的使用减少了项目成本。 例如，IBM的大型CICS事务处理项目的独立审核 表明，9％的成本节约要归功于形式方法的使用。 对T800型变换计算机的Inmos浮点单元的独立审
• 分析问题、解决问题的能力，锻炼逻辑思 维。
课程参考教材
• 《软件开发的形式化方法》，古天龙编， 2005，高等教育出版社
• 课程PPT
课程考核
• 总成绩 = 课程作业（50%） + 期末考试（50%）
形式化思想
• 广义上，舍弃事物物质内容，只取形式结 构，只考虑形式不考虑内容的一种看待、 处理问题的思想。
中的形式化方法应用（工业界应用高速发 展） • 本世纪：交互式并发软件系统的形式化方 26
经典案例及应用
• 牛津大学和Hursley实验室于20世纪80年代 合作将Z语言用于IBM商用信息控制系统。 IBM对整个开发进行的测试表明，Z语言的 应用明显地改善了产品质量、大量减少了 错误和早期诊断错误。IBM估计使总体开发 成本降低9％。这一成果获皇家技术成就奖。
22
哲学家吃饭问题
• N个哲学家围着桌子坐， 桌子上有N个筷子
• 哲学家想吃饭时总是先 拿起右边的筷子再拿起 左边的筷子
• 哲学家只有得到2个筷 子后才能吃饭
形式化方法
Formal methods are mathematically based languages, techniques and tools for specifying, designing and verifying hardware and software systems.
形式化方法讨论
• 形式化方法中的抽象数学符号及理论确实对软件工程师的 使用带来一些不便，以致于人们要花一定的时间和精力去 学习和掌握。但是，采用形式化方法可以极大地减少了系 统设计开发早期阶段的错误，避免了后期错误修改所带来 的高额成本开销，这样早期人员培训的成本开销会在后期 的系统测试和维护中的高额回报中得到补偿，在某种程度 上还降低了软件开发的成本。同时，采用形式化方法还会 提高系统的设计开发效率，并且形式化方法是高质量、高 可靠软件开发的有效途径，是软件自动化的根本前提。形 式化方法不会完全代替传统的软件开发方法和面向对象方 法，需要根据所解决问题的特点结合或选择使用。
15
软件质量的重要方面
16
如何解决软件危机
软件工程方法
SoftwaBiblioteka e Engineering• 软件工程：工程化软件开 发过程控制与管理，追求 软件设计、生产、维护的 规范化及科学化 。
• 不规范 → 规范；不严格 → 严格；无方法/技术 → 成 熟的方法/技术。
17
软件工程中的生命周期
• 五个活动
推理过程
7
例子：电梯控制系统（程序语言描述）
8
例子：电梯控制系统（有限状态机描
述）
一种具有良好语法和语义定义的形式描述方法
有效支持以自动机理论为基础的形式化验证过
程
9
软件的规约表示
• 软件的规约表示可以采用非形式化的方式来描述，包括自然语言、图、 表等，也可以采用形式化方式来描述。
• 由于非形式化方法本身所存在的矛盾、二义性、含糊性，以及描述规 约时的不完整性、抽象层次混杂等情况，使得所得到的规约不能准确 地刻画系统模型，甚至会为后来的软件开发埋下出错的隐患。
• 而对于形式化方法来说，由于其基于严格的数学，具有严格的语法和 语义定义，从而可以准确地描述系统模型，排除了矛盾、二义性、含 糊性等情况，最终得到一个相对完整、正确的系统模型。
10
软件危机
• 1968年，NATO会议提出了“软件危机”一 词
• 软件危机包含两方面问题
① 如何开发软件，以满足不断增长、日趋复杂的需求； ② 如何维护数量不断膨胀的软件产品。
31
12
软件维护困难
• 软件的维护任务特别重。 • 正式投入使用的商用软件，总是存在着一定数量
的错误。随着时间延伸，在不同的运行条件下， 软件就会出故障，就需要修改维护。
• 软件维护不是更换某种备件，而是要纠正逻辑缺 陷。当软件系统变得庞大，问题变得复杂时，常 常会发生“纠正一个错误带来更多新的错误！”
• 以数学为例，可以表示为完全形式化的东 西，一切数学都可以由符号加以形式地表 述。
– 概念形式化：
– 原理形式化：勾股定理
• 在三角形ABC中，∠C=90。，则三条边a,b,c满足
例子：电梯控制系统（自然语言描述）
6
例子：UML描述（半形式化）
一种具有良好语法和语义定义的形式描述方法
但无法或很少支持以数学为基础的形式分析和
➢ 需求分析和规格 ➢ 软件设计：逻辑模型转换为软件方案，总体结构、模
块算法 ➢ 代码编写 ➢ 软件测试：模块测试、组装测试、整体测试 ➢ 运行维护
18
软件工程 vs 形式化方法
软件工程方法试图指导软件的开发过程。
然而问题依然存在
项目成本、进度依然无法保证 软件开发的后续阶段常常发现许多前期设计错误，更
软件形式化方法
陈铁明/王婷 tmchen/wangting@
课程介绍
• 通过本课程的学习，使同学了解软件开发 中形式化方法的基本概念和原理，掌握几 种常用的软件系统形式化描述方法（有限 状态机、CSP、Z语言、时序逻辑等）和验 证方法，并能够应用这些技术对软件系统 进行形式描述和分析。
13
典型的软件项目开发
14
质量无法保证
• Therac-25是加拿大原子能公司AECL和一家法国公司CGR联合开发的一种医 疗设备，它产生的高能光束或电子流能够杀死人体毒瘤而不会伤害毒瘤 附近的人体健康组织。在1985年6月到1987年1月，因为软件缺陷引发了6 起由于电子流或X-光束的过量使用的医疗事故，造成4人死亡、2人重伤的 严重后果。
经典案例及应用
• 加州大学的安全关键系统研究组所开发的 空中交通防碰撞系统的形式化需求规格 TCASII，采用了基于Statecharts的需求状态 机语言RSML，解决了开发过程中遇到的许 多问题。TCASII项目表明了复杂过程控制系 统列写形式化需求规格的可能性以及应用 工程师们不经任何专门培训建立易读且易 评判的形式化规格的可行性。
形式化方法是渗透在软件生命期中各个环 节（需求分析、设计、实现、测试等）的 数学方法或者具有严格数学基础的软件开 发方法。
形式化方法的基本含义是借助数学的方法
来研究计算机科学中的有关问题。
24
形式化方法的主要内容
• 形式化开发过程的任务分为：模型获取、模型验证、模型 变换
➢ 模型获取：从现实世界向模型表示转换，对应软件生命周期中的 需求分析、规格、设计活动；
• 1996年，欧洲航天局阿丽亚娜5型（Ariane5）火箭在发射后40秒钟后发生 爆炸，2名法国士兵当场死亡，损耗资产达10亿美元之巨，历时9年的航 天计划因此严重受挫。爆炸原因在于惯性导航系统软件技术要求和设计 的错误。
• 2011年7月23日20时30分05秒，由北京南站开往福州站的D301次列车与杭 州站开往福州南站的D3115次列车发生动车组列车追尾事故，造成40人死 亡、172人受伤，中断行车32小时35分，直接经济损失19371.65万元。根 据初步掌握的情况分析，“7·23”动车事故是由于温州南站信号设备在设 计上存在严重缺陷，遭雷击发生故障后，导致本应显示为红灯的区间信 号机错误显示为绿灯。