1、 软件工程导论（第5版）普通高校本科计算机专业特色教材精选张海藩 编著1第第4章章 形式化说明技术形式化说明技术主要内容4.1 形式化说明技术4.2 有穷状态机4.3 Petri网4.4 Z语言教学重点有穷状态机、Petri网。24.1形式化说明技术概述形式化说明技术概述形式化方法的引入在传统的软件开发过程中，人们普遍采用各种非非形式化形式化的图形工具和文字符号工具，并按照一定的设计原则和有序步骤，同时手工或辅助编写有关设计文档。软件工程的实践表明，用户需求规格说明的质量对于后续的软件开发过程是非常重要的。u系统分析人员依据用户需求，为目标软件系统创建了需求规格说明。u设计和编程人员根据这个需
2、求规格说明进行系统结构和模块设计及编码。u软件测试及验收人员则根据这个需求规格说明验证目标系统。34.1 续续形式化方法的引入20世纪80年代中期以来，一种专用于需求规格说用于需求规格说明明的形式规格说明语言应运而生。形式规格说明语言克服了自然语言和程序设计语言的不足，应用形式化、规范化的数学理论，严格定义软件系统“做什么”的形式语义模型，并支持自动程序转换系统将需求规格说明的语义模型转换为可执行代码。由此产生的软件形式开发方法正日益受到各国软件界的重视。44.1 续续软件需求规格说明方法分类非形式化方法u用自然语言进行描述的方式。半形式化方法u用数据流图、实体-联系图、状态转换图、IPO图等
3、建立模型的方法。形式化方法u利用形式化、规范化的数学推演的方式。54.1 续续非形式化方法的缺点矛盾u一组相互冲突的陈述。二义性u读者可以用不同方式理解的陈述。含糊性u没有给出任何有用信息的笼统的陈述。不完整性u信息的描述过程中遗留了某个方面。抽象层次混乱u在非常抽象的陈述中混进了一些关于细节的低层陈述。64.1 续续形式化方法的主要思想形式化需求分析方法的主要思想，是利用形式化规格说明语言严格地定义用户需求，并采用数学推演的方法证明需求定义的性质。从某种意义上讲，形式化方法是克服需求分析阶段中主要困难（不精确性、不一致性和不完全性）的有效途径。形式化规格说明语言包括：严格的语法定义、严格的语
4、义定义以及一系列的数学推演规则。74.1 续续形式化方法的主要思想规格说明语言的语法语法一般基于集合论、数理逻辑或代数学。规格说明语言的语义语义是其所有语法符号的意义的数学描述。形式化规格说明语言的推演规则规则一般与其数学基础和语义定义方法密切相关。规则必须在规格说明语言的语义系统中可证。因此，可以认为规则是派生的语义定义，它们可以直接应用于软件规格说明的性质证明并简化推演过程。84.1 续续形式化方法的分类形式化方法是应用严格的形式符号和数学方法定义或描述目标软件系统需求规格说明的一种方法。根据对需求规格说明的定义方式分类：面向模型的形式方法。u又称基于状态描述的形式方法。u基本思想：利用域
5、、元组、集合、序列、映射、包等这些已知特性的数学抽象概念来为目标软件系统的状态特征和行为特征构造形式语义模型。语义模型就作为目标软件系统需求规格的形式说明。u主要代表：VDM方法（维也纳开发方法）、Z语言方法等。代数构造形式方法。u目标软件系统的需求规格说明提供一些特殊的构造机制，并以代数构造方式描述目标系统的结构、功能。94.1 续续软件形式开发方法将形式化方法应用于软件开发过程称为软件形式软件形式开发方法开发方法。首先，在需求分析阶段的信息收集和信息分析两项工作中，采用形式化的规格说明语言构造目标软件系统严格的形式需求规格说明即形式语义。然后，以该形式需求规格说明为起点，借助相应的形式开发
6、支持工具辅助实现目标软件系统。目前，除了在软件设计、编码阶段采用形式方法外，还在开展软件系统形式化测试的研究工作。104.1 续续形式化方法的优点对系统的需求规格说明描述精确、定义完整。形式化的需求规格说明有利于系统的设计与实现。软件实现的正确性可以形式验证，确保软件质量。114.1 续续形式化方法的缺点形式化的需求规格说明可读性差。对软件设计人员要求较高，需进行更专业化的培训。只适用于能静态定义的软件系统，它无法定义动态系统行为。形式化的规格说明（形式语义模型）的正确性验证费时费力，目前还不能简化或自动化。形式方法目前还缺乏软件工程环境的支持。124.1 续续应用形式化方法的准则应该选用适合
7、当前项目的形式化说明技术。应该形式化，但不要过分形式化。应该估算成本。应该有形式化方法顾问随时提供咨询。不应该放弃传统的开发方法。应该建立详尽的文档。不应该放弃质量标准。不应该盲目依赖形式化方法。应该进行严格的审查、验证。应该重用。134.1 续续形式化方法近年来的发展形式化方法与图形语言机制相结合。为图形语言机制赋予形式化的语法和语义，从而兼具了图形表示的直观、简洁，以及形式化方法的严谨、精确等优点。用CASE工具支持形式化软件开发。CASE工具不仅可以简化需求分析和需求描述工作，而且还可以利用自动定理证明技术帮助分析人员验证软件规格说明的数学性质。实践证明，这两条技术途径对于克服形式化方法
8、的主要缺陷是行之有效的。因此，它们仍将在形式化方法的未来发展中发挥重要作用。144.2 有穷状态机有穷状态机定义一个有穷状态机可以表示为一个5元组(J，K，T，S，F)，其中：J是一个有穷的非空状态集；K是一个有穷的非空输入集；T是一个从(J-F)K到J的转换函数；SJ，是一个初始状态；FJ，是终态集。154.2 续续例1一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。164.2 续续例1保险箱的状态
9、转换情况174.2 续续例1保险箱的状态转换表4.1184.2 续续例1保险箱例子的有穷状态机描述状态集J：保险箱锁定，A，B，保险箱解锁，报警。输入集K：1L，1R，2L，2R，3L，3R。转换函数T：如表4.1所示。初始态S：保险箱锁定。终态集F：保险箱解锁，报警。194.2 续续扩展定义一个有穷状态机可以表示为一个5元组(J，K，T，S，F)，其中：J是一个有穷的非空状态集；K是一个有穷的非空输入集；P是一个谓词集；T是一个从(J-F)KP到J的转换函数；SJ，是一个初始状态；FJ，是终态集。204.2 续续例2一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他
10、状态的一个事件。转换规则：当前状态菜单+事件所选择的项下个状态。当前状态菜单+事件所选择的项+谓词下个状态。214.2 续续例3：电梯系统自然语言描述 在一幢m层的大厦中需要一套控制n部电梯的产品，要求这n部电梯按照约束条件C1，C2和C3在楼层间移动。C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。C3：当对电梯没有请求时，它关门并停在当前楼
11、层。224.2 续续例3：电梯系统电梯按钮的状态转换图转换函数：EB（e，f）：按下电梯e内的按钮并请求去f层。状态EBON(e,f)：电梯按钮(e,f)打开EBOFF(e,f)：电梯按钮(e,f)关闭234.2 续续例3：电梯系统事件EBP（e，f）：电梯按钮（e，f）被按下。EAF（e，f）：电梯e到达f层。谓词V（e，f）：电梯e停在f层。状态转换规则的形式化描述如下：EBOFF(e,f)+EBP(e,f)+not V(e,f)EBON(e,f)EBON(e,f)+EAF(e,f)EBOFF(e,f)V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f)244.2 续
12、续例3：电梯系统楼层按钮的状态转换图转换函数：FB（d，f）：f层请求电梯向d方向运动的按钮。状态FBON(d,f)：楼层按钮(d,f)打开FBOFF(d,f)：楼层按钮(d,f)关闭254.2 续续例3：电梯系统事件FBP（d，f）：楼层按钮（d，f）被按下EAF（1n，f）：电梯1或或n到达f层 谓词S（d，e，f）：电梯e停在f层并且移动方向由d确定为向上(d=U)或向下(d=D)或待定(d=N)。状态转换规则的形式化描述如下：FBOFF(d,f)+FBP(d,f)+not S(d,1n,f)FBON(d,f)FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f)
13、其中，d=UorD。264.2 续续例3：电梯系统电梯的3个状态：M(d,e,f)：电梯e正沿d方向移动，即将到达的是第f层S(d,e,f)：电梯e停在f层，将朝d方向移动(尚未关门)W(e,f)：电梯e在f层等待(已关门)274.2 续续例3：电梯系统电梯3个事件：DC(e,f)：电梯e在楼层f关上门ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下RL：电梯按钮或楼层按钮被按下进入打开状态，登录需求284.2 续续例3：电梯系统电梯的状态转换规则（仅发生在关门之时）：S(U,e,f)+DC(e,f)M(U,e,f+1)S(D,e,f)+DC(e,f)M(D,e
14、,f-1)S(N,e,f)+DC(e,f)W(e,f)294.2 续续例3：电梯系统电梯的状态转换图状态事件规则304.2 续续评价格式：当前状态+事件+谓词下个状态CASE工具把一个有穷状态机描述的规格说明直接转变为源代码。314.3 Petri网网Petri网Petri网的思想是1962年由Carl Adam Petri提出来的。最初是一种表达异步系统的控制规则的图形表示法，现在广泛应用于硬件与软件系统的开发中。Petri网适用于描述与分析相互独立、协同操作的处理系统，即并发执行的处理系统。324.3 续续Petri网基本概念 Petri网简称PNG（Petri Net Graph），是一
15、种有向图，包含四种元素。位置P：符号为“”，它用来表示系统的状态。转换T：用短竖线表示，代表系统中的事件。输入函数I：用由位置指向转换的箭头表示。输出函数O：用由转换指向位置的箭头表示。334.3 续续Petri网的组成344.3 续续Petri网的组成位置P：P1，P2，P3，P4转换T：t1，t2输入函数：I(t1)=P2，P4 I(t2)=P2输出函数：O(t1)=P1 O(t2)=P3，P3354.3 续续Petri网形式化定义Petri网是一个四元组C=（P，T，I，O），其中，P=P1，Pn是一个有穷位置集，n0。T=t1，tm是一个有穷转换集，m0，且T和P不相交。I：TP为输入
16、函数，是由转换到位置无序单位组(bags)的映射。O：TP为输出函数，是由转换到位置无序单位组的映射。364.3 续续带标记的Petri网Petri网的标记是在Petri网中权标的分配。标记：表明系统当前处于什么状态的标志。通常，当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。Petri网中权标总数不固定。Petri网具有非确定性。374.3 续续带标记的Petri网标记：(1，2，0，1)384.3 续续带标记的Petri网t1被激发。标记：(2，1，0，0)394.3 续续带标记的Petri网t1，t2 被激发。标记：(2，0，2，0)404.3 续续状态迁移当激发
17、产生的结果有几个时，将随机地选择一个结果输出，并把作为结果的位置的状态加上权标。权标在PNG中的游动，称为“状态的迁移”。414.3 续续Petri网形式化定义带有标记的Petri网成为一个五元组(P，T，I，O，M)。Petri网C=(P，T，I，O)中的标记M，是由一组位置P到一组非负整数的映射：M：P0，1，2，424.3 续续含禁止线的Petri网禁止线：用一个小圆圈而不是用箭头标记的输入线。通常，当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许的。434.3 续续例1：电梯系统自然语言描述 在一幢m层的大厦中需要一套控制n部电梯的产品，要求这n部电梯按照约束
18、条件C1，C2和C3在楼层间移动。C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。C3：当对电梯没有请求时，它关门并停在当前楼层。444.3 续续例1：电梯系统电梯按钮454.3 续续例1：电梯系统楼层按钮464.3 续续例2：环形铁路有一个环形铁路，在A站与B站之间是单轨，在某一个时刻只能走一列火车，但A站与B站都是双向运行的。上行和下行列车
19、交替行驶。474.3 续续例2：环形铁路484.3 续续例3：进程同步机制设在一个多任务系统中有两个进程PR1 和PR2，它们是用了一个公共资源R。该资源在系统运行的某一个时刻只能为一个进程所占有。为了解决两个进程在运行中可能会同时申请资源的矛盾，要用原语LOCK（对资源加锁）和UNLOCK（对资源解锁）控制R的使用，保证进程间的同步。494.3 续续例3：进程同步机制504.4 Z语言语言Z语言用Z语言描述的、最简单的形式化规格说明含有下述4个部分：给定的集合、数据类型及常数。状态定义。初始状态。操作。使用Z语言需要具备集合论、函数、数理逻辑等方面的知识。514.4 续续给定的集合一个Z规格
20、说明从一系列给定的初始化集合开始。初始化集合：不需要详细定义的集合。电梯系统：给定的初始化集合称为Button；Z规格说明开始于：Button524.4 续续状态定义一个Z规格说明由若干个“格”组成；每个格含有一组变量说明和一系列限定变量取值范围的谓词。Z格-S的格式534.4 续续状态定义电梯系统Button集合有4个子集：floor_buttons：楼层按钮的集合。elevator_buttons：电梯按钮的集合。buttons：电梯问题中所有按钮的集合。pushed：所有处于打开状态的按钮的集合。约束条件：floor_buttons集与elevator_buttons集不相交 floor
21、_buttons集与elevator_buttons集共同组成buttons集。544.4 续续状态定义电梯系统P：给定集的所有子集，即幂集554.4 续续初始状态抽象的初始状态是指系统第一次开启时的状态。电梯系统：Button_InitButton_Statepushed=564.4 续续操作电梯系统代表一个格被用在另一个格中？代表输入变量！代表输出变量574.4 续续操作电梯系统代表一个格被用在另一个格中？代表输入变量！代表输出变量 代表集合差运算584.4 续续评论Z语言优点容易发现用z写的规格说明中的错误。对于精确度的要求减少了模糊性、不一致性和遗漏的几率。在需要时可严格地验证规格说明的正确性。学习编写Z规格说明不难。可降低软件开发费用。Z规格说明转换为自然语言规格说明，更容易保证正确性和清晰性。59
