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

《第4章形式化说明技术.ppt》由会员分享，可在线阅读，更多相关《第4章形式化说明技术.ppt（45页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、第第4章章 形式化说明技术形式化说明技术4.1 概述概述4.2 有穷状态机有穷状态机4.3 Petri网网4.4 Z语言语言4.5 小结小结习题习题 软件工程使用的方法划分成：软件工程使用的方法划分成：非形式化、半形式化和形式化非形式化、半形式化和形式化3类。类。非形式化方法：用自然语言描述需求规格说明。非形式化方法：用自然语言描述需求规格说明。半形式化方法：用数据流图或实体半形式化方法：用数据流图或实体-联系图建立模联系图建立模型。型。形式化方法：基于数学的技术来描述系统性质。形式化方法：基于数学的技术来描述系统性质。1 形式化方法的发展形式化方法的发展 形式化方法（形式化方法（formal

2、 methods）的研究高潮始于的研究高潮始于 2020世纪世纪6060年代后期，针对当时所谓年代后期，针对当时所谓“软件危机软件危机”,人人们提出种种解决方法们提出种种解决方法,归纳起来有两类：归纳起来有两类：一是采用工程方法来组织、管理软件的开发程；一是采用工程方法来组织、管理软件的开发程；二是深入探讨程二是深入探讨程 序和程序开发过程的规律，建立序和程序开发过程的规律，建立严密的理论，以其用来指导软件开发实践。严密的理论，以其用来指导软件开发实践。前者导致前者导致“软件工程软件工程”的出现和发展，后者则推动的出现和发展，后者则推动了形式化方法的深入研究。了形式化方法的深入研究。2 形式化

3、方法的定义形式化方法的定义 用于开发计算机系统的形式化方法是描述用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术，这样的形式系统性质的基于数学的技术，这样的形式化方法提供了一个框架，可以在框架中以化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验系统的而不是特别的方式刻划、开发和验 证系统。证系统。如果一个方法有良好的数学基础，如果一个方法有良好的数学基础，那么它就是形式化的，典型地以形式化规那么它就是形式化的，典型地以形式化规约语言给出。约语言给出。3 形式化方法的研究内容形式化方法的研究内容 形式化方法的一个重要研究内容是形式形式化方法的一个重要研究内容是

4、形式规约规约(Formal Specification,(Formal Specification,也称形式规也称形式规范或形式化描述范或形式化描述),),它是对程序它是对程序“做什么做什么”(what to do)(what to do)的数学描述的数学描述,是用具有精确是用具有精确语义的形式语言书写的程序功能描述语义的形式语言书写的程序功能描述,它是它是设计和编制程序的出发点设计和编制程序的出发点,也是验证程序是也是验证程序是否正确的依据。否正确的依据。4 形式化方法的分类形式化方法的分类 根据说明目标软件系统的方式，形式化方法可以根据说明目标软件系统的方式，形式化方法可以分为两类：分为两

5、类：1）面向模型的形式化方法。面向模型的方法通）面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。过构造一个数学模型来说明系统的行为。2）面向属性的形式化方法。面向属性的方法通）面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统过描述目标软件系统的各种属性来间接定义系统行为。行为。根据表达能力，形式化方法可以分为五类：根据表达能力，形式化方法可以分为五类：1.基于模型的方法：通过明确定义状态和操作来建基于模型的方法：通过明确定义状态和操作来建立一个系统模型。立一个系统模型。2.基于逻辑的方法：用逻辑描述系统预期的性能，基于逻辑的方法：用逻辑

6、描述系统预期的性能，包括底层规约、时序和可能性行为。包括底层规约、时序和可能性行为。3.代数方法：通过将未定义状态下不同的操作行为代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的显式定义。相联系，给出操作的显式定义。4.过程代数方法：通过限制所有容许的可观察的过过程代数方法：通过限制所有容许的可观察的过程间通信来表示系统行为。程间通信来表示系统行为。5.基于网络的方法：由于图形化表示法易于理解，基于网络的方法：由于图形化表示法易于理解，而且非专业人员能够使用，因此是一种通用的系而且非专业人员能够使用，因此是一种通用的系统确定表示法。统确定表示法。用自然语言书写的系统规格说明书：存在

