第4章-形式化说明技术课件.ppt

1、第第4章章 形式化说明技术形式化说明技术前言前言4.1 概述概述4.2 有穷状态机有穷状态机4.3 Petri网网4.4 Z语言语言4.5 小结小结 形式化说明技术形式化说明技术=形式化方法形式化方法，概念等同。，概念等同。软件生命周期软件生命周期包括哪几个阶段？包括哪几个阶段？可行性研究需求分析总体设计详细设计编码和单元测试软件维护需求需求规格说明书总体设计总体设计规格说明书详细设计详细设计规格说明书系统系统规格说明书描述“系统系统规格说明书”的方法，有哪些？综合测试描述描述“系统系统规格说明书规格说明书”的的3种方法种方法按照按照形式化的程度形式化的程度非形式化方法非形式化方法形式化方法形

2、式化方法半形式化方法半形式化方法例如：自然语言，是例如：自然语言，是典型的典型的非形非形式化方法式化方法例如：数据流图例如：数据流图(ch2)、实体、实体-联系联系图图(ch3)，是，是典型的典型的半形式化方法半形式化方法例如：例如：有穷状态机有穷状态机、 Petri网网、 Z语语言言，是，是典型的典型的形式化方法形式化方法给出定义给出定义非形式化方法非形式化方法形式化方法形式化方法半形式化方法半形式化方法形式化方法课本定义形式化方法课本定义非数学方法半数学方法数学方法二义性 准确性 给出给出3种方法种方法的通俗定义的通俗定义用非数学方法描述系统规格说明书的方法用数学方法描述系统规格说明书的方

3、法用半数学方法描述系统规格说明书的方法形式化方法形式化方法课本的定义课本的定义所谓所谓形式化方法形式化方法，是描述系统性质的基于数学的技，是描述系统性质的基于数学的技术术（如：集合论、函数、数理逻辑）（如：集合论、函数、数理逻辑），也就是说，如果一种方法，也就是说，如果一种方法有有坚实的数学基础坚实的数学基础，那么它就是，那么它就是形式化形式化的。的。实质上与上面的通俗定义是一样的。实质上与上面的通俗定义是一样的。第第4章章 形式化说明技术形式化说明技术前言前言4.1 概述概述4.2 有穷状态机有穷状态机4.3 Petri网网4.4 Z语言语言4.5 小结小结用用自然语言自然语言（典型的非形式

4、化方法）（典型的非形式化方法）书写的书写的系统规系统规格说明书格说明书，可能存在，可能存在矛盾矛盾、二义性二义性、含糊性含糊性、不完不完整性整性及及抽象层次混乱抽象层次混乱等问题。等问题。4.1 概述概述 4.1.1 非形式化方法的缺点非形式化方法的缺点矛盾矛盾是指一组相互冲突的陈述。是指一组相互冲突的陈述。矛盾矛盾是指一组相互冲突的陈述。是指一组相互冲突的陈述。（不同系统分析员定义范围不同）（不同系统分析员定义范围不同）二义性二义性是指读者可以用不同方式理解的陈述。是指读者可以用不同方式理解的陈述。含糊性含糊性，例如：这样的需求：，例如：这样的需求：“系统界面应该是对系统界面应该是对用户友好

5、的。用户友好的。”实际上，这样笼统的陈述并没有给实际上，这样笼统的陈述并没有给出任何有用的信息。出任何有用的信息。不完整性不完整性可能是在系统规格说明中最常遇到的问题可能是在系统规格说明中最常遇到的问题之一。之一。（如规格中没有考虑登录失败的转向的页面，即考虑问题不全面）（如规格中没有考虑登录失败的转向的页面，即考虑问题不全面）抽象层次混乱抽象层次混乱是指在非常抽象的陈述中混进了一些是指在非常抽象的陈述中混进了一些关于细节的低层次陈述。关于细节的低层次陈述。（总体设计中混入了详细设计，分不清他们）（总体设计中混入了详细设计，分不清他们）4.1.2 形式化方法的优点形式化方法的优点人在理解用人在

6、理解用自然语言自然语言描述的描述的系统规格说明系统规格说明时，容易时，容易产生产生二义性二义性。为了。为了克服非形式化方法的缺点克服非形式化方法的缺点，人们，人们把把数学数学引入软件开发过程，创造了引入软件开发过程，创造了基于数学的基于数学的形式形式化方法化方法。运用运用形式化方法形式化方法描述描述系统规格说明系统规格说明具有如下具有如下优点优点：（1）因数学的因数学的严谨性严谨性和和准确性准确性可克服可克服二义性，二义性，能能够够简洁准确地描述简洁准确地描述系统规格说明；系统规格说明；（2）可以在不可以在不同的软件生命周期的各阶段之间同的软件生命周期的各阶段之间平滑地过渡（平滑地过渡（3）提

