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