7、矛盾、二义用自然语言书写的系统规格说明书：存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。性、含糊性、不完整性及抽象层次混乱等问题。矛盾：指一组相互冲突的陈述。矛盾：指一组相互冲突的陈述。二义性：指读者可以用不同方式理解的陈述。二义性：指读者可以用不同方式理解的陈述。含糊性：系统规格说明书庞大，易出现含糊性。含糊性：系统规格说明书庞大，易出现含糊性。不完整性：遗漏了客户的一些需求。不完整性：遗漏了客户的一些需求。抽象层次混乱：是指在非常抽象的陈述中混进了一些抽象层次混乱：是指在非常抽象的陈述中混进了一些关于细节的低层次陈述。关于细节的低层次陈述。4.1 概述概述 4.1.1 非形式化方

8、法的缺点非形式化方法的缺点 数学特别适合于表示状态，也就是表示数学特别适合于表示状态，也就是表示“做什么做什么”。需求规格说明书主要描述应用系统在运行前和运行需求规格说明书主要描述应用系统在运行前和运行后的状态，因此，数学更适于描述详细的需求。后的状态，因此，数学更适于描述详细的需求。没有二义性，容易发现矛盾和不完整性，没有含糊没有二义性，容易发现矛盾和不完整性，没有含糊性。性。可以在不同的软件工程活动之间平滑地过渡。可以在不同的软件工程活动之间平滑地过渡。功能规格说明与系统设计都用数学表达，易于过渡。功能规格说明与系统设计都用数学表达，易于过渡。它提供了高层确认的手段。它提供了高层确认的手段

9、。可以使用数学方法证明可以使用数学方法证明:设计符合规格说明，程序代设计符合规格说明，程序代码正确地实现了设计结果。码正确地实现了设计结果。4.1.2 形式化方法的优点形式化方法的优点 软件系统的复杂性，仅用少数几个数学公式来描述软件系统的复杂性，仅用少数几个数学公式来描述它很困难。它很困难。即使应用了形式化方法，完整性也是难于保证的。即使应用了形式化方法，完整性也是难于保证的。（遗漏的一些需求）（遗漏的一些需求）4.1.2 形式化方法问题形式化方法问题(1)应该选用适当的表示方法。应该选用适当的表示方法。如果用这种技术描述其不适于描述的概念，则不仅工如果用这种技术描述其不适于描述的概念，则不

10、仅工作量大而且描述方式也很复杂。作量大而且描述方式也很复杂。(2)应该形式化，但不要过分形式化。应该形式化，但不要过分形式化。形式化技术还不适于描述系统的每个方面，形式化技术还不适于描述系统的每个方面，形式化规格说明技术有助于防止含糊和误解，适于说形式化规格说明技术有助于防止含糊和误解，适于说明系统中易出错的或关键的部分。明系统中易出错的或关键的部分。(3)应该估算成本。应该估算成本。为了使用形式化方法，通常需要事先进行大量的培训。为了使用形式化方法，通常需要事先进行大量的培训。最好预先估算所需的成本并编入预算。最好预先估算所需的成本并编入预算。4.1.3 应用形式化方法的准则应用形式化方法的

11、准则(4)应该有形式化方法顾问随时提供咨询。应该有形式化方法顾问随时提供咨询。绝大多数软件工程师对形式化方法中使用的数学和逻绝大多数软件工程师对形式化方法中使用的数学和逻辑并不很熟悉。辑并不很熟悉。(5)不应放弃传统的开发方法。（取长补短效果好）不应放弃传统的开发方法。（取长补短效果好）(6)应该建立详尽的文档。应该建立详尽的文档。使用自然语言注释形式化的规格说明书，以帮助用户使用自然语言注释形式化的规格说明书，以帮助用户和维护人员理解系统。和维护人员理解系统。(7)不应该放弃质量标准。不应该放弃质量标准。形式化方法并不能保证软件的正确性，在开发过程中形式化方法并不能保证软件的正确性，在开发过

12、程中仍需实施其他质量保证活动。仍需实施其他质量保证活动。(8)不应该盲目依赖形式化方法。不应该盲目依赖形式化方法。形式化方法并不能保证开发出的软件绝对正确。形式化方法并不能保证开发出的软件绝对正确。(9)应该测试、测试再测试。应该测试、测试再测试。形式化方法不能证明系统性能或其他质量指标是否形式化方法不能证明系统性能或其他质量指标是否符合需要，因此，软件测试的重要性并没有降低。符合需要，因此，软件测试的重要性并没有降低。(10)应该重用。应该重用。用形式化方法说明的软件构件具有清晰定义的功用形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们有更好的可重用性。能和接口，使得它们有更好的可

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

