软件工程导论2006年8月7日本节从软件形式化描述的基本概念入手 。在理解应用软件形式化技术的意义的 基础之上，重点介绍软件的Z语言规格说 明技术和Petri。 第六讲 软件工程的形式 化方法22006年8月7日第一节 形式化技术概述 什么是形式化方法？从广义上讲，形式化方法是指将离散数学的方法用于解决 软件工程领域的问题，主要包括建立精确的数学模型以及对模 型的分析活动。狭义的讲，形式化方法是运用形式化语言，进行形式化的 规格描述、模型推理和验证的方法。就形式化建模而言，形式化表示必须包含一组定义其语法 语义的形式化规则。这些规则可用于分析给定的表达式是否符 合语法规定，或证明该表达式具有某种性质。32006年8月7日形式化语言的基础一阶命题逻辑：一阶命题逻辑提供以下机制 一组构造表达式的原子公式变量，数值常量，括号 一组逻辑连接符and (), or (), not(.), implies(), logical equality (=)与， 或， 非， 蕴含， 逻辑等价 量词 ：“for all”全称量词 ：“there exists”存在量词42006年8月7日形式化语言的基础一阶命题逻辑中的表达式表达式的取值可以为真或为假(xy yz) xz x+1 y yz) - xz x3 x-6开表达式与闭表达式 如果一个变量是受量词约束的，则称之为限定变量，否则 称之为自由变量 若公式中所有变量均为限定变量，则称该公式为闭表达式 闭表达式的值非真即假52006年8月7日关于形式化方法：悲观者的角度形式化方法是为数学家准备的；形式化方法仅供从事形式化研究的人使用；从事形式化研究的人仅使用形式化方法；62006年8月7日关于形式化方法：悲观者的角度形式化方法的运用将延缓软件开发进度；形式化方法的运用将提高软件开发成本；72006年8月7日关于形式化方法：悲观者的角度形式化方法仅应用于开发安全要求极高的系统；形式化方法仅被用于无关紧要的系统，且缺少工具支持；82006年8月7日关于形式化方法：乐观者的角度运用形式化方法将开发出完美的软件；形式化方法可以替换传统的软件工程方法；92006年8月7日形式化方法在软件工程中的作用102006年8月7日软件的正确性将形式化方法运用于软件工程实践当中的主要目的是保证软件 的正确性。正确性证明的两个标准运行在机器上的程序满足规格说明规格说明在给定的领域性质之下满足需求112006年8月7日软件的完整性完整性证明的两个标准是否已发现所有重要需求是否已发现所有重要领域性质122006年8月7日形式化方法可应用于何处？形式化需求规约 作为程序验证的基准 规约语言Z，VDM，Larch 作为程序行为的模型，与需求相对照 形式化领域知识 以便就以下问题进行推理 .领域知识是否完整；对未来的系统有何影响 形式化有助于直接精确地刻画环境 需求的形式化 以便进行需求模拟 以便测试逻辑一致性 以便测试完整性（依据底层的数学模型）132006年8月7日形式化方法的优点？用数学语言能够解决规格说明的二义性问题，提高其精确性;数学提供了确认手段，使得证明和验证软件程序满足用户和系统 的需求成为可能;针对需求和设计模型进行自动的分析和推理;分析模型性质推导模型逻辑结果模拟/执行模型，有助于可视化及验证;软件的设计过程就是一个形式化的过程;软件设计的最终产物是程序，它可看作是一种可执行的 形式规约，用于解决非形式化的问题。142006年8月7日为什么不采用形式化？形式化方法比其他技术的抽象级别要低容易陷入细节需提早确定系统边界形式化方法通常限于正确一致的模型但绝大多数情况下，模型都并非绝对正确、一致、完整不知使用哪个工具合适要描述的是程序行为还是需求？形式化方法的鼓吹者常常过于依赖某一种工具常常对研究原型的规模有着过高的期盼152006年8月7日为什么不采用形式化？形式化方法需要作出更大的努力延缓项目进展需要更多的数学训练回报也并非立竿见影许多项目均不适合运用形式化方法162006年8月7日三类不同的模型？172006年8月7日模型类型自然语言 很强的表达能力及适应性 不易于表示模型的语义 适于需求获取及为模型加标注，便于通信 半形式化的表示 便于表示结构及语义 可推理、一致性检查、模拟等（如图、表、结构化英语等） 通常是可视化的，以便在多个干系人间通信 形式化表示 具有精确的语义定义，可能进行广泛的推理 距离应用领域较远182006年8月7日形式验证一致性分析与类型检查 该形式模型的表示是否规范？ 验证 针对小型示例的模型模拟 形式化挑战 针对给定情况的提问 状态爆炸 检查应用程序性质 证明设计的逐级求精是正确的 设计是否满足需求？192006年8月7日第二节 现有形式化方法概述 所谓形式化规格说明语言的关键思想是把软件开发 过程中的需求规格说明阶段和软件设计说明阶段分 开,在需求规格说明阶段精确地描述软件“做什么”， 而不涉及“怎么做”。编写规格说明与编写计算机程 序的不同之处在于规格说明是对目标软件系统的功 能描述，而计算机系统则是实现目标软件系统功能 的过程描述。202006年8月7日各种形式化方法的区别本体不同 固定本体：状态，事件，动作状态图，状态机 可扩充本体：定义新概念的元语言 数学基础不同 基于逻辑的方法：一阶谓词逻辑，时序命题逻辑 基于代数的方法：代数语言，集合语言 基于图的方法：状态图、Petri 网等 对时间的处理不同 状态/事件模型：将时间表示为事件序列；将时间表示为 量化的区间 将时间作为一级类对象来处理212006年8月7日形式规约语言源自程序证明技术 派生出许多通用的规约语言 适合描述程序单元的行为 核心技术：类型检查，定理证明 在需求工程中的适用性较差 无抽象及结构化机制 与程序语义密切相关 举例：Larch, Z, VDM222006年8月7日并发/反应式系统建模旨在表达程序行为的动态性重点研究并发与反应式系统（如实时、嵌入式系统）支持对安全性、活性与性能的推理提供一种精确的规格描述语言核心技术：一致性检查，模型检测在需求工程中的适用性较差建模语言专为需求工程设计举例：Statecharts, RSML, Parnas-tables, SCR, 232006年8月7日形式化的概念模型关注需求工程知识的表达 重点对领域实体、行为、主体，断言进行建模 提供领域模型的形式化本体 一阶谓词逻辑是形式化基础 核心技术：推理机，默认的知识库系统命令 解释器 需求工程中的适用性较好 -建模模式能够表达核心需求模式 举例：Reqtsapprentice, RML, Telos, Albert II, 242006年8月7日形式化方法的正确运用有选择地使用形式化方法 轻量级的形式化方法 目前最为流行的技术转化方式 两种方法 形式化方法的轻量级应用：对部分模型有选择的运用形 式化方法 轻量级的形式化方法：允许未加评估的谓词的新方法252006年8月7日第三节 建模语言介绍重点介绍Z 语言和Petri 网262006年8月7日基于集合论及一阶谓词逻辑 强类型语言；声明性语言 使用称为“模式”的图形结构 一种抽象层次较低的结构化机制 一种可用的规约构造模块 容易理解Z 语言272006年8月7日Z 语言模式表示282006年8月7日Z 语言模式表示292006年8月7日Z 语言规约描述过程 逐一描述系统组成成分 各规约片断组合在一起形成完整的规约描述302006年8月7日Z 语言实例：停车场管理系统基本数据类型定义 “停车提示”是一个基本数据类型的名字 “停好”和“停车场满”是该类型的数据可能的取值 停车提示= 停好| 停车场满全局变量声明 在Z 语言中，N 和Z 属于基本数据集合，分别表 示正整数集合和整数集合。停车场容量: Z/*变量声明*/ 停车场容量0/*变量约束*/312006年8月7日Z 语言实例：停车场管理系统状态定义 每个系统有唯一的状态定义，可以为状态命名。本例 中为系统状态命名为“停车场状态”。状态定义中首先声明一或 多个表示系统状态的变量，这里的变量名为“停车数量”，类型 为整数。该变量的约束条件为取值大于等于0，小于等于最大 停车数量。 停车场状态 停车数量: Z/*状态变量声明*/ 停车数量0 停车数量停车场容量322006年8月7日Z 语言实例：停车场管理系统初始化定义系统状态变量的初始值。系统的初始化定义是唯 一的。停车场初始化停车数量= 0332006年8月7日Z 语言实例：停车场管理系统操作定义 每个系统可以定义若干个操作。 Z 语言中操作的定义是基于状态的，而不是基于过程的。 该操作如何改变了系统的状态变量的值？ 该操作有哪些输入变量？ 有哪些输出变量？ 当一个操作改变了某个系统状态变量x时，在操作定义的第一 行写出状态变化声明x。 当一个操作未改变任何系统状态变量时，即可以在操作定义 第一行写出以下状态声明状态变量（可省略）。342006年8月7日操作定义（续）Z 语言实例：停车场管理系统352006年8月7日操作定义也可以采用以下形式：Z 语言实例：停车场管理系统表示：操作“进入停车场”分为“正常停车”和“停车场满”两 种可能情况，具体执行时选择哪种情况，由环境满 足哪种操作的约束条件来决定。362006年8月7日Z 语言总结Z 语言系统规约定义一组状态模式以及影响这组状态的操作模 式.优点 有良好的数学基础 结构清晰简单.缺点 所有的状态变量是全局的，就一个操作模式进行推理时，要 同时考虑可能受到影响的其它所有操作模式。当系统超过一 定规模时，这项工作将变得异常困难。372006年8月7日Petri 网1962 年，联邦德国的Carl Adam Petri在他的博士论文 “KommunikationmitAutomaten”用自动机通信中首 次使用网状结构模拟通信系统。 该系统模型后来以Petri 网为名流传。现在，Petri 网一 词既指这种模型，又指以这种模型为基础发展起来的理论 ，有时又把Petri 网称为网论（net theory）。 Petri 网分为两类 位置/迁移Petri 网 高级网：谓词迁移Petri 网、有色Petri 网、计时 Petri 网382006年8月7日.Petri 网结构定义392006年8月7日Petri 网结构402006年8月7日Petri 网概念变迁是Petri 网中的主动元素 通过点火变迁，过程从一个状态转变到另一个状态，因此 变迁经常表示事件、操作、转换或传输。 库所是Petri 网中的被动元素 不能改变网的状态，通常表示媒介、缓冲器、地理位置、 （子）状态、阶段或条件。 令牌通常表示对象 这些对象可能是具体的事物，也可能是抽象的信息。 点火 变迁t1（记录）从输入库所p1（申报）中获取令牌，然后 释放到库所p3（审核）中，我们把这一行为称为对变迁的点火（ firing） 前面Petri 网示例 每个令牌都表示一个保险索赔案例。412006年8月7日Petri 网概念就绪 Petri 网的状态用库所中令牌的分布来描述，可以使 用（1, 0, 0）描述当前状态。即p1（申报）中有一个 令牌，而p2（审核）和p3（就绪）中一个都没有。 变迁只有满足可点火条件时才能点火，即每个输入库 所中均至少有一个令牌，变迁才具有发生权，点火就 绪。 如图，p1（申报）是就绪（enabled）的，其他两个 都不是。422006年8月7日就绪演示 432006年8月7日Petri 网具有丰富的结构描述能力，例如：可以描述顺 序、并发、冲突、混合结构下的Petri