7、供了提供了高层确认手段高层确认手段，如可以证明设计是否符合规，如可以证明设计是否符合规格说明。格说明。4.1.2 形式化方法的优点形式化方法的优点4.1.3 应用形式化方法的准则应用形式化方法的准则人们对形式化方法的人们对形式化方法的看法并不一致看法并不一致。形式化方法对。形式化方法对某些软件工程某些软件工程师很有吸引力，其拥护者甚至师很有吸引力，其拥护者甚至宣称宣称这这种方法可以引发软件开发方法的革命；种方法可以引发软件开发方法的革命；另一些人另一些人则则对把数学引入软件开发过程对把数学引入软件开发过程持怀疑甚至反对的态度持怀疑甚至反对的态度。编者认为编者认为，对形式化方法也，对形式化方法也

8、应该应该“一分为二一分为二”，既，既不要过分不要过分夸大它的优点夸大它的优点也也不要一概排斥不要一概排斥。为了为了更好更好地地发挥发挥这种方法的这种方法的长处长处，下面，下面给出给出应用形式化方法应用形式化方法的几条的几条准则准则，供读者在，供读者在实际实际工作中工作中使用使用。4.1.3 应用形式化方法的准则应用形式化方法的准则(1) 应该选用适当的表示方法。应该选用适当的表示方法。（系统性质不同，（系统性质不同，FSM、Petri网）网）(2) 应该形式化，但不要过分形式化。应该形式化，但不要过分形式化。（关键（关键 界面）界面）(3) 应该估算成本。应该估算成本。（培训）（培训）(4)

9、应该有形式化方法顾问随时提供咨询。应该有形式化方法顾问随时提供咨询。 (开发人员不开发人员不熟悉形式化方法中使用的数学和逻辑，且没有受过专业的训练熟悉形式化方法中使用的数学和逻辑，且没有受过专业的训练) (5) 不应该放弃传统的开发方法。不应该放弃传统的开发方法。（集成（集成 取长补短）取长补短）(6) 应该建立详尽的文档。应该建立详尽的文档。（帮助开发人员和客户理解系统）（帮助开发人员和客户理解系统）(7) 不应该放弃质量标准。不应该放弃质量标准。 (应用形式化方法有助于开发出高质量的软应用形式化方法有助于开发出高质量的软件，但不能保证软件的正确性，即描述不符客户需求，无法验证正确性件，但不

10、能保证软件的正确性，即描述不符客户需求，无法验证正确性)(8) 不应该盲目依赖形式化方法。不应该盲目依赖形式化方法。（无法验证需求是否满足客户要求）（无法验证需求是否满足客户要求）(9) 应该测试、测试再测试。应该测试、测试再测试。 （同上）（同上） (10) 应该重用。应该重用。（降低成本（降低成本 提高质量提高质量 提高开发速度）提高开发速度）4.2 有穷状态机有穷状态机4.1.3 应用形式化方法的准则应用形式化方法的准则第第4章章 形式化说明技术形式化说明技术前言前言4.1 概述概述4.2 有穷状态机有穷状态机4.3 Petri网网4.4 Z语言语言4.5 小结小结下面通过一个简单下面通

11、过一个简单例子例子介绍介绍有穷状态机有穷状态机的的基本概念基本概念。一个一个保险箱保险箱上装了一个上装了一个复合锁复合锁，锁有，锁有三个位置三个位置，分，分别标记为别标记为1、2、3，转盘转盘可向左可向左(L)或向右或向右(R)转动。转动。这样，在这样，在任意时刻任意时刻转盘都有转盘都有6种种可能的可能的运动运动，即，即1L、1R、2L、2R、3L和和3R。保险箱的。保险箱的组合密码组合密码是是1L、3R、2L，转盘的任何其他运动都将引起，转盘的任何其他运动都将引起报警报警。图图4.1描绘了保险箱的描绘了保险箱的状态转换状态转换情况。情况。4.2 有穷状态机有穷状态机（4.2.1 FSM、4.

12、2.2 EFSM） 4.2.1 概念概念图图4.1 保险箱的状态转换图保险箱的状态转换图状态状态事件事件/输入输入图图4.1是一个是一个有穷状态机有穷状态机的的状态转换图状态转换图。状态转换。状态转换并不一定要用并不一定要用图形方式图形方式描述，表描述，表4.1的的表格形式表格形式也也可以表达同样的信息。可以表达同样的信息。转换函数：当前状态转换函数：当前状态+事件事件/输入输入 下个状态下个状态从上面这个简单例子可以看出，一个从上面这个简单例子可以看出，一个有穷状态机有穷状态机包包括下述括下述5个部分个部分：状态集状态集J、输入集输入集K、由当前状态由当前状态和当前输入确定下一个状态和当前输