14、有穷状态机 4.2.1 概念概念图图4.1 保险箱的状态转换图保险箱的状态转换图图图4.1是一个有穷状态机的状态转换图。状态转换并是一个有穷状态机的状态转换图。状态转换并不一定要用图形方式描述，表不一定要用图形方式描述，表4.1（见书（见书68页）的表页）的表格形式也可以表达同样的信息。格形式也可以表达同样的信息。从上面这个简单例子可以看出，一个有穷状态机包括从上面这个简单例子可以看出，一个有穷状态机包括下述下述5个部分：状态集个部分：状态集J、输入集、输入集K、由当前状态和当、由当前状态和当前输入确定下一个状态前输入确定下一个状态(次态次态)的转换函数的转换函数T、初始态、初始态S和终态集和

15、终态集F。对于保险箱的例子，相应的有穷状态机。对于保险箱的例子，相应的有穷状态机的各部分如下。的各部分如下。状态集状态集J：保险箱锁定，：保险箱锁定，A，B，保险箱解锁，报警，保险箱解锁，报警。输入集输入集K：1L，1R，2L，2R，3L，3R。转换函数转换函数T：如表：如表4.1所示。所示。初始态初始态S：保险箱锁定。：保险箱锁定。终态集终态集F：保险箱解锁，报警。：保险箱解锁，报警。如果使用更形式化的术语，一个有穷状态机可以表示如果使用更形式化的术语，一个有穷状态机可以表示为一个为一个5元组元组(J，K，T，S，F)，其中：，其中：J是一个有穷的非空状态集；是一个有穷的非空状态集；K是一个

16、有穷的非空输入集；是一个有穷的非空输入集；T是一个从是一个从(J-F)K到到J的转换函数；的转换函数；SJ，是一个初始状态；，是一个初始状态；FJ，是终态集。，是终态集。有穷状态机的概念在计算机系统中应用得非常广泛。有穷状态机的概念在计算机系统中应用得非常广泛。例如，每个菜单驱动的用户界面都是一个有穷状态机例如，每个菜单驱动的用户界面都是一个有穷状态机的实现。一个菜单的显示和一个状态相对应，键盘输的实现。一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他状态的一入或用鼠标选择一个图标是使系统进入其他状态的一个事件。状态的每个转换都具有下面的形式：个事件。状态的每个转换

17、都具有下面的形式：当前状态当前状态菜单菜单+事件事件所选择的项所选择的项下个状态。下个状态。为了对一个系统进行规格说明，通常都需要对有穷状为了对一个系统进行规格说明，通常都需要对有穷状态机做一个很有用的扩展，即在前述的态机做一个很有用的扩展，即在前述的5元组中加入元组中加入第第6个组件个组件谓词集谓词集P，从而把有穷状态机扩展为，从而把有穷状态机扩展为一个一个6元组，其中每个谓词都是系统全局状态元组，其中每个谓词都是系统全局状态Y的函的函数。转换函数数。转换函数T现在是一个从现在是一个从(J-F)KP到到J的函数。的函数。现在的转换规则形式如下：现在的转换规则形式如下：当前状态当前状态菜单菜单

18、+事件事件所选择的项所选择的项+谓词谓词下下个状态。个状态。4.2.24.2.2例题例题：一个浮点二进制数的构成是：一个可选的：一个浮点二进制数的构成是：一个可选的符号符号(+(+或或-)-)，后跟一个或多个二进制位，再跟上一个字，后跟一个或多个二进制位，再跟上一个字符符E E，再加上另一个可选符号，再加上另一个可选符号(+(+或或-)-)及一个或多个二进及一个或多个二进制位。例如，下列的字符串都是浮点二进制数：制位。例如，下列的字符串都是浮点二进制数：110101E-101110101E-101-100111E11101-100111E11101+1E0+1E0更形式化地，浮点二进制数定义如

19、下：更形式化地，浮点二进制数定义如下：floatingfloatingpointpoint binarybinary=signsignbitstringbitstringE Esignsignbitstringbitstringsignsign=+=+-bitstringbitstring=bitbitbitstringbitstringbitbit=0=01 1其中，其中，符号符号=表示定义为；表示定义为；符号符号.表示可选项；表示可选项；符号符号a ab b表示表示a a或或b b。假设有这样一个有穷状态机：以一串字符为输入，判假设有这样一个有穷状态机：以一串字符为输入，判断字符串中是否含

