软件形式化方法讲解

《软件形式化方法讲解》由会员分享，可在线阅读，更多相关《软件形式化方法讲解（31页珍藏版）》请在金锄头文库上搜索。

1、软件形式化方法 陈铁明/王婷 tmchen/wangting 课程介绍 通过本课程的学习，使同学了解软件开发 中形式化方法的基本概念和原理，掌握几 种常用的软件系统形式化描述方法（有限 状态机、CSP、Z语言、时序逻辑等）和验 证方法，并能够应用这些技术对软件系统 进行形式描述和分析。 分析问题、解决问题的能力，锻炼逻辑思 维。 课程参考教材 软件开发的形式化方法，古天龙编， 2005，高等教育出版社 课程PPT 课程考核 总成绩 = 课程作业（50%） + 期末考试（50%） 形式化思想 广义上，舍弃事物物质内容，只取形式结构，只考 虑形式不考虑内容的一种看待、处理问题的思想。 以数学为例，

2、可以表示为完全形式化的东西，一切 数学都可以由符号加以形式地表述。 概念形式化： 原理形式化：勾股定理 在三角形ABC中，C=90。，则三条边a,b,c满足a2+b2=c2 具有两个基本特点： 自然语言符号化，抽象概括为形式语言； 对直观意义的推理关系进行语义刻画和语法刻画。 例子：电梯控制系统（自然语言描述 ） 6 例子：UML描述（半形式化） 7 u 一种具有良好语法和语义定义的形式描述方法 u 但无法或很少支持以数学为基础的形式分析和 推理过程 例子：电梯控制系统（程序语言描述 ） 8 例子：电梯控制系统（有限状态机描述） 9 u 一种具有良好语法和语义定义的形式描述方法 u 有效支持以

3、自动机理论为基础的形式化验证过 程 软件的规约表示 软件的规约表示可以采用非形式化的方式来描述，包括自然语言、 图、表等，也可以采用形式化方式来描述。 由于非形式化方法本身所存在的矛盾、二义性、含糊性，以及描述规 约时的不完整性、抽象层次混杂等情况，使得所得到的规约不能准确 地刻画系统模型，甚至会为后来的软件开发埋下出错的隐患。 而对于形式化方法来说，由于其基于严格的数学，具有严格的语法和 语义定义，从而可以准确地描述系统模型，排除了矛盾、二义性、含 糊性等情况，最终得到一个相对完整、正确的系统模型。 10 软件危机 1968年，NATO会议提出了“软件危机”一词 软件危机包含两方面问题 如何

4、开发软件，以满足不断增长、日趋复杂的需求； 如何维护数量不断膨胀的软件产品。 软件危机主要表现如下几个方面 开发成本昂贵 项目进度难控 修改维护困难 质量无法保证 -11- 项目进度难控 为软件开发制定进度是很困难的事情。如有10人月的工作量，则 由一个人完成需要10个月，由10个入完成则需要一个月。但这种 工作量估计方式仅对各部分工作互下干扰的情况下才适用，但作 为整体，尚需讨论合作，这种讨论交流活动就增加了工作量。软 件系统的结构很复杂，各部分附加联系极大。 Brook提出的法则“ 在已拖延的软件项目上增加入力只会使其更难按期完成” 。 1995年，美国共取消810亿美元的软件项目，其中3

5、1%未完取消， 53%的项目延长一半时间，9%按期完成且不超期。1998年，美国 企业应用项目28%的项目取消，40%无限拖长且资金超出预算。 2008年的数据显示，按时、在预算内交付，并且完成了应有功能 的成功项目只有32%。 -12- 软件维护困难 软件的维护任务特别重。 正式投入使用的商用软件，总是存在着一定数量 的错误。随着时间延伸，在不同的运行条件下， 软件就会出故障，就需要修改维护。 软件维护不是更换某种备件，而是要纠正逻辑缺 陷。当软件系统变得庞大，问题变得复杂时，常 常会发生“纠正一个错误带来更多新的错误！” -13- 典型的软件项目开发 14 质量无法保证 Therac-25