13、入确定下一个状态(次态次态)的转换函数的转换函数T、初始态初始态S和和终态集终态集F。对于。对于保险箱保险箱的例子，相应的的例子，相应的有穷状态机的各部分如下。有穷状态机的各部分如下。状态集状态集J：保险箱锁定，：保险箱锁定，A，B，保险箱解锁，报，保险箱解锁，报警。警。输入集输入集K：1L，1R，2L，2R，3L，3R。转换函数转换函数T：如表：如表4.1所示。所示。（当前状态（当前状态+事件事件/输入输入 下个状态）下个状态）初始态初始态S：保险箱锁定。：保险箱锁定。终态集终态集F：保险箱解锁，报警。：保险箱解锁，报警。如果使用如果使用更形式化的术语更形式化的术语，一个，一个有穷状态机有穷

14、状态机可以表可以表示为一个示为一个5元组元组(J，K，T，S，F)，其中：，其中：J是一个有穷的是一个有穷的非空状态集非空状态集；K是一个有穷的是一个有穷的非空输入集非空输入集；T是一个从是一个从(J-F)K到到J的的转换函数转换函数；SJ，是一个，是一个初始状态初始状态；F J，是，是终态集终态集。 有穷状态机有穷状态机应用得非常应用得非常广泛广泛。该方法主要用于在。该方法主要用于在系系统规格说明书统规格说明书中中描述系统的状态转换描述系统的状态转换。例如例如：上面：上面所讲的保险箱的例子，所讲的保险箱的例子，即即用用FSM描述了保险箱系统描述了保险箱系统的状态转换。的状态转换。但是但是，对

15、于一些复杂的系统，对于一些复杂的系统，FSM难以描述清楚难以描述清楚系系统规格说明书统规格说明书中的中的状态转换状态转换。例：例：当前状态：当前状态：某登录页面某登录页面+事件：事件：点登录按钮点登录按钮 下一状态：下一状态：登录后的主页登录后的主页 为了为了满足满足复杂系统的规格说明复杂系统的规格说明中的中的状态转换的描述状态转换的描述，需要对需要对有穷状态机有穷状态机做一个很有用的做一个很有用的扩展扩展，即在前述，即在前述的的5元组元组中加入中加入第第6个组件个组件谓词集谓词集P，从而把有，从而把有穷状态机扩展为一个穷状态机扩展为一个6元组元组，即，即EFSM。转换函数转换函数T现在是一个

16、从现在是一个从(J-F)KP到到J的函数。现在的的函数。现在的转换转换规则规则形式如下：形式如下：当前状态当前状态+事件事件+谓词谓词 下个状态。下个状态。（上述即是（上述即是EFSM定义）定义）为了具体说明怎样用为了具体说明怎样用EFSM表达系统的规格说明，表达系统的规格说明，现在用这种技术给出大家熟悉的现在用这种技术给出大家熟悉的电梯系统电梯系统的规格说的规格说明。首先给出用明。首先给出用自然语言自然语言描述的对电梯系统的描述的对电梯系统的需求需求：在一幢在一幢m层层的大厦中需要一套控制的大厦中需要一套控制n部电梯部电梯的产品，的产品，要求这要求这n部电梯按照部电梯按照需求需求R1，R2和

17、和R3在楼层间移在楼层间移动。动。R1：每部电梯内每部电梯内有有m个按钮，个按钮，每个按钮每个按钮代表代表一个楼一个楼层层。当。当按下一个按钮按下一个按钮时该按钮时该按钮指示灯亮指示灯亮，同时电梯，同时电梯驶向相应的楼层，驶向相应的楼层，到达到达按钮指定的楼层时指示灯按钮指定的楼层时指示灯熄熄灭灭。4.2.2 例子例子EFSM的状态转换函数：当前状态+事件+谓词=下一个状态R2：除除了大厦的了大厦的最低层最低层和和最高层最高层之外，之外，每层楼每层楼都都有有两个按钮两个按钮分别请求分别请求电梯上行电梯上行和和下行下行。这两个按钮。这两个按钮之一被之一被按按下时相应的指示下时相应的指示灯亮灯亮，

18、当，当电梯到达电梯到达此此楼层楼层时时灯熄灭灯熄灭，电梯向要求的方向移动。，电梯向要求的方向移动。R3：当对电梯：当对电梯没有请求没有请求时，它时，它关门关门并并停在当前楼停在当前楼层层。现在使用一个现在使用一个扩展的有穷状态机扩展的有穷状态机对本产品进行规格对本产品进行规格说明。这个问题中有说明。这个问题中有两个按钮集两个按钮集。n部电梯部电梯中的中的每每一部都有一部都有m个按钮个按钮，一个按钮一个按钮对应对应一个楼层一个楼层。因为。因为这这mn个按钮都在电梯中，所以称它们为个按钮都在电梯中，所以称它们为电梯按电梯按钮钮。此外，。此外，每层楼每层楼有有两个按钮两个按钮，一个，一个请求向上请求