20、有合法的浮点二进制数。试对这个有断字符串中是否含有合法的浮点二进制数。试对这个有穷状态机进行规格说明。穷状态机进行规格说明。该该有有穷穷状状态态机机的的初初态态是是“等等待待字字符符串串输输人人”。在在初初态态若若接接收收到到字字符符十十、或或字字符符一一、或或二二进进制制位位，则则进进人人“输输人人尾尾数数”状状态态；在在初初态态若若接接收收到到其其他他字字符符，则则进进人人终终态态“非非浮浮点点二二进进制制数数”。在在“输输人人尾尾数数”状状态态若若接接收收到到二二进进制制位位，则则保保持持该该状状态态不不变变；若若接接收收到到字字符符 E E，则则进进人人“等等待待输输人人指指数数”状状

21、态态；若若接接收收到到其其他他字字符符，则则进进人人终终态态“非非浮浮点点二二进进制制数数”。在在“等等待待输输人人指指数数”状状态态若若接接收收到到字字符符、或或字字符符一一、或或二二进进制制位位，则则进进人人“输输人人指指数数”状状态态；若若接接收收到到其其他他字字符符，则则进进人人终终态态“非非浮浮点点二二进进制制数数”。在在“输输人人指指数数”状状态态若若接接收收到到二二进进制制位位，则则保保持持该该状状态态不不变变；若若输输人人其其他他字字符符，则则进进人人终终态态“非非浮浮点点二二进进制制数数”；若若输输人人结结束束，则进人终态则进人终态“浮点二进制数浮点二进制数”。仔仔细细研研究

22、究图图示示的的有有穷穷状状态态机机可可以以发发现现，它它还还有有不不够够严严格格的的地地方方。有有兴兴趣趣的的同同学学请请进进一一步步改改进进它它，画画出出更更严严格格的的、与与浮浮点点二二进进制制数数定定义义完完全全一一致致的的有有穷穷状态机。状态机。有穷状态机方法采用了一种简单的格式来描述规格说有穷状态机方法采用了一种简单的格式来描述规格说明：明：当前状态当前状态+事件事件+谓词谓词下个状态下个状态这种形式的规格说明易于书写、易于验证，而且可以这种形式的规格说明易于书写、易于验证，而且可以比较容易地把它转变成设计或程序代码。事实上，可比较容易地把它转变成设计或程序代码。事实上，可以开发一个

23、以开发一个CASE工具把一个有穷状态机规格说明直工具把一个有穷状态机规格说明直接转变为源代码。维护可以通过重新转变来实现，也接转变为源代码。维护可以通过重新转变来实现，也就是说，如果需要一个新的状态或事件，首先修改规就是说，如果需要一个新的状态或事件，首先修改规格说明，然后直接由新的规格说明生成新版本的产品。格说明，然后直接由新的规格说明生成新版本的产品。4.2.3 评价评价有穷状态机方法比数据流图技术更精确，而且和它一有穷状态机方法比数据流图技术更精确，而且和它一样易于理解。不过，它也有缺点：在开发一个大系统样易于理解。不过，它也有缺点：在开发一个大系统时三元组时三元组(即状态、事件、谓词即

24、状态、事件、谓词)的数量会迅速增长。的数量会迅速增长。此外，和数据流图方法一样，形式化的有穷状态机方此外，和数据流图方法一样，形式化的有穷状态机方法也没有处理定时需求。下节将介绍的法也没有处理定时需求。下节将介绍的Petri网技术，网技术，是一种可处理定时问题的形式化方法。是一种可处理定时问题的形式化方法。4.3 Petri网网 PetriPetri网是对离散并行系统的数学表示。网是对离散并行系统的数学表示。PetriPetri网是网是19601960年代由卡尔年代由卡尔AA佩特里发明佩特里发明的，适合于描述异步的、并发的计算机系统的，适合于描述异步的、并发的计算机系统模型。模型。PetriP

25、etri网既有严格的数学表述方式，网既有严格的数学表述方式，也有直观的图形表达方式，既有丰富的系统也有直观的图形表达方式，既有丰富的系统描述手段和系统行为分析技术，又为计算机描述手段和系统行为分析技术，又为计算机科学提供坚实的概念基础。科学提供坚实的概念基础。4.3.1 概念概念 并发系统中遇到的一个主要问题是定时问题。并发系统中遇到的一个主要问题是定时问题。表现形式：如同步问题、竞争条件以及死锁问题。表现形式：如同步问题、竞争条件以及死锁问题。定时问题通常是由不好的规格说明造成的。规格定时问题通常是由不好的规格说明造成的。规格说明不恰当，则导致不完善的设计或实现。说明不恰当，则导致不完善的设

