软件的形式化理论和方法 主要内容 l软件开发过程和问题 l形式化方法简介 l形式化方法历史 l主要的形式化证明工具 l形式化方法的应用举例 l结论软件开发过程 l一般来说,软件开发的主要步骤大致如下 : 提出问题并进行需求分析; 设计:包括功能和结构设计; 编码和构建; 调试; 发布,维护和升级。 l常用的开发模型:如传统的瀑布模型,较 新近的快速原型、迭代式开发模型等等软件开发的期望 l软件质量稳定,可靠性高 l尽量提高开发的效率 l尽量降低开发的成本 l问题:现在的情况怎么样?软件开发的实际情况 l软件开发的实际情况并不乐观 项目经常延误,预算经常超支 开发的后续阶段常发现许多前期设计错误,更 正的代价高昂 发布运行的软件中常常存在着许多错误,时常 崩溃 软件维护和更新工作的代价很高 l问题:这样的实际情况会造成什么问题?软件缺陷造成的损失软件缺陷造成的损失(2)软件问题的本质 l 极端复杂 规模:成万、成百万、甚至成千万行代码 系统组成部分之间异常复杂的直接与间接相互作用 静态结构与动态性质之间难以把握的复杂关系 l 多变性 异常丰富多彩的应用需求 需求的不断提升和变化 l 要求