19、向上，另，另一个一个请求向下请求向下，这些按钮称为，这些按钮称为楼层按钮楼层按钮。EFSM的状态转换函数：当前状态+事件+谓词=下一个状态电梯按钮电梯按钮的的状态转换图状态转换图如如图图4.2所示，即所示，即需求需求R1。令令(e,f)表示表示电梯电梯e内的内的按钮按钮f，在某一时刻，在某一时刻电梯按钮电梯按钮(e,f)有两个状态：有两个状态：发光发光(打开打开)和和不发光不发光(关闭关闭)。设这。设这2个状态表示如下：个状态表示如下：EBON(e,f)：电梯按钮：电梯按钮(e,f)打开打开EBOFF(e,f)：电梯按钮：电梯按钮(e,f)关闭关闭如果如果电梯按钮电梯按钮(e,f)发光发光且电

20、梯且电梯到达到达f层层，该，该按钮按钮将将熄熄灭灭。相反相反如果如果按钮熄灭按钮熄灭，则，则按下按下它时，它时，按钮按钮将将发光发光。上述描述上述描述中中包含包含了了两个事件两个事件，它们分别是：，它们分别是：EBP(e,f)：电梯按钮：电梯按钮(e,f)被按下被按下EAF(e,f)：电梯：电梯e到达到达f层层EFSM的状态转换函数：当前状态+事件+谓词=下一个状态图图4.2 电梯按钮的状态转换图电梯按钮的状态转换图图图4.3楼层按钮的状态转换图楼层按钮的状态转换图EFSM的状态转换函数：当前状态+事件+谓词=下一个状态blackboard为了定义为了定义与这些与这些事件事件和和状态状态相联系

21、的相联系的状态转换规则状态转换规则，需要需要一个一个谓词谓词V(e,f)，它的含义如下：，它的含义如下：V(e,f)：电梯：电梯e停在停在f层层如果如果电梯按钮电梯按钮(e,f)处于处于关闭状态关闭状态当前状态当前状态，而，而且且电梯按钮电梯按钮(e,f)被按下被按下事件事件，而且，而且电梯电梯e不在不在f层层谓词谓词，则该，则该电梯按钮打开发光电梯按钮打开发光下个状态下个状态。状态转换规则状态转换规则的的形式化描述形式化描述如下：如下：EBOFF(e,f)+EBP(e,f)+not V(e,f) EBON(e,f)反之反之，如果，如果电梯到达电梯到达f层层，而且，而且电梯按钮是打开的电梯按钮

22、是打开的，于是它就会于是它就会熄灭熄灭。这条。这条转换规则转换规则可以形式化地可以形式化地表示表示为为：EBON(e,f)+EAF(e,f) EBOFF(e,f)EFSM的状态转换函数：当前状态+事件+谓词=下一个状态接下来考虑接下来考虑楼层按钮楼层按钮，即，即需求需求R2。令。令FB(d,f)表示表示f层请求电梯向层请求电梯向d方向运动的方向运动的按钮按钮，楼层按钮楼层按钮FB(d,f)的的状态转换图状态转换图如图如图4.3所示。所示。楼层按钮的状态楼层按钮的状态如下：如下：FBON(d,f)：楼层按钮：楼层按钮(d,f)打开打开FBOFF(d,f)：楼层按钮：楼层按钮(d,f)关闭关闭如果

23、如果楼层按钮楼层按钮已经已经打开打开，而且，而且一部电梯到达一部电梯到达f层层，则则按钮关闭按钮关闭。反之反之，如果，如果楼层按钮楼层按钮原来是原来是关闭关闭的，的，被按下被按下后该后该按钮将打开按钮将打开。这段叙述中包含了以下。这段叙述中包含了以下两两个事件个事件。EFSM的状态转换函数：当前状态+事件+谓词=下一个状态FBP(d,f)：楼层按钮：楼层按钮(d,f)被按下被按下EAF(1n,f)：电梯：电梯1或或或或n到达到达f层层其中其中1n表示表示或为或为1或为或为2或为或为n。为了定义为了定义与这些与这些事件事件和和状态状态相联系的相联系的状态转换规则状态转换规则，同样也需要一个同样也

24、需要一个谓词谓词，它是，它是S(d,e,f)，它的定义如下。，它的定义如下。S(d,e,f)：电梯：电梯e停在停在f层并且移动方向由层并且移动方向由d确定为向确定为向上上(d=U)或向下或向下(d=D)或待定或待定(d=N)。EFSM的状态转换函数：当前状态+事件+谓词=下一个状态使用谓词使用谓词S(d,e,f)，形式化转换规则形式化转换规则为：为：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)其中，其中，d=Uor D。也就是说，如果也就是说，如果在在f层层请求电梯向请求电