26、计或实现。解决这种问题的一种有效技术是解决这种问题的一种有效技术是Petri网。网。Petri网包含网包含4种元素：种元素：一组位置一组位置P、一组转换、一组转换T、输入函数、输入函数I及输出函数及输出函数O。图图4.5举例说明了举例说明了Petri网的组成。网的组成。图图4.5 Petri网的组成网的组成 一组位置：用圆圈表示一组位置：用圆圈表示 P为为P1，P2，P3，P4 一组转换：用短直线表示。一组转换：用短直线表示。T为为t1，t2，用于转换的输入用于转换的输入/出函数出函数 输入函数：由位置指向转换的箭头表示。输入函数：由位置指向转换的箭头表示。I(t1)=P2，P4 I(t2)=

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

28、的标记：是在网的标记：是在Petri网中权标网中权标(token)的分配。的分配。例如，在图例如，在图4.6中有中有4个权标，个权标，P1：1，P2：2，P3：0，P4：1。上述标记用向量上述标记用向量(1，2，0，1)表示。表示。由于由于P2和和P4中有权标，因此中有权标，因此t1启动启动(即被激发即被激发)。当每个输入位置所拥有的权标数大于等于从该位置当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。到转换的线数时，就允许转换。当当t1被激发时，被激发时，P2和和P4上各有一个权标被移出，而上各有一个权标被移出，而P1上则增加一个权标。上则增加一个权标。Petri网中

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

30、为网的标记为(1，2，0，1)，t1和和t2都都可以被激发。可以被激发。假设假设t1被激发，结果如图被激发，结果如图4.7所示，标记为所示，标记为(2，1，0，0)。此时，只有此时，只有t2可以被激发。如果可以被激发。如果t2也被激发了，则也被激发了，则权标从权标从P2中移出，两个新权标被放在中移出，两个新权标被放在P3上，结果如图上，结果如图4.8所示，标记为所示，标记为(2，0，2，0)。图图4.7 图图4.6的的Petri网在转换网在转换 t1被激发后的情况被激发后的情况图图4.8 图图4.7的的Petri网在转换网在转换 t2被激发后的情况被激发后的情况 更形式化地说，更形式化地说，P

31、etri网网C=(P，T，I，O)中的标记中的标记M，是由一组位置，是由一组位置P到一组非负整数的映射。到一组非负整数的映射。M：P0，1，2，这样，带有标记的这样，带有标记的Petri网成为一个五元组网成为一个五元组(P，T，I，O，M)。对对Petri网的一个重要扩充是加入禁止线，如图网的一个重要扩充是加入禁止线，如图4.9所示。所示。禁止线：是用一个小圆圈而不是用箭头标记的输入禁止线：是用一个小圆圈而不是用箭头标记的输入线。线。当每个输入线上至少有一个权标，而禁止线上没有当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许的。权标的时候，相应的转换才是允许的。在图在

32、图4.9中，中，P3上有一个权标而上有一个权标而P2上没有权标，因上没有权标，因此转换此转换t1可以被激发。可以被激发。图图4.9 含禁止线的含禁止线的Petri网网 把把Petri网应用于电梯问题。网应用于电梯问题。当用当用Petri网表示电梯系统的规格说明时，网表示电梯系统的规格说明时，每个楼层用一个位置每个楼层用一个位置Ff代表代表(1fm)，电梯是用一个权标代表的。电梯是用一个权标代表的。在位置在位置Ff上有权标，表示在楼层上有权标，表示在楼层f上有电梯。上有电梯。1.电梯按钮电梯按钮 电梯问题的第一个约束条件描述了电梯问题的第一个约束条件描述了电梯按钮电梯按钮的行为。的行为。4.3.

33、2 例子例子1.电梯按钮电梯按钮第一条约束第一条约束C1：每部电梯有：每部电梯有m个按钮，每层对应一个个按钮，每层对应一个按钮。当按下一个按钮时该按钮指示灯亮，指示电梯按钮。当按下一个按钮时该按钮指示灯亮，指示电梯移往相应的楼层。当电梯到达指定的楼层时，按钮将移往相应的楼层。当电梯到达指定的楼层时，按钮将熄灭。熄灭。电梯中楼层电梯中楼层f的按钮，在的按钮，在Petri网中用位置网中用位置EBf表示表示(1fm)。在。在EBf上有一个权标，就表示电梯内楼层上有一个权标，就表示电梯内楼层f的的按钮被按下了。按钮被按下了。电梯按钮只有在第一次被按下时才会由暗变亮，以电梯按钮只有在第一次被按下时才会由

