软件形式化方法ppt课件.ppt

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