25、梯向d方向方向运动的运动的楼层楼层按钮按钮处于处于关闭状态关闭状态，现在，现在该按钮被按下该按钮被按下，并且并且当时当时没有正停在没有正停在f层层准备向准备向d方向移动的电梯方向移动的电梯，则，则该楼层该楼层按钮打开按钮打开。反之反之，如果，如果楼层按钮楼层按钮已经已经打开打开，且，且至少至少有一部电梯到达有一部电梯到达f层层，该部电梯将朝该部电梯将朝d方向运动方向运动，则，则按钮按钮将将关闭关闭。EFSM的状态转换函数：当前状态+事件+谓词=下一个状态有穷状态机有穷状态机方法方法采用采用了一种了一种简单的格式简单的格式来来描述规格描述规格说明说明：当前状态当前状态+事件事件+谓词谓词 下个状

26、态下个状态这种形式的规格说明这种形式的规格说明易于书写易于书写、易于验证易于验证，而且可，而且可以以比较容易比较容易地把它地把它转变成转变成设计设计或或程序代码程序代码。事实上，。事实上，可以可以开发一个开发一个CASE工具工具把一个把一个有穷状态机规格说有穷状态机规格说明明直接直接转变转变为为源代码源代码。维护维护可以通过可以通过重新转变重新转变来实来实现，现，也就是说也就是说，如果需要一个新的状态或事件，首，如果需要一个新的状态或事件，首先修改规格说明，然后先修改规格说明，然后直接直接由新的规格说明由新的规格说明生成生成新新版本的产品。版本的产品。4.2.3 评价评价EFSM的状态转换函数

27、：当前状态+事件+谓词=下一个状态有穷状态机有穷状态机方法比方法比数据流图数据流图技术技术更精确更精确，而且而且和它和它一样易于理解一样易于理解。不过，它。不过，它也有缺点也有缺点：在开发一个：在开发一个大大系统系统时时三元组三元组(即状态、事件、谓词即状态、事件、谓词)的的数量数量会迅速会迅速增长增长。此外，。此外，和数据流图和数据流图方法方法一样一样，形式化的，形式化的有穷有穷状态机状态机方法也方法也没有处理没有处理定时需求。下节将介绍的定时需求。下节将介绍的Petri网网技术，是一种技术，是一种可处理可处理定时问题的形式化方法。定时问题的形式化方法。EFSM的状态转换函数：当前状态+事件

28、+谓词=下一个状态第第4章章 形式化说明技术形式化说明技术前言前言4.1 概述概述4.2 有穷状态机有穷状态机4.3 Petri网网4.4 Z语言语言4.5 小结小结并发系统并发系统中遇到的一个主要问题是中遇到的一个主要问题是定时问题定时问题。这个。这个问题可以问题可以表现为多种形式表现为多种形式，如，如同步问题同步问题、竞争条件竞争条件以及以及死锁问题死锁问题。定时问题定时问题通常是由通常是由不好的设计不好的设计或或有有错误的实现错误的实现引起的，引起的，而而这样的设计或实现通常又是这样的设计或实现通常又是由由不好的规格说明不好的规格说明造成的。造成的。可以应用可以应用Petri网网技术设计

29、技术设计系统规格说明系统规格说明，解决，解决并发并发系统系统遇到的定时问题。遇到的定时问题。4.3 Petri网网 4.3.1 概念概念Petri网网是由是由Carl Adam Petri发明的。发明的。最初最初只有只有自自动化专家动化专家对对Petri网感兴趣，网感兴趣，后来后来Petri网在计算机网在计算机科学中也得到广泛的应用，科学中也得到广泛的应用，例如例如，在性能评价、操，在性能评价、操作系统和软件工程等领域，作系统和软件工程等领域，Petri网应用得都比较广网应用得都比较广泛。泛。特别特别是已经证明，是已经证明，用用Petri网可以有效地描述并网可以有效地描述并发活动。发活动。下面

30、介绍下面介绍3种种Petri网网：（1）最基本的）最基本的Petri网；网；（2）带权标的）带权标的Petri网；网；（3）带禁止线的）带禁止线的Petri网。网。Petri网网包含包含4种元素种元素：一组位置一组位置P（Place）、一组一组转换转换T（Transition）、输入函数输入函数I以及以及输出函数输出函数O。图图4.5举例说明了举例说明了Petri网的组成。网的组成。图图4.5 Petri网的组成网的组成一组位置一组位置P为为P1，P2，P3，P4，在图中用圆圈代表位置，在图中用圆圈代表位置位置P输出函数O转换T输入函数I（1）基本的）基本的Petri网网blackboard一

31、组位置一组位置P为为P1，P2，P3，P4，在图中用，在图中用圆圈圆圈代表代表位置位置。一组转换一组转换T为为t1，t2，在图中用，在图中用短直线短直线表示表示转转换换。两个用于转换的两个用于转换的输入函数输入函数，用由，用由位置指向转换的箭位置指向转换的箭头头表示，它们是：表示，它们是：I(t1)=P2，P4I(t2)=P2两个用于转换的两个用于转换的输出函数输出函数，用由，用由转换指向位置的箭转换指向位置的箭头头表示，它们是：表示，它们是：O(t1)=P1O(t2)=P3，P3注意，输出函数注意，输出函数O(t2)中有两个中有两个P3（1）基本的）基本的Petri网网注意注意，输出函数，输

