《程序设计方法学六.ppt》由会员分享，可在线阅读，更多相关《程序设计方法学六.ppt（71页珍藏版）》请在第壹文秘上搜索。
1、3/30/20231第六章第六章 程序设计的形式化方法程序设计的形式化方法 软件新技术软件新技术 智能化技术智能化技术 扩大软件功能的关键途径扩大软件功能的关键途径 自动化技术自动化技术 提高软件生产率的根本途径提高软件生产率的根本途径 集成化技术集成化技术 助于提高生产率、提高质量助于提高生产率、提高质量 并行化技术并行化技术 提高系统实效的关键技术提高系统实效的关键技术 自然化技术自然化技术 实现社会信息化实现社会信息化3/30/20232重要方向重要方向 攻克的关键教技术攻克的关键教技术网络体系网络体系 传感器网与因特网的高效融合传感器网与因特网的高效融合集成芯片集成芯片 从从Syste
2、m on chip到到Chip on demount虚拟计算虚拟计算 资源聚合的有效性和可靠性验证资源聚合的有效性和可靠性验证软件工程软件工程 基于网络环境的需求工程基于网络环境的需求工程知识处理知识处理 挖掘从消息到知识到决策的元知识挖掘从消息到知识到决策的元知识高效系统高效系统 在高性（效）能计算系统中系列关注在高性（效）能计算系统中系列关注 信息安全信息安全信息教育信息教育3/30/20233跨越源之识规律跨越源之识规律创新根植辨短长创新根植辨短长汪成为院士3/30/20234软件自动化的三个层次软件自动化的三个层次 软件自动化（自动程序设计）软件自动化（自动程序设计）广义：尽可能地借助
3、计算机系统实现软件开发广义：尽可能地借助计算机系统实现软件开发狭义：从形式化的软件功能规范到可执行程序代码狭义：从形式化的软件功能规范到可执行程序代码 这一过程的自动化这一过程的自动化 从软件需求规范从软件需求规范 软件功能、性能规范的转换软件功能、性能规范的转换解决从解决从 “非形式非形式” “形式形式”难度很大，寄希望于受限自然语言方面的突破难度很大，寄希望于受限自然语言方面的突破 从软件功能、性能规范从软件功能、性能规范 软件设计软件设计从从“做什么做什么” “如何做如何做“ 从软件设计规范从软件设计规范 高级语言高级语言 已有相当的进展，出现了许多工具已有相当的进展，出现了许多工具3/
4、30/202351 概述概述一、重要意义一、重要意义 软件发展中的问题：软件发展中的问题： 整体功能不强、缺乏智能、质量欠佳、生产效整体功能不强、缺乏智能、质量欠佳、生产效率低率低 软件自动化是提高软件生产率的根本途径软件自动化是提高软件生产率的根本途径 软件自动化的前提是形式化软件自动化的前提是形式化 因此将形式化的理论和方法用于需求分析与规格因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的前提说明是实现软件自动化的前提3/30/20236二、发展状况二、发展状况 有有30多年历史多年历史Dijkstra、Hoare程序验证程序验证 Scott、Stratchey 程序语义程
5、序语义 形式化方法形式化方法(Formal Method)：通过严格的规范化的数学理论来描述软件系统通过严格的规范化的数学理论来描述软件系统“做做什么什么”的方法。需要形式规范语言的支持。的方法。需要形式规范语言的支持。 形式规范语言：形式规范语言：提供了一个称为语法域的记号系统。一个称为语义提供了一个称为语法域的记号系统。一个称为语义域的目标集合，以及一组精确定义的哪些目标系统域的目标集合，以及一组精确定义的哪些目标系统满足那个规范的规则。满足那个规范的规则。 3/30/20237 因此，形式化方法是在软件系统的开发过程中使用因此，形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型
6、的方法。一种形式系统来表示模型的方法。 形式系统是二元组（形式系统是二元组（L，Cn） L：语言（形式规范语言）：语言（形式规范语言） Cn：对应关系，由推理规则构成：对应关系，由推理规则构成 在软件规范方法方面的代表性成果有：在软件规范方法方面的代表性成果有： 基于异调代数的代数方法基于异调代数的代数方法 特点：用抽象代数中的公理化方法来刻画抽象数特点：用抽象代数中的公理化方法来刻画抽象数据类型中运算的性质，而不涉及数据的具据类型中运算的性质，而不涉及数据的具体表示。体表示。 基本理论：代数语义基本理论：代数语义3/30/20238抽象模型方法抽象模型方法 特点：基于某些已知的特点：基于某些
7、已知的ADT来给出待定义的来给出待定义的 ADT的抽象模型，用抽象模型来刻画待的抽象模型，用抽象模型来刻画待 定义的定义的ADT中运算的功能。中运算的功能。 基本理论：指称语义基本理论：指称语义状态机方法状态机方法 特点：通过状态的转换来刻画输入与输出间的特点：通过状态的转换来刻画输入与输出间的 关系关系 基本理论：操作语义基本理论：操作语义高阶软件方法（高阶软件方法（HOS） 基于控制公理基于控制公理 基本理论：公理语义基本理论：公理语义 3/30/20239 在软件规范语言方面的代表性成果有：在软件规范语言方面的代表性成果有： 一阶谓词演算组成语言一阶谓词演算组成语言 80年代：年代：Z语
8、言、语言、Larch语言、语言、VDM语言语言 90年代：面向实时及分布式的年代：面向实时及分布式的LOTOS语言、语言、 面向对象的面向对象的Z+、Object-Z、VDM+等等三、分类三、分类基于模型的方法基于模型的方法 给出系统（程序）状态和状态变换与操作的显式的给出系统（程序）状态和状态变换与操作的显式的表示但亦是抽象的定义，不涉及并发的行为。表示但亦是抽象的定义，不涉及并发的行为。 如：如：Z、VDM3/30/202310代数方法代数方法 通过联系不同的操作间的行为关系给出操作的隐通过联系不同的操作间的行为关系给出操作的隐式定义，未给出并发的显式表示。式定义，未给出并发的显式表示。
9、如：如：OBJ、Larch过程代数方法过程代数方法 给出并发过程的一个显式模型，并通过过程间允给出并发过程的一个显式模型，并通过过程间允许的可观察的通信上的限制来约束表示行为。许的可观察的通信上的限制来约束表示行为。如：如：CSP（通信顺序进程）和（通信顺序进程）和CCS（通信系统计算）（通信系统计算）基于逻辑的方法基于逻辑的方法 采用逻辑来描述系统的特性，包括程序行为的低采用逻辑来描述系统的特性，包括程序行为的低级规范和系统时间的行为规范。级规范和系统时间的行为规范。 如：时态逻辑、模态逻辑如：时态逻辑、模态逻辑3/30/202311基于网络的方法基于网络的方法 根据网络中的数据流显式地给出
10、系统的并发模根据网络中的数据流显式地给出系统的并发模型，包括数据从一个结点流向另一个结点的条件。型，包括数据从一个结点流向另一个结点的条件。 如：如：Petri网、谓词变换网网、谓词变换网 3/30/202312四、形式化软件开发方法四、形式化软件开发方法采用软件生命周期的变换模型，其实质是将现实世界采用软件生命周期的变换模型，其实质是将现实世界的需求反映成软件的模型化过程。涉及三方面模型：的需求反映成软件的模型化过程。涉及三方面模型：现实世界，模型表示和计算机系统。因此开发的过程现实世界，模型表示和计算机系统。因此开发的过程就是从三方面对系统进行描述和转换的过程。就是从三方面对系统进行描述和
11、转换的过程。开发过程中的任务为：开发过程中的任务为：(1) 模型获取：从现实世界向模型表示的过程，涉及如何模型获取：从现实世界向模型表示的过程，涉及如何提取、表示模型。对应需求分析、设计等活动。提取、表示模型。对应需求分析、设计等活动。(2) 模型验证：对得到的模型表示进行检验，判断是否捕模型验证：对得到的模型表示进行检验，判断是否捕获了所有的需求，该模型是否具有所期望的特性。获了所有的需求，该模型是否具有所期望的特性。(3) 模型变换：是向计算机系统变换的过程，模型变换：是向计算机系统变换的过程， 关键的任关键的任务是一致性检测。对应实现和测试。务是一致性检测。对应实现和测试。3/30/20
12、2313 三项任务分别对应三方面的活动：三项任务分别对应三方面的活动：1. 形式化规范（规格）：形式化规范（规格）：软件规范是指对软件系统对象及用来对系统对软件规范是指对软件系统对象及用来对系统对象进行操作的方法的集合。以及对所开发系统象进行操作的方法的集合。以及对所开发系统中的各对象在生命周期间的集体行为的描述。中的各对象在生命周期间的集体行为的描述。对应与软件生命周期的各个阶段，规范应该理对应与软件生命周期的各个阶段，规范应该理解为是一个多阶段的行为。见例图解为是一个多阶段的行为。见例图规范可以采用非、半形式化的方法来描述，形规范可以采用非、半形式化的方法来描述，形式化规范精确地描述了用户
13、的需求、软件系统式化规范精确地描述了用户的需求、软件系统的功能及各种性质，其描述的是的功能及各种性质，其描述的是“做什么做什么”，而不考虑而不考虑“如何做如何做”。因此，在理解、掌握形。因此，在理解、掌握形式规范语言和方法的基础上对所描述的系统的式规范语言和方法的基础上对所描述的系统的全面、深入的了解，给出恰如其分的描述上至全面、深入的了解，给出恰如其分的描述上至关重要的。关重要的。3/30/202314包含各规格阶段的生命周期模型例包含各规格阶段的生命周期模型例需求分析需求分析BSSRD系统设计系统设计1DS系统设计系统设计2PS软件开发软件开发代码实现代码实现软件测试软件测试运行运行SRD
14、：软件需求文档：软件需求文档BS：行为规范：行为规范DS：设计规范：设计规范PS：程序规范：程序规范3/30/202315软件系统规范的形式化方法软件系统规范的形式化方法从形式化规范到目标软件系统的可实现和可执行从形式化规范到目标软件系统的可实现和可执行角度，可分为三类：角度，可分为三类：(1) 操作类：此类方法基于状态和转移，通过可执行操作类：此类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证。如：有限状态机、模型执行而得到验证。如：有限状态机、Statecharts、Petri网等。网等。(2) 描述类：
15、此类方法基于数学公理和概念，通过逻描述类：此类方法基于数学公理和概念，通过逻辑或代数给出系统状态空间，具有高度抽象的特辑或代数给出系统状态空间，具有高度抽象的特点，便于通过自动工具进行验证。如：基于代数点，便于通过自动工具进行验证。如：基于代数的的Z、VDM、Larch等，基于逻辑的命题线性时态等，基于逻辑的命题线性时态逻辑、一阶线性时态逻辑、计算树逻辑等。逻辑、一阶线性时态逻辑、计算树逻辑等。(3) 双重类：此类方法兼具二者的特点，如：扩展状双重类：此类方法兼具二者的特点，如：扩展状态机态机/实时时态逻辑等。实时时态逻辑等。3/30/202316形式化规范的成功案例形式化规范的成功案例 IB
16、M商用信息系统，牛津大学和商用信息系统，牛津大学和Hursley实验室使用实验室使用Z语言。总体成本降低语言。总体成本降低9，获皇家技术成就奖。，获皇家技术成就奖。 Praxis公司使用公司使用VDM开发的伦敦机场信息显示系统，开发的伦敦机场信息显示系统，软件质量大为提高，故障率软件质量大为提高，故障率0.75(220)每每K行代码。行代码。 其他领域：其他领域： 数据库：数据库：HP医用仪器实时数据库系统医用仪器实时数据库系统 电子仪器：电子仪器：Tektronix系列谐波发生器系列谐波发生器 硬件：硬件：INMOS浮点处理器、浮点处理器、INMOS中中T9000系列系列虚拟信道处理器虚拟信道处理器 运输系统：巴黎地铁自动火车保护系统、以色列运输系统：巴黎地铁自动火车保护系统、以色列机载航空电子软件等等机载航空电子软件等等3/30/2023172. 形式化验证形式化验证软件开发中错误发现的越晚修改的代价越大，软件开发中错误发现的越晚修改的代价越大，与传统方法不同的是形式化方法要求在完成形与传统方法不同的是形式化方法要求在完成形式规范后就进行形式验证。式规范后就进行形式验证。形式验证主
