软件开发的形式化方法概述PPT课件

1 软件开发的形式化方法 刘靖liujing 2012 9 17 2 课程介绍 通过本课程的学习 使同学了解软件开发中形式化方法的基本概念和原理 掌握几种常用的软件系统形式化描述方法 有限状态机 Petri网 时序逻辑等 并应用形式描述 形式验证等形式化分析技术对具有一定规模的软件系统进行形式描述和分析本课程的学习重点是理解形式化方法的基本概念 掌握常用的形式描述和分析技术 并针对典型软件系统进行形式化描述和分析实践 3 课程内容 软件开发的形式化方法概述有限状态机 FSM 方法Petri网方法时序逻辑与形式验证模型检验 ModelChecking 4 课程安排 课程讲授 实例实践 形式描述一种软件系统 并进行系统行为的形式化分析 实践包括三个部分 有限状态机方法实践Petri网方法实践模型检验方法实践 5 课程考核 总成绩 实例实践成绩 90 考勤 10 有限状态机方法实践 30 Petri网方法实践 40 模型检测方法实践 20 6 课程参考教材 参考材料 软件开发的形式化方法 古天龙编 2005 高等教育出版社 软件可靠性方法 DoronA Peled著 王林章等译 2012 机械工业出版社 形式描述技术 叶新铭编 计算机学院自编教材经典教材 学术论文 7 软件开发 软件是什么软件开发现状 软件危机 软件可靠性如何保证软件可靠运行软件工程与形式化方法 8 软件无处不在 9 软件是什么 It sdifferent fromotherengineeringdisciplines inthatwetakeonnoveltaskseverytime Thenumberoftimes civilengineers makemistakesisverysmall Andatfirstyouthink what swrongwithus It sbecauseit slikewe rebuildingthefirstskyscrapereverytime BillGates Microsoft 1992 Ibelievethe spreadsheetproduct I mworkingonnowisfarmorecomplexthana747 jumbojetairliner ChrisPeters Microsoft 1992 10 软件现状 软件系统正迅速多样化和复杂化国家在基础软件研究上的投资不足开发可靠和安全软件的技术不足软件需求远远超过了国家的软件开发能力国家正依赖着脆弱的软件 11 软件开发现状 希望寻求软件可靠运行的保障 12 典型的软件项目开发 13 软件危机的产生根源 开发成本昂贵项目进度难控质量无法保证修改维护困难软件异常复杂 规模 结构 环境等 14 软件修改维护困难 软件的维护任务特别重正式投入使用的商用软件 总是存在着一定数量的错误 随着时间延伸 在不同的运行条件下 软件就会出故障 就需要修改维护软件修改和维护与通常意义下的硬件设备维护是完全不同的 因为软件故障是软件中的逻辑故障所造成的 不是硬件磨损之类的问题软件维护不是更换某种备件 而是要纠正逻辑缺陷 当软件系统变得庞大 问题变得复杂时 常常会发生 纠正一个错误带来更多新的错误 15 软件质量 是反映软件产品满足规定和潜在需要能力的特性的总和 描述和评价软件产品质量的一组属性常称为软件质量特性通常包括以下特性 功能正确 可靠 易用 效率 可维护 可测试等 16 软件质量的重要方面 17 软件的可靠性 指在给定的环境下 特定的时间内 软件无失效运行的概率是软件质量的关键特性可度量 可分析 18 软件为什么会失效 19 软件失效的机理 错误故障失效 避错查错改错容错 X 20 如何保证软件可靠运行 目标 提高软件的可靠性 增强软件质量 软件工程方法SoftwareEngineering 形式化方法FormalMethod 21 SCIENCENaturalSystems ENGINEERINGArtificialSystems PUREAbstractSystems APPLIEDConcreteSystems THEORY EXPERIMENT DESIGN 22 软件工程 工程化软件可靠性指用恰当的进度 可接受的开销开发具有令人满意的可靠性的软件软件工程 工程化的软件开发过程控制与管理 追求软件设计 生产 维护的规范化及科学化不规范 规范 不严格 严格 无方法 技术 成熟的方法 技术旨在形成工程化的软件开发的原理 方法及技术 23 软件可靠性工程 24 形式化方法 Formalmethodsaremathematicallybasedlanguages techniquesandtoolsforspecifying designingandverifyinghardwareandsoftwaresystems形式化方法是渗透在软件生命期中各个环节 需求分析 设计 实现 测试等 的数学方法或者具有严格数学基础的软件开发方法形式化方法的基本含义是借助数学的方法来研究计算机科学中的有关问题 25 软件工程vs形式化方法 正如许多软件工程方法所指出的 即使遵循了很多优秀设计准则和优良编码规范 程序仍可能包含很多错误 因此 使用一些方法来消除程序中的人为错误就变得更加重要了软件工程方法试图指导软件的开发过程形式化方法的目的是为开发过程提供一些辅助性的技术和工具 用于发现并指出软件实现中潜在的缺陷问题 26 形式化方法的主要内容 形式化方法是一系列用于描述和分析系统的符号表示法及相关技术 它们以一些数学理论为基础 如逻辑 自动机和图论等 且都致力于提高软硬件系统的质量针对软件系统的的形式化方法 包括软件系统的形式化规约 specification 和形式化验证 verification 形式化规约 通过具有明确数学定义的文法和语义的方法或语言 对软件的期望特性 软件功能行为进行的精确且简洁的描述例如 时序逻辑 有限自动机 Petri网 进程代数等 27 例子 UML描述 半形式化 一种具有良好语法和语义定义的形式描述方法但无法支持以数学为基础的形式分析过程 28 例子 电梯控制系统 自然语言描述 29 例子 电梯控制系统 程序语言描述 30 例子 电梯控制系统 有限状态机描述 一种具有良好语法和语义定义的形式描述方法有效支持以自动机理论为基础的形式分析过程 31 形式描述 建模 的必要性 WeneedthemodelingbeforeapplyingtoolsandtechniquesforincreasingthereliabilityofasystemRepresentthesystemintermsofmathematicalobjectsthatreflectitobservedpropertiesModelinginvolvesprocessofabstraction simplifyingthedescriptionofthesystem whilepreservingonlyalimitednumberoftheexpectedoriginaldetails Bettermanagethecomplexityofthesystem 32 形式化方法与软件生命周期 形式化的软件开发实际上就是把现实世界的需求反映成软件的模型化过程 故涉及到三方面的系统模型现实世界 体现了软件的功能性能需求模型表示 描述了软件的功能性能行为 指标等计算机系统 运行着真实的软件代码 33 需求 标准需求系统没有死锁没有进程能饿死别的进程进程内的状态断言不能失效应用相关系统不变式 进程断言有效的活性需求合理的终止状态状态间的因果和时序关系公平性假设等等 1功能 2性能 3安全 4时间 34 模型 模型是现实的抽象细节的抽象程度与正确性性质相关通过减少细节获得分析能力 减少无关细节使状态数变少分析的性能就高一些 模型的目的是解释和预言模型是设计辅助模型多层次vs多维化模型精确化而非细节化 35 形式化方法 形式化的软件开发过程就是从这三个方面对软件系统进行描述和转换的过程 主要任务是模型获取 模型验证 模型变换 36 形式化方法的主要内容 模型获取从现实世界向模型表示转换的过程 包括如何提取并表示模型 对应于软件生命周期的需求分析和设计过程模型验证对所得到的模型表示进行检验 判断其是否捕获了所有的用户需求 以及该模型是否具备了所期望的特性 对应于软件生命周期的设计过程模型变换从模型表示向计算机系统变换的过程 一个抽象的模型可以变换到各种计算机系统环境上 关键任务之一是执行一致性测试 判断变换后的计算机系统是否与模型表示一致 对应于软件生命周期的实现和测试过程 形式化规约 Specification 形式化验证 Verification 程序求精 Refinement 37 形式化规约 规约 Specification 一种对系统及其期望特性或者行为的描述 描述的主要内容包括 功能特性 系统的功能行为 结构特性 系统的组成 各组成部分或子系统间的关联 时间特性 时间相关的系统特性 等形式化规约就是通过具有明确数学定义的文法和语义的语言实现以上描述形式规约精确地描述了用户的需求 软件系统的功能行为以及各种性质 描述的是应该 做什么 而不考虑 怎么做 因此 需要注意建立形式规约时 应考虑如何描述得恰如其分 既不过多也不过少 38 形式化规约 软件的规约表示可以采用非形式化的方式来描述 包括自然语言 图 表等 也可以采用形式化方式来描述由于非形式化方法本身所存在的矛盾 二义性 含糊性 以及描述规约时的不完整性 抽象层次混杂等情况 使得所得到的规约不能准确地刻画系统模型 甚至会为后来的软件开发埋下出错的隐患而对于形式化方法来说 由于其基于严格的数学 具有严格的语法和语义定义 从而可以准确地描述系统模型 排除了矛盾 二义性 含糊性等情况 同时 在对系统进行严格地描述的过程中 将会帮助用户明确其原本模糊的需求 并发现用户所陈述的需求中存在的矛盾等情况 从而相对完整 正确地理解用户需求 最终得到一个完整 正确的系统模型 39 形式化规约的分类 操作类方法 基于状态和转移 通过可执行模型来描述系统 模型本身能够采用静态分析和模型执行而得到验证 这类方法包括有限状态机 Statecharts Petri网等描述类方法 基于数学公理和概念 通过逻辑或代数给出系统的状态空间 是高度抽象的 便于通过自动工具进行验证 包括基于代数的Z VDM Larch等方法 和基于时态逻辑的方法双重类方法 兼有前面二者的特点 既能够通过数学公理和概念来高度抽象地描述系统 又具有状态和转移的可执行特征 这类方法包括扩展状态机 实时时态逻辑 ESM RTTL TRIO TROL等 40 形式化验证 定理证明方法 给出关键性质成立的形式证明工具 定理证明器 证明检查器应用条件 系统能用数学理论表达优点 自动化 速度快 可用于部分系统描述 反例缺点 状态爆炸模型检验方法 检验性质在所有状态成立工具 模型检验器应用条件 系统能用有穷行为模型表达优点 可以处理无穷状态系统缺点 难以完全自动化 使用门槛较高 41 程序求精 程序求精 是将自动推理和形式化方法相结合而形成的一门新技术 它研究从抽象的形式规格推演出具体的面向计算机的程序代码的全过程基本思想 用一个抽象程度低 过程性强的程序去代替一个抽象程度高 过程性弱的程序 并保持它们之间功能的一致 这里所说的 程序 是对规约 设计文档以及程序代码的统称在这种理解下 程序可以划分为若干层次 最高层是不能直接执行的程序 即规约 它由抽象的描述语句构成 最低层是可以直接执行的程序 即程序代码 它由可执行的命令语句构成 最高层和最低层之间为一系列混合程序 其中既含有抽象的描述语句 又含有可执行的命令语句 42 形式化方法 43 形式化方法的发展 20世纪60年代 程序正确性证明研究20世纪80年代 硬件电路设计的形式化方法应用 时序逻辑和模型检验的诞生 20世纪90年代 通信协议和智能控制系统中的形式化方法应用 工业界应用高速发展 本世纪 交互式并发软件系统的形式化方法应用 44 形式化方法的发展 尽管当前对大型复杂的系统进行完整的形式化验证还不现实 但把形式化技术应用于大型复杂系统的关键部分确实是一个有效的实用策略软件开发工程师们开始使用更为严格的形式化规约及形式化验证技术 成功地完成了过程控制领域工业规模系统的设计 通信系统中大量的安全可靠通信协议得到了测试和检验形式化技术成功的工业应用引起了人们的普遍关注 可以预计 在未来的工业应用软硬件系统开发中 形式化技术将会发挥越来越重要的作用 45 形式化方法的应用必要性 保证软件质量的需要节约开发成本的需要形式方法和复用广泛的应用领域 46 保证软件质量 为了得到高质量的软件 我们强烈地希望使用软件工程中最好的实践 软件中存在的缺陷至少会引起客户的愤怒 而在更坏的情况下可能会给客户的业务造成较大的破坏或者造成生命损失因此 企业要采用最好的实践 使他们的软件过程变得成熟起来 形式化方法是一种前沿技术 研究表明 这种技术非常有助于那些希望把软件产品的缺陷出现率减到最小的公司 47 节约开发成本 有证据显示 形式化方法的使用可以有效减少软件项目的开发成本例如 IBM的大型CICS事务处理项目的独立审核表明 9 的成本节约要归功于使用形式化方法对T800型变换计算机的Inmos浮点单元的独立审核也证明 形式化方法的使用估计可以减少12个月的测试时间 48 形式方法和复用 软件复用有助于提高软件开发的生产率 其基本思想是开发出可在未来项目中使用的基本部件 这就要求软件部件具有高质量和高可用性 而且部件的实际行为和使用环境也要具备一个文档化的描述形式化方法在软件复用中占有一席之地 因为它可提高部件正确性的置信度 并对某个部件的行为进行明确的形式描述 可以对