6、是加拿大原子能公司AECL和一家法国公司CGR联合开发的一种医 疗设备，它产生的高能光束或电子流能够杀死人体毒瘤而不会伤害毒瘤 附近的人体健康组织。在1985年6月到1987年1月，因为软件缺陷引发了6 起由于电子流或X-光束的过量使用的医疗事故，造成4人死亡、2人重伤的 严重后果。 1996年，欧洲航天局阿丽亚娜5型（Ariane5）火箭在发射后40秒钟后发生 爆炸，2名法国士兵当场死亡，损耗资产达10亿美元之巨，历时9年的航 天计划因此严重受挫。爆炸原因在于惯性导航系统软件技术要求和设计 的错误。 2011年7月23日20时30分05秒，由北京南站开往福州站的D301次列车与杭 州站开往福

7、州南站的D3115次列车发生动车组列车追尾事故，造成40人死 亡、172人受伤，中断行车32小时35分，直接经济损失19371.65万元。根 据初步掌握的情况分析，“723”动车事故是由于温州南站信号设备在设 计上存在严重缺陷，遭雷击发生故障后，导致本应显示为红灯的区间信 号机错误显示为绿灯。 -15- 软件质量的重要方面 16 如何解决软件危机 17 软件工程方法 Software Engineering 软件工程：工程化软件开发过 程控制与管理，追求软件设 计、生产、维护的规范化及科 学化 。 不规范 规范；不严格 严 格；无方法/技术 成熟的方 法/技术。 旨在形成工程化的软件开发的 原

8、理、方法及技术。 软件工程中的生命周期 五个活动 需求分析和规格 软件设计：逻辑模型转换为软件方案，总体结构、模 块算法 代码编写 软件测试：模块测试、组装测试、整体测试 运行维护 -18- 软件工程 vs 形式化方法 n软件工程方法试图指导软件的开发过程。 n然而问题依然存在 n 项目成本、进度依然无法保证 n 软件开发的后续阶段常常发现许多前期设计错误，更正错 误代价高昂 n 发布运行软件时常崩溃，维护代价依然很高 n正如许多软件工程方法所指出的，即使遵循了 很多优秀设计准则和优良编码规范，程序仍可 能包含很多错误，因此，使用一些方法来消除 程序中的人为错误就变得更加重要了。 19 软件开

9、发中为什么使用形式化方法 n 形式化方法的目的是为开发过程提供一些技术和 工具，用于发现并指出软件实现中潜在的缺陷问 题。 n 对软件需求的描述：非形式化的描述很可能导致描述 的不明确和不一致；形式化方法则要求描述的明确性 ，而描述的不一致性也就相对易于发现。 n 对软件设计的描述：软件设计的描述和软件需求的描 述一样重要。 n 对于编程：自动代码生成。 n 对于测试：测试用例的自动生成。 20 软件开发中为什么使用形式化方法 保证质量的需要 为了得到高质量的软件，企业要采用最好的实践， 使他们的软件过程变得成熟起来。形式化方法是一 种前沿技术，研究表明，这种技术非常有助于那些 希望把软件产品

10、的缺陷出现率减到最小的公司。 节约成本的需要 有证据显示，形式方法的使用减少了项目成本。例 如，IBM的大型CICS事务处理项目的独立审核表明 ，9的成本节约要归功于形式方法的使用。对 T800型变换计算机的Inmos浮点单元的独立审核也 证明，形式化方法的使用估计可以减少12个月的测 试时间。 演示 形式化规约和验证工具PAT（Process Analysis Toolkit）演示 哲学家吃饭问题 Sliding Game Shunting Game 22 http:/sav.sutd.edu.sg/PAT/wp-source/resources/pat3_5_1/PAT3.Setup.3.

11、5.1.msi 哲学家吃饭问题 N个哲学家围着桌子坐 ，桌子上有N个筷子 哲学家想吃饭时总是先 拿起右边的筷子再拿起 左边的筷子 哲学家只有得到2个筷 子后才能吃饭 形式化方法 n nFormal methods are Formal methods are mathematically mathematically based based languages, techniques and tools forlanguages, techniques and tools for specifyingspecifying, , designingdesigning andand verifyi