34、暗变亮，以后再按它则只会被忽略。后再按它则只会被忽略。1.电梯按钮电梯按钮电梯按钮的行为规律：电梯按钮的行为规律：首先，假设按钮没有发亮，显然在位置首先，假设按钮没有发亮，显然在位置EBf上没有上没有权标，从而在存在禁止线的情况下，转换权标，从而在存在禁止线的情况下，转换“EBf被按被按下下”是允许发生的。是允许发生的。假设现在按下按钮，则转换被激发并在假设现在按下按钮，则转换被激发并在EBf上放置上放置了一个权标，如图了一个权标，如图4.10所示。以后不论再按下多少次所示。以后不论再按下多少次按钮，禁止线与现有权标的组合都决定了转换按钮，禁止线与现有权标的组合都决定了转换“EBf被按下被按下

35、”不能再被激发了，因此，位置不能再被激发了，因此，位置EBf上的权标上的权标数不会多于数不会多于1。图图4.10 Petri网表示的电梯按钮网表示的电梯按钮 假设电梯在假设电梯在g层，如图层，如图4.10所示，位置所示，位置Fg上有一个上有一个权标。权标。由于每条输入线上各有一个权标，转换由于每条输入线上各有一个权标，转换“电梯在运电梯在运行行”被激发，从而被激发，从而EBf和和Fg上的权标被移走，按钮上的权标被移走，按钮EBf被关闭，在位置被关闭，在位置Ff上出现一个新权标，即转换的激上出现一个新权标，即转换的激发使电梯由发使电梯由g层驶到层驶到f层。层。电梯由电梯由g层移到层移到f层是需要

36、时间的，也就是说，在层是需要时间的，也就是说，在标准标准Petri网中转换是瞬时完成的，而在现实情况下网中转换是瞬时完成的，而在现实情况下就需要时间控制就需要时间控制Petri网，使转换与非零时间相联系。网，使转换与非零时间相联系。2.楼层按钮楼层按钮 在第二个约束条件中描述了楼层按钮的行为。在第二个约束条件中描述了楼层按钮的行为。第二条约束第二条约束C2：除了第一层与顶层之外，每个楼层：除了第一层与顶层之外，每个楼层都有两个按钮，一个要求电梯上行，另一个要求电梯都有两个按钮，一个要求电梯上行，另一个要求电梯下行。这些按钮在按下时发亮，当电梯到达该层并将下行。这些按钮在按下时发亮，当电梯到达该

37、层并将向指定方向移动时，相应的按钮才会熄灭。向指定方向移动时，相应的按钮才会熄灭。在在Petri网中楼层按钮用位置网中楼层按钮用位置FBfu和和FBfd表示，分别表示，分别代表代表f楼层请求电梯上行和下行的按钮。楼层请求电梯上行和下行的按钮。底层的按钮为底层的按钮为FB1u，最高层的按钮为最高层的按钮为FBmd，中间每一层有两个按钮中间每一层有两个按钮FBfu和和FBfd(1fm)。图图4.11 Petri网表示楼层按钮网表示楼层按钮 图图4.11所示的情况为电梯由所示的情况为电梯由g层驶向层驶向f层。根据电梯层。根据电梯乘客的要求，某一个楼层按钮亮或两个楼层按钮都亮。乘客的要求，某一个楼层按

38、钮亮或两个楼层按钮都亮。如果两个按钮都亮了，则只有一个按钮熄灭。如果两个按钮都亮了，则只有一个按钮熄灭。图图4.11所示的所示的Petri网可以保证，当两个按钮都亮了网可以保证，当两个按钮都亮了的时候，只有一个按钮熄灭。但是要保证按钮熄灭正的时候，只有一个按钮熄灭。但是要保证按钮熄灭正确，则需要更复杂的确，则需要更复杂的Petri网模型。网模型。最后，考虑第三条约束。最后，考虑第三条约束。第三条约束第三条约束C3：当电梯没有收到请求时，它将停留：当电梯没有收到请求时，它将停留在当前楼层并关门。在当前楼层并关门。这条约束很容易实现，如图这条约束很容易实现，如图4.11所示，当没有请求所示，当没有请求(FBfu和和FBfd上无权标）时，任何一个转换上无权标）时，任何一个转换“电梯在运电梯在运行行”都不能被激发。都不能被激发。