32、出函数O(t2)中有两个中有两个P3，是，是因为因为有两个有两个箭头由箭头由t2指向指向P3。更形式化的更形式化的Petri网结构网结构，是一个，是一个四元组四元组C=(P,T,I,O)。其中，其中，P=P1，Pn是一个有穷位置集，是一个有穷位置集，n0。T=t1，tm是一个有穷转换集，是一个有穷转换集，m0，且，且T和和P不相交。不相交。I：TP为输入函数，是由转换到位置无序单位组为输入函数，是由转换到位置无序单位组(bags)的映射。的映射。O：TP为输出函数，是由转换到位置无序单位为输出函数，是由转换到位置无序单位组的映射。组的映射。4.3.2 Petri网的动态转换网的动态转换（1）基

33、本的）基本的Petri网网Petri网的网的标记标记是在是在Petri网中网中权标权标(token)的分配。的分配。例如，在例如，在图图4.6中有中有4个个权标，其中一个在权标，其中一个在P1中，两中，两个在个在P2中，中，P3中没有，还有一个在中没有，还有一个在P4中。上述中。上述标标记记可以用可以用向量向量(1，2，0，1)表示。由于表示。由于P2和和P4中有中有权标，因此权标，因此t1启动启动(即被激发即被激发)。通常，当通常，当每个输入每个输入位置位置所拥有的所拥有的权标数权标数大于等于大于等于从从该位置到转换的线该位置到转换的线数数时，就时，就允许转换允许转换。当当t1被激发时，被激

34、发时，P2和和P4上各有上各有一个权标被移出，而一个权标被移出，而P1上则增加一个权标。上则增加一个权标。Petri网中网中权标总数不是固定权标总数不是固定的，在这个例子中两个权标的，在这个例子中两个权标被移出，而被移出，而P1上只能增加一个权标。上只能增加一个权标。（2）带权标的）带权标的Petri网网在图在图4.6中中P2上有权标，因此上有权标，因此t2也可以被激发。当也可以被激发。当t2被激发时，被激发时，P2上将移走一个权标，而上将移走一个权标，而P3上新增加上新增加两个权标。两个权标。Petri网网具有具有非确定性非确定性，也就是说也就是说，如果，如果数个转换都达到了激发条件，则其中

35、数个转换都达到了激发条件，则其中任意一个任意一个都可都可以被激发。图以被激发。图4.6所示所示Petri网的网的标记标记为为(1，2，0，1)，t1和和t2都可以被激发都可以被激发。假设假设t1被激发了，则结果如被激发了，则结果如图图4.7所示，所示，标记标记为为(2，1，0，0)。此时此时，只有，只有t2可可以被激发。如果以被激发。如果t2也被激发了，则权标从也被激发了，则权标从P2中移出，中移出，两个新权标被放在两个新权标被放在P3上，结果如图上，结果如图4.8所示，所示，标记标记为为(2，0，2，0)。（2）带权标的）带权标的Petri网网图图4.6 带标记的带标记的Petri网网（2）

36、带权标的）带权标的Petri网网图图4.7 图图4.6的的Petri网在转换网在转换 t1被激发后的情况被激发后的情况（2）带权标的）带权标的Petri网网图图4.8 图图4.7的的Petri网在转换网在转换 t2被激发后的情况被激发后的情况（2）带权标的）带权标的Petri网网更形式化地说，更形式化地说，Petri网网C=(P，T，I，O)中的中的标记标记M，是由，是由一组位置一组位置P到一组到一组非负整数非负整数的的映射映射：M：P0，1，2，这样，这样，带有标记的带有标记的Petri网网成为一个成为一个五元组五元组(P，T，I，O，M)。（2）带权标的）带权标的Petri网网图图4.9

37、含禁止线的含禁止线的Petri网网（3）带禁止线的）带禁止线的Petri网网禁止线（转换的输入线）对对Petri网网的一个的一个重要扩充重要扩充是加入是加入禁止线禁止线。如图。如图4.9所示，所示，禁止线禁止线是用一个是用一个小圆圈小圆圈而而不是不是用用箭头标记箭头标记的的输入线输入线。通常，当。通常，当每个输入线每个输入线上上至少有一个权标至少有一个权标，而而禁止线禁止线上上没有权标没有权标的时候，相应的的时候，相应的转换才是允许转换才是允许的的。在。在图图4.9中，中，P3上有一个权标而上有一个权标而P2上没有权标，上没有权标，因此因此转换转换t1可以被激发可以被激发。（3）带禁止线的）带

