《软件工程 第14章：形式化方法.ppt》由会员分享，可在线阅读，更多相关《软件工程 第14章：形式化方法.ppt（79页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、软件工程软件工程Software Engineering2022/12/221广东工业大学计算机学院第第14章章形式化方法形式化方法o形式化方法提供了规约环境的基础，它使得所生成形式化方法提供了规约环境的基础，它使得所生成的分析模型比用传统的或面向对象的方法生成的模的分析模型比用传统的或面向对象的方法生成的模型更完整、一致和无二义性。型更完整、一致和无二义性。o本章内容：本章内容：o14.1基础知识基础知识o14.2有限状态机（有限状态机（FSM）o14.3PETRI网基本原理网基本原理2022/12/222广东工业大学计算机学院14.1基础知识基础知识o形式化方法的定义：形式化方法的定义：o
2、定义定义14.1：用于开发计算机系统的形式化方法：用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术。这样的形式化是描述系统性质的基于数学的技术。这样的形式化方法提供了一个框架，人们可以在框架中以系统的方法提供了一个框架，人们可以在框架中以系统的方式刻画、开发和验证系统。方式刻画、开发和验证系统。o形式化规约的目标：无二义性、一致性和完整性。形式化规约的目标：无二义性、一致性和完整性。o注：使用形式化方法，完整性是难以达到的。注：使用形式化方法，完整性是难以达到的。2022/12/223广东工业大学计算机学院14.1.1形式化方法概念形式化方法概念o例例14-1：符号表：它由一组没有
3、重复的项构成。如图：符号表：它由一组没有重复的项构成。如图14-1所示。程序被用于维护一个符号表，在许多不同类型的应所示。程序被用于维护一个符号表，在许多不同类型的应用中使用此符号表。用中使用此符号表。oo图图14-1符号表符号表2022/12/224广东工业大学计算机学院例例14-1o如果对于上表有一个陈述：包括不多于如果对于上表有一个陈述：包括不多于MaxIds的的用户名，那么就为表设定了一个限制，这就称为数用户名，那么就为表设定了一个限制，这就称为数据不变式的条件的一个构成成分。数据不变式是一据不变式的条件的一个构成成分。数据不变式是一个条件，它在包含一组数据的系统的执行过程中总个条件，
4、它在包含一组数据的系统的执行过程中总保持为真。上面讨论的符号表的数据不变式有两个保持为真。上面讨论的符号表的数据不变式有两个构成成分：构成成分：o（1）表中包含的名字数不超过）表中包含的名字数不超过MaxIds。o（2）在表中没有重复的名字。在上面描述的符号）在表中没有重复的名字。在上面描述的符号表程序的情形下，这意味系统执行过程中无论什么表程序的情形下，这意味系统执行过程中无论什么时候检查符号表，它将总是包含不超过时候检查符号表，它将总是包含不超过MaxIds的的职员标识符，并且没有重复。职员标识符，并且没有重复。2022/12/225广东工业大学计算机学院形式化方法概念形式化方法概念o状态
5、的概念，在形式化方法的语言环境中，状态是状态的概念，在形式化方法的语言环境中，状态是系统访问和修改的存储数据。在上述符号表程序的系统访问和修改的存储数据。在上述符号表程序的例子中，状态是符号表。例子中，状态是符号表。o操作的概念，这是在系统中发生的读或写状态数据操作的概念，这是在系统中发生的读或写状态数据的动作。如果对符号表程序考虑从符号表加入或移的动作。如果对符号表程序考虑从符号表加入或移出职员名，则它将关联两个操作：一个是加一个指出职员名，则它将关联两个操作：一个是加一个指定名到符号表中的操作，另一个是从表中移出一个定名到符号表中的操作，另一个是从表中移出一个现存名的操作。如果程序提供检查
6、某指定名是否包现存名的操作。如果程序提供检查某指定名是否包含在表中的机制，则有一个返回某种表示名字是否含在表中的机制，则有一个返回某种表示名字是否在表中的指示值的操作。在表中的指示值的操作。2022/12/226广东工业大学计算机学院o一个操作和两个条件相关联：前置条件和后置条件。一个操作和两个条件相关联：前置条件和后置条件。前置条件定义某特定操作在其中合法的环境。操作前置条件定义某特定操作在其中合法的环境。操作的后置条件定义当操作完成后所产生的现象，是通的后置条件定义当操作完成后所产生的现象，是通过其对状态的影响来定义的。在加标识符到职员标过其对状态的影响来定义的。在加标识符到职员标识符符号
7、表的操作的例子中，后置条件已经将数学识符符号表的操作的例子中，后置条件已经将数学的刻画表增加了新标识符。的刻画表增加了新标识符。2022/12/227广东工业大学计算机学院14.1.2形式化规约语言形式化规约语言o形式化规约语言通常由三个主要的成分构成：形式化规约语言通常由三个主要的成分构成：o（1）语法，定义用于表示规约的特定符号。）语法，定义用于表示规约的特定符号。o（2）语义，帮助定义用于描述系统的）语义，帮助定义用于描述系统的“对象的全对象的全域（域（universeofobjects）”。o（3）一组关系，定义确定出哪个对象真正满足规）一组关系，定义确定出哪个对象真正满足规约的规则。
8、约的规则。2022/12/228广东工业大学计算机学院Z的符号的缩略集合：的符号的缩略集合：o集合：集合：oS PX S被声明为被声明为X的集合。的集合。ox Sx是是S中的成员。中的成员。oxS x不是不是S中的成员。中的成员。oST S是是T的子集：的子集：S中每个元素均在中每个元素均在T中。中。oS TS和和T的并：包含在的并：包含在S或或T或两者中的或两者中的每个元素。每个元素。oSTS和和T的交：包含同时在的交：包含同时在S和和T中的元中的元素。素。2022/12/229广东工业大学计算机学院oSTS和和T的差：包含在的差：包含在S中的而不在中的而不在T中中的每个元素。的每个元素。o
9、空集：不包含任何成员。空集：不包含任何成员。ox单元素集：仅仅包含单元素集：仅仅包含x元素。元素。oN自然数集合：自然数集合：0，1，2，oS FXS被声明为被声明为X的有限集。的有限集。oMax(S)数的非空集合数的非空集合S中的最大元素。中的最大元素。2022/12/2210广东工业大学计算机学院o功能：功能：of xyf被声明为从被声明为从x到到y的部分内射。的部分内射。odomff的定义域的定义域:f(x)有定义的值有定义的值x的集合的集合oranff的值域的值域:x在在f的定义域上变化而形的定义域上变化而形成的成的f(x)值的集合。值的集合。ofxy一个和一个和f相同的函数，除了相同
10、的函数，除了x被映射被映射到到y(x)值的集合。值的集合。oxf一个和一个和f相似的函数，除了相似的函数，除了x被从定被从定义域中去除。义域中去除。2022/12/2211广东工业大学计算机学院o逻辑：逻辑：oP QP与与Q同时为真时才为真。同时为真时才为真。oPQP蕴含蕴含Q：或者：或者Q为真或者为真或者P为假时为真。为假时为真。oS=S在操作中在操作中schemaS中没有成分改中没有成分改变。变。2022/12/2212广东工业大学计算机学院例例14-2o例例14-2：下面用：下面用Z语言语言schema的例子描述了块的例子描述了块处理器的状态和数据不变式：处理器的状态和数据不变式：202
11、2/12/2213广东工业大学计算机学院14.2有限状态机（有限状态机（FSM）o很多实时系统，特别是实时控制系统，其整个分析很多实时系统，特别是实时控制系统，其整个分析机制与系统的状态有相当大的关系。有限状态机由机制与系统的状态有相当大的关系。有限状态机由有限的状态和相互之间的转移构成，在任何时候只有限的状态和相互之间的转移构成，在任何时候只能是给定数目的状态中的一个。能是给定数目的状态中的一个。o主要有两种方法来建立有限状态机，一种是主要有两种方法来建立有限状态机，一种是“状态状态转移图转移图”，另一种是，另一种是“状态转移表状态转移表”，分别用图形方，分别用图形方式和表格方式建立有限状态
12、机。式和表格方式建立有限状态机。2022/12/2214广东工业大学计算机学院有限状态机的组成如下：有限状态机的组成如下：o（1）一个有限的状态集合）一个有限的状态集合Q。o（2）一个有限的输入集合）一个有限的输入集合I。o（3）一个变迁函数）一个变迁函数：QIQ变迁函数也是一变迁函数也是一个状态函数，在某一状态下，给定输入后，个状态函数，在某一状态下，给定输入后，FSM转入该函数产生的新状态。转入该函数产生的新状态。的定义域内的某些数的定义域内的某些数值可以是未定义的。值可以是未定义的。2022/12/2215广东工业大学计算机学院简单有限状态机图图14-2中的左图表明该中的左图表明该FSM
13、有有q0、q1、q2、q3四个四个状态，输入集中有状态，输入集中有a、b、c、四个元素；右图中各、四个元素；右图中各个状态之间的转换关系则更清晰。有限状态机非常个状态之间的转换关系则更清晰。有限状态机非常适合于描述这样的系统：系统含有有限个状态，不适合于描述这样的系统：系统含有有限个状态，不同事件的发生可以用不同状态之间的转换来模拟同事件的发生可以用不同状态之间的转换来模拟。2022/12/2216广东工业大学计算机学院有限状态机的特点有限状态机的特点o有限状态机的优点在于简单易用，状态间的关系能有限状态机的优点在于简单易用，状态间的关系能够直观看到。够直观看到。o但应用在实时系统中时，其最大
14、的缺点是：任何时但应用在实时系统中时，其最大的缺点是：任何时刻系统只能有一个状态，无法表示并发性，不能描刻系统只能有一个状态，无法表示并发性，不能描述异步并发的系统。另外，在系统部件较多时，状述异步并发的系统。另外，在系统部件较多时，状态数随之增加，导致复杂性显著增长。态数随之增加，导致复杂性显著增长。2022/12/2217广东工业大学计算机学院14.3Petri网基本原理网基本原理oPetri网在软件分析中，是一种系统的数学和图形网在软件分析中，是一种系统的数学和图形的描述与分析的方法。对于具有并发、异步、分布、的描述与分析的方法。对于具有并发、异步、分布、并行、不确定性或随机性的信息处理
15、系统，都可以并行、不确定性或随机性的信息处理系统，都可以利用利用Petri网构造出要开发的网构造出要开发的Petri网模型。这种网模型。这种模型可以表示系统结构和动态行为方面的信息。模型可以表示系统结构和动态行为方面的信息。2022/12/2218广东工业大学计算机学院o由于由于Petri网的表示方法是用图形工具。因此其表网的表示方法是用图形工具。因此其表示形式与传统方法的结构图、流程图具有同样的直示形式与传统方法的结构图、流程图具有同样的直观、形象效果。其特别之处在于可以使用标记模拟观、形象效果。其特别之处在于可以使用标记模拟系统的动态行为和并发活动。另一方面，作为一种系统的动态行为和并发活
16、动。另一方面，作为一种数学工具，便于计算和验证系统的数学方程。它可数学工具，便于计算和验证系统的数学方程。它可以建立状态方程、代数方程以及系统行为的其他数以建立状态方程、代数方程以及系统行为的其他数学模型。因此，系统开发人员和理论研究工作者都学模型。因此，系统开发人员和理论研究工作者都可以根据需要利用可以根据需要利用Petri网。网。2022/12/2219广东工业大学计算机学院14.3.1静态结构静态结构oPetri网的基本成分可以表示为一个三元组：网的基本成分可以表示为一个三元组：N=（P，T；F）o并满足以下条件：并满足以下条件：（1）P T。（2）PT=。（3）F（PT）（TP）。）。
17、（4）DOM（F）COD（F）=P T。2022/12/2220广东工业大学计算机学院o其中：其中：P=p1，p2，pn是是N的有穷位置的有穷位置集合。集合。T=t1，t2，tn是是N的有穷转移集合。的有穷转移集合。F是由是由N中一个中一个P元素和一个元素和一个T元素组成的有序偶元素组成的有序偶的集合。的集合。DOM（F）=xy：（：（y，x）F，COD（F）=xy：（：（x，y）F。如果用圆圈表示位置，用矩形框表示转移，用有如果用圆圈表示位置，用矩形框表示转移，用有向边表示位置与转移的有序偶，那么就构成了向边表示位置与转移的有序偶，那么就构成了Petri网的图形表示。网的图形表示。2022/
18、12/2221广东工业大学计算机学院例例14-3:N的的Petri网网o例例14-3：N的的Petri网网N=（P，T；F）P=p1，p2，p3，p4，p5，p6 T=t1，t2，t3，t4，t5，t6 F=(p1，t1)，(t1，p2)，(p2，t2)，(t2，p1)，(p1,t3)，(t3，p3)，(t3，p4)，(p3，t4)，(p4，t5)，(t4，p5)，(t5，p6)，(p5，t6)，(p6，t6)oN的的Petri网图形表示，如图网图形表示，如图14-3所示。所示。2022/12/2222广东工业大学计算机学院图14-3 N的Petri网的图形表示2022/12/2223广东工业
19、大学计算机学院14.3.2动态特征动态特征o具有动态特征的具有动态特征的Petri网就可以表示为六元组：网就可以表示为六元组：=（P，T；F，K，W，M0）o其中：（其中：（P，T；F）的含义与前面静态结构中的含）的含义与前面静态结构中的含义相同。义相同。oK：PN+w，是位置上容量函数，是位置上容量函数，N+=1，2，3，；若；若K(p)=w，表示位置，表示位置p的容的容量为无穷。量为无穷。oW：FN+，是弧集合上的权函数。，是弧集合上的权函数。oM：PN0，是，是Petri网网的标识（的标识（marking），），M0为初始标识，为初始标识，N0=0，1，2，3，p P，必须满足，必须满足
20、M（p）K（p）。）。2022/12/2224广东工业大学计算机学院o在在Petri网的图形表示中，弧（网的图形表示中，弧（x，y）上的）上的W值标值标在弧（在弧（x，y）上，）上，M(p)的值不是用数字，而是用的值不是用数字，而是用实心点表示，即在位置实心点表示，即在位置P对应的圆圈中标注对应的圆圈中标注M(p)个实心点，每个实心点称为一个标记（个实心点，每个实心点称为一个标记（token）。）。同一位置中的诸多标记代表同一类完全等价的个体。同一位置中的诸多标记代表同一类完全等价的个体。2022/12/2225广东工业大学计算机学院例例14-4：具有：具有M0和和W的的Petri网可以表示为
21、网可以表示为如图如图14-4所示。所示。图14-4 具有M0和W的Petri网 2022/12/2226广东工业大学计算机学院对于图对于图14-4所示的所示的Petri网：网：M0=（1，0，0，0，0，0）W（t2，p1）=W（t5，p6）=W（t6，p1）=4W（t3，p3）=6W（t4，p5）=5W（p1，t3）=W（p3，t4）=W（p5，t6）=W（p6，t6）=W（t3，p4）=W（p4，t5）=W（p1，t1）=W（t1，p2）=W（p2，t2）=12022/12/2227广东工业大学计算机学院14.3.3转移启动规则转移启动规则o前面介绍的前面介绍的Petri网的动态特征是网的
22、动态特征是Petri网的动态网的动态行为的特性描述。这种动态行为是通过转移启动引行为的特性描述。这种动态行为是通过转移启动引起标识改变的变化来体现的。而转移启动则要有可起标识改变的变化来体现的。而转移启动则要有可以启动转移（转移有效）的条件和启动规则。以启动转移（转移有效）的条件和启动规则。2022/12/2228广东工业大学计算机学院1.转移转移t有效的条件有效的条件o若在标识若在标识M下，下，p1，p1*tM（p1）W（p1，t），且：），且：op2，p2 t*M（p2）W（t，p2）K（p2）o此时称此时称t在在M下有效，记为下有效，记为Mt。o在定义转移有效的条件时，如果一个没有任何输
23、入在定义转移有效的条件时，如果一个没有任何输入位置的转移叫源转移，一个源转移的有效是无条件位置的转移叫源转移，一个源转移的有效是无条件的。的。2022/12/2229广东工业大学计算机学院2.转移转移t启动的结果启动的结果o若若t在在M下有效，下有效，t就可以启动。启动后将就可以启动。启动后将M变成新变成新标识标识M，记为，记为MtM或或MM，并称，并称M为为M的的后继标识。后继标识。o在定义转移在定义转移t启动的结果时，如果一个没有任何输启动的结果时，如果一个没有任何输出位置的转移叫潭转移，一个潭转移的启动将消耗出位置的转移叫潭转移，一个潭转移的启动将消耗标记，而不产生任何标记。标记，而不产
24、生任何标记。2022/12/2230广东工业大学计算机学院转移启动规则例图转移启动规则例图o图14-5 转移启动规则的Petri网2022/12/2231广东工业大学计算机学院图图14-6混惑的混惑的Petri网网2022/12/2232广东工业大学计算机学院并发与冲突并发与冲突o1）并发）并发o设设M为为Petri网网的一个标识，若存在的一个标识，若存在t1和和t2使得使得Mt1和和Mt2，并满足，并满足Mt1M1M1t2，且，且Mt2M2Mt1，则称，则称t1和和t2在在M下并发。就是说在下并发。就是说在M标识下，标识下，t1和和t2都有都有效，且它们当中任一个转移，启动都不会使另一个效，
25、且它们当中任一个转移，启动都不会使另一个转移无效。转移无效。2022/12/2233广东工业大学计算机学院o2）冲突）冲突o设设M为为Petri网网的一个标识，若存在的一个标识，若存在t1和和t2使得使得Mt1和和Mt2，并满足，并满足Mt1M1M1t2，且，且Mt2M2M2t1，则称，则称t1和和t2在在M下冲突，就是说在下冲突，就是说在M标识下，标识下，t1和和t2都有都有效，但效，但t1和和t2中只有一个能启动，而且其中任一中只有一个能启动，而且其中任一个转移启动都会使另一个转移无效。个转移启动都会使另一个转移无效。2022/12/2234广东工业大学计算机学院14.3.4行为特性行为特
26、性o1.可达性可达性o2.有界性有界性o3.活性活性o4.可逆性可逆性o5.可覆盖性可覆盖性o6.持久性持久性o7.同步距离同步距离o8.公平性公平性2022/12/2235广东工业大学计算机学院14.3.5行为特性分析方法行为特性分析方法o行为特性分析方法分为三类：行为特性分析方法分为三类：o（1）可覆盖性（可达性）树。这种方法实质上包）可覆盖性（可达性）树。这种方法实质上包含了所有可达标识或它们的可覆盖标识的枚举，适含了所有可达标识或它们的可覆盖标识的枚举，适用于所有类型的网。但由于用于所有类型的网。但由于“状态空间的爆炸状态空间的爆炸”的的问题，它只限制于规模较小的网。问题，它只限制于规
27、模较小的网。o（2）矩阵方程求解。这种方法求解能力强，但在）矩阵方程求解。这种方法求解能力强，但在许多情况下，它仅适用于许多情况下，它仅适用于Petri网的一些特殊子类网的一些特殊子类或特殊情况。或特殊情况。o（3）分层或化简。这种方法是在保证网系统要分）分层或化简。这种方法是在保证网系统要分析的性质不变的情况下进行分层或化简，它涉及一析的性质不变的情况下进行分层或化简，它涉及一些变换方法的研究，许多问题有待探索。些变换方法的研究，许多问题有待探索。2022/12/2236广东工业大学计算机学院1.不变量不变量o所谓不变量是指网系统中有所谓不变量是指网系统中有S-不变量不变量和和T-不变量不变
28、量。例例14-5：如图：如图14-7所示的是不变量的所示的是不变量的Petri网。网。o图14-7 不变量的Petri网 2022/12/2237广东工业大学计算机学院例例14-6：如图：如图14-8所示显示的是不变所示显示的是不变量的量的Petri网网图14-8 显示的是不变量的Petri网2022/12/2238广东工业大学计算机学院例例14-7：如图：如图14-9所示显示的是不变所示显示的是不变量的量的Petri网网图14-9 显示的是不变量的Petri网2022/12/2239广东工业大学计算机学院2.状态方程状态方程o如果如果N=（P，T；F）是纯网，则）是纯网，则C与与N存在一一存
29、在一一对应的关系。在此，用对应的关系。在此，用m维列向量来表示标识维列向量来表示标识M，即即M=M(p1)，M(p2），），M(pm)T。o这样，这样，MtJ的充分必要条件则为：的充分必要条件则为：oi 1，2，m：(C)TijM(i)o或写为：或写为：o(C)T*jMo其中其中(C)T*j表示矩阵表示矩阵(Cij)T的第的第j列。列。2022/12/2240广东工业大学计算机学院o如果如果M1tjM2，则有，则有M2=M1+CT*j。若。若M0M，就可以推出状态方程为：，就可以推出状态方程为：oM=M0+CTUo其中其中CTU是矩阵乘法；是矩阵乘法；是转移序列，是转移序列，U是是T-向量，向
30、量，它以它以tj为序标的分量值为为序标的分量值为tj在在中出现的次数，即中出现的次数，即U(tj)=#(tj/)；M0是是的初始标识的的初始标识的S-向量向量表示，由表示，由导出的可达标识导出的可达标识M也表示为也表示为S-向量的形向量的形式。式。2022/12/2241广东工业大学计算机学院3.关联矩阵关联矩阵o定义定义14-2：设：设=（N，M0），其中），其中N=（P，T；F）是一个纯网，即）是一个纯网，即x X：*xx*=。o其中：其中：oP=p1，p2，pmoT=t1，t2，tno（1）用）用S-元素作序标的列向量元素作序标的列向量V：PZ称为称为的的S-向量。向量。o（2）用）用T
31、-元素作序标的列向量元素作序标的列向量U：TZ称为称为的的T-向量。向量。2022/12/2242广东工业大学计算机学院o（3）用）用TP作序标的矩阵作序标的矩阵C：TPZ称为称为的的关联矩阵，其矩阵元素关联矩阵，其矩阵元素C(tj，pi)=W(tj，pi)W(pi，tj)。也可写作：。也可写作：oCjinm=C+jinmCjinmo或：或：C=C+C2022/12/2243广东工业大学计算机学院定义定义14-2o其中：其中：oC+ji就是从转移就是从转移j到它的输出位置到它的输出位置i的弧的权，的弧的权，Cji是转移的输入位置是转移的输入位置i到转移到转移j的弧的权。从转移规的弧的权。从转移
32、规则很容易可以看出，则很容易可以看出，Cji、C+ji和和Cji分别表示当分别表示当转移转移j一旦启动（发生），位置一旦启动（发生），位置i中标记取走、增加中标记取走、增加和改变的数量。和改变的数量。2022/12/2244广东工业大学计算机学院关联矩阵一般表示关联矩阵一般表示其中Cji表示取走、增加后产生的变化数。此关联矩阵给出了系统的结构。2022/12/2245广东工业大学计算机学院4.用关联矩阵和状态方程求不变量用关联矩阵和状态方程求不变量o通过网系统的关联矩阵和状态方程，就可以很方便通过网系统的关联矩阵和状态方程，就可以很方便地求出地求出S-不变量。不变量。o设设I是是的的S-不变量
33、，不变量，M M0，则：，则：oITM=ITM0o设设是从是从M0到到M的转移序列：的转移序列：M0M。于是。于是M0+CTU=M，其中，其中U是对应于是对应于的的T-向量，对向量，对所有所有tj T，U(tj)是是tj在在中出现的次数。两边同中出现的次数。两边同时乘以时乘以IT，则得：，则得：oITM0+ITCTU=ITMo因为因为I为为S-不变量，则不变量，则ITCT=(CI)T=T，是是分量全为分量全为0的的T-向量。向量。2022/12/2246广东工业大学计算机学院定义定义14-3o定义定义14-3：设：设I为系统为系统的一个的一个S-向量，向量，C是是的关联矩阵，的关联矩阵，CT是
34、是C的转置矩阵。的转置矩阵。o（1）若）若CI=，就称，就称I为为的的S-不变量。不变量。o（2）若）若I=si SI(si)0称为称为S-不变量不变量I的子集。的子集。o（3）若）若Is，就称，就称I为非负为非负S-不变量，其中不变量，其中s为分量全为为分量全为0的的S-向量。向量。2022/12/2247广东工业大学计算机学院o（4）若不存在比）若不存在比I小的非负小的非负S-不变量，即不存在不变量，即不存在非负非负S-不变量不变量I，使，使sII，就说，就说I是最小非是最小非负负S-不变量。不变量。o（5）s也称为也称为的的S-不变量。但若它是惟一的不变量。但若它是惟一的S-不变量，就说
35、不变量，就说没有没有S-不变量。不变量。2022/12/2248广东工业大学计算机学院定义定义14-4o定义定义14-4：设：设J为系统为系统的一个的一个T-向量，向量，s为为零零S-向量，则：向量，则：o（1）只要）只要CTJ=s，即在，即在S所引起的变化均为所引起的变化均为0，就说，就说J是是的的T-不变量。不变量。o（2）若）若T-不变量不变量J，就说，就说J是非负是非负T-不变量。不变量。o（3）J=tj TJ(tj)0称为称为T-不变量不变量J的子集。的子集。o（4）非负）非负T-不变量不变量J是最小的。如果不存在比是最小的。如果不存在比J更更小的非负小的非负T-不变量，即不存在非负
36、不变量，即不存在非负T-不变量不变量J，使，使J0,Cy0(或 X0，CTX0）守恒守恒 Y0，Cy=0（或X，CTX0）部分守恒部分守恒 Y0，CY=0重复重复 X0，CTX0部分重复部分重复 X0，CTX=0（或X0，CTX0一致一致 Y，CY0）部分一致部分一致 X0，CTX=02022/12/2264广东工业大学计算机学院o例例14-10：用表：用表14-2中的结论分析图中的结论分析图14-12至至14-16所示五个网的结构特性。所示五个网的结构特性。2022/12/2265广东工业大学计算机学院2022/12/2266广东工业大学计算机学院2022/12/2267广东工业大学计算机学
37、院2022/12/2268广东工业大学计算机学院2022/12/2269广东工业大学计算机学院表表14-3用表用表14-2中结论对图中结论对图14-12至图至图14-16的分析结果的分析结果图图14-12图图14-13图图14-14图图14-15图图14-16结构有界结构有界守恒守恒部分守恒部分守恒重复重复部分重复部分重复一致一致部分一致部分一致2022/12/2270广东工业大学计算机学院14.3.7Petri网到程序结构的转换网到程序结构的转换从从Petri网的概念与分析方法可以知道，网的概念与分析方法可以知道，Petri网网是用来描述和分析要开发系统模型的工具，不是计是用来描述和分析要开
38、发系统模型的工具，不是计算机的实现应用工具。另一方面，算机的实现应用工具。另一方面，Petri网的结构网的结构与软件结构的性质也不同。其表现形式也不同。由与软件结构的性质也不同。其表现形式也不同。由此可以得出：通过分析，有了此可以得出：通过分析，有了Petri网结构。要实网结构。要实现从现从Petri网结构到程序结构的转换，必须在网结构到程序结构的转换，必须在Petri网与程序结构之间建立恰当的联系或对应关网与程序结构之间建立恰当的联系或对应关系，这样才能实现从系，这样才能实现从Petri网到程序结构的转换。网到程序结构的转换。2022/12/2271广东工业大学计算机学院1.流程图方法流程图
39、方法图图14-17 14-17 流程图与流程图与PetriPetri网互换网互换 图图14-1814-18 流程图与流程图与PetriPetri网互换网互换 2022/12/2272广东工业大学计算机学院oPetri网转移为等价的流程图网转移为等价的流程图2022/12/2273广东工业大学计算机学院o动作：动作：oaInput（y1）:Input（y2）;y3=1oby10?ocodd（y1）?ody3:=y3*y2;y1:=y1-1;oey2:=y2*y2;y1:=y1/2;ofutput（y3）2022/12/2274广东工业大学计算机学院2.编程语言的方法编程语言的方法o除了流程图与除
40、了流程图与Petri网互相转换的方法外，也可以网互相转换的方法外，也可以用编程语言转换。但是编程语言（如用编程语言转换。但是编程语言（如Ada、C+等）必须选用具有并发机制。用具有并发机制编程等）必须选用具有并发机制。用具有并发机制编程语言与语言与Petri网两者之间建立起恰当的联系，这样网两者之间建立起恰当的联系，这样就可以实现从就可以实现从Petri网到编程语言的转换。网到编程语言的转换。2022/12/2275广东工业大学计算机学院o采用的是改进的谓词采用的是改进的谓词/转移网（转移网（Mprt），它是谓词），它是谓词/转移网（转移网（prt）的一种受限形式。）的一种受限形式。Mprt网
41、与网与prt网的主要区别是网的主要区别是Mprt网中的位置只能具有一种类网中的位置只能具有一种类型的标记。这样，把位置中的标记表示进程实例，型的标记。这样，把位置中的标记表示进程实例，不同的标记代表了不同的进程实例。标记的流动，不同的标记代表了不同的进程实例。标记的流动，反映了进程的执行情况，进程在转移处交互，当转反映了进程的执行情况，进程在转移处交互，当转移启动时交换信息，完成进程间的同步移启动时交换信息，完成进程间的同步2022/12/2276广东工业大学计算机学院3.面向对象的程序设计方法面向对象的程序设计方法o这里的关键问题是把这里的关键问题是把Petri网引入面向对象程序设网引入面向
42、对象程序设计，必须解决有关对象的表示，对象间的通信机制计，必须解决有关对象的表示，对象间的通信机制和模型的验证等方面的问题。下面介绍对象和模型的验证等方面的问题。下面介绍对象Petri网（网（OPN）结构。）结构。oOPN由内部结构和接口两部分组成。由内部结构和接口两部分组成。o1）OPN的内部结构的内部结构o（1）标记。）标记。o（2）转移。）转移。o（3）禁止弧。）禁止弧。o2）OPN的接口的接口2022/12/2277广东工业大学计算机学院小结小结o本章介绍了形式化方法的基本原理与应用知识。形式化方法本章介绍了形式化方法的基本原理与应用知识。形式化方法提供了规约环境的基础，它使得所生成的
43、分析模型比用传提供了规约环境的基础，它使得所生成的分析模型比用传统的或面向对象的方法生成的模型更完整、一致和无二义。统的或面向对象的方法生成的模型更完整、一致和无二义。集合论和逻辑符号的描述设施使得软件工程师能创建清晰集合论和逻辑符号的描述设施使得软件工程师能创建清晰的关于事实的陈述。的关于事实的陈述。o使用形式化方法的决策必须考虑启动成本以及不同的技术相使用形式化方法的决策必须考虑启动成本以及不同的技术相关的文化变更。在大多数情况下，形式化方法对安全关键关的文化变更。在大多数情况下，形式化方法对安全关键和业务关键的系统具有最高的回报。和业务关键的系统具有最高的回报。o近几年来，由于软件开发中的并行问题和不确定性问题，把近几年来，由于软件开发中的并行问题和不确定性问题，把Petri网作为解决并发问题的工具被大家接受。对于具有并网作为解决并发问题的工具被大家接受。对于具有并发、异步、分布、并行、不确定性或随机性的信息处理系发、异步、分布、并行、不确定性或随机性的信息处理系统，都可以利用统，都可以利用Petri网方法构造出要开发的网方法构造出要开发的Petri网模型。网模型。2022/12/2278广东工业大学计算机学院谢谢谢谢2022/12/2279广东工业大学计算机学院