12、ngverifying hardware and hardware and software systemssoftware systems. . n形式化方法是渗透在软件生命期中各个环节（ 需求分析、设计、实现、测试等）的数学方法 或者具有严格数学基础的软件开发方法。 n形式化方法的基本含义是借助数学的方法来研 究计算机科学中的有关问题。 24 形式化方法的主要内容 形式化开发过程的任务分为：模型获取、模型验证、模型 变换 模型获取：从现实世界向模型表示转换，对应软件生命周期中的 需求分析、规格、设计活动； 模型验证：是否满足需求及具有所期望的特性； 模型变换：从模型表示向计算机系统变换的过

13、程。 这些任务对应三方面的活动：形式化规约、形式化验证、 程序求精 25 形式化方法的发展 20世纪60年代：程序正确性证明研究 20世纪80年代：硬件电路设计的形式化方法应用（ 时序逻辑和模型检验的诞生） 20世纪90年代：通信协议和智能控制系统中的形式 化方法应用（工业界应用高速发展） 本世纪：交互式并发软件系统的形式化方法应用 26 经典案例及应用 牛津大学和Hursley实验室于20世纪80年代 合作将Z语言用于IBM商用信息控制系统。 IBM对整个开发进行的测试表明，Z语言的 应用明显地改善了产品质量、大量减少了 错误和早期诊断错误。IBM估计使总体开发 成本降低9。这一成果获皇家技

14、术成就 奖。 经典案例及应用 Praxis公司于1992年交付给英国民航局的信息显示 系统是伦敦机场新空中交通管理系统的一部分。 在该系统的需求分析阶段，形式化描述和非形式 结构化的需求概念相结合；在系统规格阶段，采 用了抽象的VDM模型；在设计阶段，抽象VDM细 化为更为具体的规格。项目开发的生产效率和采 用非形式化技术相当，甚至更好。同时，软件质 量得到了很大的提高，软件的故障率仅为0.75每 千行代码，大大低于采用非形式化技术所提供的 软件的故障率（约为220每千行代码）。 经典案例及应用 加州大学的安全关键系统研究组所开发的 空中交通防碰撞系统的形式化需求规格 TCASII，采用了基于

15、Statecharts的需求状态 机语言RSML，解决了开发过程中遇到的许 多问题。TCASII项目表明了复杂过程控制系 统列写形式化需求规格的可能性以及应用 工程师们不经任何专门培训建立易读且易 评判的形式化规格的可行性。 经典案例及应用 除此之外还有： （1）数据库：用于存储病人监护信息的HP医用仪器实时 数据库系统。 （2）核反应堆系统：核反应器安全系统、核发电系统的 切换装置。 （3）电信系统：AT&T的5ESS电话交换系统、德国电信的 电话业务系统。 （4）保密系统：NATO控制指挥和控制系统中的保密策略 模型、Multinet网关系统的数据安全传输、美国国家标 准和技术院的令牌访问

16、控制系统。 （5）通信协议：协议规格、测试集的生成、协议转换。 （6）运输系统：巴黎地铁的自动火车保护系统、英国铁 路信号控制、以色列机载航空电子软件。 形式化方法讨论 形式化方法中的抽象数学符号及理论确实对软件工程师的 使用带来一些不便，以致于人们要花一定的时间和精力去 学习和掌握。但是，采用形式化方法可以极大地减少了系 统设计开发早期阶段的错误，避免了后期错误修改所带来 的高额成本开销，这样早期人员培训的成本开销会在后期 的系统测试和维护中的高额回报中得到补偿，在某种程度 上还降低了软件开发的成本。同时，采用形式化方法还会 提高系统的设计开发效率，并且形式化方法是高质量、高 可靠软件开发的有效途径，是软件自动化的根本前提。形 式化方法不会完全代替传统的软件开发方法和面向对象方 法，需要根据所解决问题的特点结合或选择使用