38、禁止线的Petri网网现在把现在把Petri网网应用于应用于上一节讨论过的上一节讨论过的电梯问题电梯问题。当。当用用Petri网网表示表示电梯系统的规格说明电梯系统的规格说明时，时，每个楼层每个楼层用用一个位置一个位置Ff代表代表(1fm)，在，在Petri网中网中电梯电梯是用一是用一个个权标权标代表的。代表的。在位置在位置Ff上有权标，表示在楼层上有权标，表示在楼层f上有电梯。上有电梯。1. 电梯按钮电梯按钮（即需求（即需求R1）电梯问题电梯问题的第一个的第一个需求需求R1描述了电梯按钮的行为描述了电梯按钮的行为，现在现在复述复述一下这个一下这个需求需求R1。4.3.2 例子例子blackb

39、oardPetri网：网：五元组(P，T，I，O，M)需求需求R1：每部电梯：每部电梯有有m个按钮，个按钮，每层每层对应对应一个按钮一个按钮。当当按下按下一个按钮时该按钮一个按钮时该按钮指示灯亮指示灯亮，指示指示电梯移往电梯移往相应的楼层。当电梯相应的楼层。当电梯到达到达指定的楼层时，按钮将指定的楼层时，按钮将熄熄灭灭。为了为了用用Petri网网表达表达电梯按钮的规格说明电梯按钮的规格说明，在，在Petri网中还必须设置网中还必须设置其他的位置其他的位置。电梯中电梯中楼层楼层f的按钮的按钮，在在Petri网中用网中用位置位置EBf表示表示(1fm)。在在EBf上有一上有一个个权标权标，就表示，

40、就表示电梯内楼层电梯内楼层f的按钮的按钮被按下了。被按下了。Petri网：网：五元组(P，T，I，O，M)电梯按钮电梯按钮只有在只有在第一次第一次被按下时才会被按下时才会由暗变亮由暗变亮，以以后后再按它则只会再按它则只会被忽略被忽略。图图4.10所示的所示的Petri网网准确准确地地描述了描述了电梯按钮的行为规律电梯按钮的行为规律。首先首先，假设按钮没假设按钮没有发亮有发亮，显然在，显然在位置位置EBf上上没有权标没有权标，从而在存在，从而在存在禁止线禁止线的情况下，的情况下，转换转换“EBf被按下被按下”是允许发生是允许发生的。假设现在的。假设现在按下按钮按下按钮，则，则转换被激发转换被激发

41、并在并在EBf上上放置了一个放置了一个权标权标，如图，如图4.10所示。所示。以后以后不论再按下不论再按下多少次按钮，禁止线与现有权标的组合都决定了转多少次按钮，禁止线与现有权标的组合都决定了转换换“EBf被按下被按下”不能再被激发了不能再被激发了，因此因此，位置位置EBf上的权标数不会多于上的权标数不会多于1。Petri网：网：五元组(P，T，I，O，M)图图4.10 Petri网表示的电梯按钮网表示的电梯按钮blackboardPetri网：网：五元组(P，T，I，O，M)假设电梯由假设电梯由g层驶向层驶向f层层，因为电梯在，因为电梯在g层，如图层，如图4.10所示，位置所示，位置Fg上上

42、有一个权标有一个权标。由于。由于每条输入线每条输入线上各上各有一个权标，转换有一个权标，转换“电梯在运行电梯在运行”被激发被激发，从而，从而EBf和和Fg上的上的权标被移走权标被移走，按钮按钮EBf被关闭被关闭，在位，在位置置Ff上上出现一个新权标出现一个新权标，即即转换的激发使电梯由转换的激发使电梯由g层驶到层驶到f层。层。事实上事实上，电梯由，电梯由g层移到层移到f层层是是需要时间需要时间的，为处理的，为处理这个情况及其他类似的问题这个情况及其他类似的问题(例如，由于物理上的例如，由于物理上的原因按钮被按下后不能马上发亮原因按钮被按下后不能马上发亮)，Petri网模型网模型中中必须加入时限

43、必须加入时限。也就是说也就是说，在，在标准标准Petri网网中中转换是转换是瞬时完成的瞬时完成的，而，而在现实情况下在现实情况下就就需要时间控制需要时间控制Petri网，以使网，以使转换与非零时间转换与非零时间相联系。相联系。Petri网：网：五元组(P，T，I，O，M)2. 楼层按钮楼层按钮（即需求（即需求R2）在第二个在第二个需求需求R2中描述了中描述了楼层按钮楼层按钮的行为。的行为。需求需求R2：除：除了了第一层与顶层第一层与顶层之外，之外，每个楼层每个楼层都有都有两个按钮两个按钮，一个要求电梯，一个要求电梯上行上行，另一个要求电梯，另一个要求电梯下下行行。这些按钮在。这些按钮在按下按下

44、时时发亮发亮，当电梯，当电梯到达到达该层该层并将并将向指定方向移动向指定方向移动时，相应的时，相应的按钮才会熄灭按钮才会熄灭。在在Petri网中网中楼层按钮楼层按钮用用位置位置FBfu和和FBfd表示，分别表示，分别代表代表f楼层请求电梯上行和下行的按钮楼层请求电梯上行和下行的按钮。底层底层的按的按钮为钮为FB1u，最高层最高层的按钮为的按钮为FBmd，中间中间每一层有每一层有两个按钮两个按钮FBfu和和FBfd(1fm)。图图4.11所示的情况为所示的情况为电梯由电梯由g层驶向层驶向f层层。blackboardPetri网：网：五元组(P，T，I，O，M)图图4.11 Petri网表示楼层按

45、钮网表示楼层按钮Petri网：网：五元组(P，T，I，O，M)最后，考虑第三最后，考虑第三需求需求R3。需求需求R3：当电梯没有收到请求时，它将停留在当当电梯没有收到请求时，它将停留在当前楼层并关门。前楼层并关门。这条需求很容易实现，如图这条需求很容易实现，如图4.11所示，当没有请求所示，当没有请求(FBfu和和FBfd上无权标）时，上无权标）时，任何一个转换任何一个转换“电梯在电梯在运行运行”都不能被激发都不能被激发。Petri网：网：五元组(P，T，I，O，M)第第4章章 形式化说明技术形式化说明技术前言前言4.1 概述概述4.2 有穷状态机有穷状态机4.3 Petri网网4.4 Z语言

46、语言4.5 小结小结用用Z语言语言描述的、最简单的描述的、最简单的形式化规格说明形式化规格说明含有下含有下述述4个部分个部分：1、给定集合。、给定集合。2、状态定义。、状态定义。3、初始状态。、初始状态。4、操作。、操作。4.4 Z语言语言 4.4.1 简介简介1. 给定集合给定集合一个一个Z规格说明规格说明从一系列给定的从一系列给定的初始化集合初始化集合开始。开始。电梯问题中有电梯问题中有两个按钮集两个按钮集。n部电梯中的每一部都有部电梯中的每一部都有m个按个按钮，一个按钮对应一个楼层。因为这钮，一个按钮对应一个楼层。因为这mn个个按钮按钮都都在电梯在电梯中中，所以称它们为，所以称它们为电梯

47、按钮电梯按钮。此外，。此外，每层每层楼有两个按钮，楼有两个按钮，一个请求向上，另一个请求向下，这些按钮称为一个请求向上，另一个请求向下，这些按钮称为楼层按钮楼层按钮。对于对于电梯问题，给定的电梯问题，给定的初始化集合初始化集合称为称为Button，即所有按，即所有按钮的集合钮的集合（即：电梯按钮（即：电梯按钮楼层按钮）楼层按钮）。(“类型类型”“集集合合”)2. 状态定义状态定义“类型类型”“集合集合”的解释说明的解释说明我们可以这么理解我们可以这么理解C语言中的语言中的int类型：类型： int m； -216,-2,-1,0,1,2, 216-1 m；即即“类型类型”“集合集合” “变量变

48、量”“集合中的一个元素集合中的一个元素”步骤步骤3. 初始状态初始状态2. 状态定义状态定义一个一个Z规格说明由若干个规格说明由若干个“格格(schema)”组成组成，每个，每个格含有格含有一组变量说明一组变量说明和和一系列限定变量取值范围的一系列限定变量取值范围的谓词谓词。例如，格。例如，格S的格式如下图所示。的格式如下图所示。（“格格”可用来可用来描述描述系统的系统的状态状态和和操作操作。）。）Button_State格的名称格的名称说明部分说明部分谓词部分谓词部分在在电梯问题电梯问题中，中，Button有有4个子集个子集（变量）（变量），即，即floor_buttons(楼层按钮的集合楼

49、层按钮的集合)、elevator_buttons(电梯按钮的集合电梯按钮的集合)、buttons(电梯电梯问题中所有按钮的集合问题中所有按钮的集合)以及以及pushed(所有被按的按所有被按的按钮的集合，即所有处于打开状态的按钮的集合钮的集合，即所有处于打开状态的按钮的集合)。图图4.13描述了描述了格格Button_State，其中，其中，符号符号P表示幂表示幂集集(即给定集的所有子集的集合即给定集的所有子集的集合)。约束条件声明约束条件声明，floor_buttons集与集与elevator_buttons集集不相交不相交，而且而且它们共同组成它们共同组成buttons集集(在下面的讨论中

50、并不需要在下面的讨论中并不需要floor_buttons集和集和elevator_buttons集，把它们放于集，把它们放于图图4.13中只是用来说明中只是用来说明Z格包含的内容格包含的内容)。自定义类型的说明自定义类型的说明说明部分说明部分谓词部分谓词部分格的名称，此格用来描述系统的按钮格的名称，此格用来描述系统的按钮状态状态类型说明类型说明集合Button的所有子集的集合3. 初始状态初始状态抽象的抽象的初始状态初始状态是指是指系统第一次开启时的状态系统第一次开启时的状态。对。对于于电梯问题电梯问题来说，来说，抽象的初始状态抽象的初始状态为：为：Button_Init Button_Sta