《软件工程课件 SE14》由会员分享，可在线阅读，更多相关《软件工程课件 SE14（79页珍藏版）》请在金锄头文库上搜索。
1、软件工程Software EngineeringDate1广东工业大学计算机学院第14章形式化方法o形式化方法提供了规约环境的基础，它使得所生成的分析模型比用传统的或面向对象的方法生成的模型更完整、一致和无二义性。o本章内容：o14.1基础知识o14.2有限状态机（FSM）o14.3PETRI网基本原理Date2广东工业大学计算机学院14.1基础知识o形式化方法的定义：o定义14.1：用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术。这样的形式化方法提供了一个框架，人们可以在框架中以系统的方式刻画、开发和验证系统。o形式化规约的目标：无二义性、一致性和完整性。o注：使用形式化方法，
2、完整性是难以达到的。Date3广东工业大学计算机学院14.1.1形式化方法概念o例14-1：符号表：它由一组没有重复的项构成。如图14-1所示。程序被用于维护一个符号表，在许多不同类型的应用中使用此符号表。oo图14-1符号表Date4广东工业大学计算机学院例14-1o如果对于上表有一个陈述：包括不多于MaxIds的用户名，那么就为表设定了一个限制，这就称为数据不变式的条件的一个构成成分。数据不变式是一个条件，它在包含一组数据的系统的执行过程中总保持为真。上面讨论的符号表的数据不变式有两个构成成分：o（1）表中包含的名字数不超过MaxIds。o（2）在表中没有重复的名字。在上面描述的符号表程序
3、的情形下，这意味系统执行过程中无论什么时候检查符号表，它将总是包含不超过MaxIds的职员标识符，并且没有重复。Date5广东工业大学计算机学院形式化方法概念o状态的概念，在形式化方法的语言环境中，状态是系统访问和修改的存储数据。在上述符号表程序的例子中，状态是符号表。o操作的概念，这是在系统中发生的读或写状态数据的动作。如果对符号表程序考虑从符号表加入或移出职员名，则它将关联两个操作：一个是加一个指定名到符号表中的操作，另一个是从表中移出一个现存名的操作。如果程序提供检查某指定名是否包含在表中的机制，则有一个返回某种表示名字是否在表中的指示值的操作。Date6广东工业大学计算机学院o一个操作
4、和两个条件相关联：前置条件和后置条件。前置条件定义某特定操作在其中合法的环境。操作的后置条件定义当操作完成后所产生的现象，是通过其对状态的影响来定义的。在加标识符到职员标识符符号表的操作的例子中，后置条件已经将数学的刻画表增加了新标识符。Date7广东工业大学计算机学院14.1.2形式化规约语言o形式化规约语言通常由三个主要的成分构成：o（1）语法，定义用于表示规约的特定符号。o（2）语义，帮助定义用于描述系统的“对象的全域（universeofobjects）”。o（3）一组关系，定义确定出哪个对象真正满足规约的规则。Date8广东工业大学计算机学院Z的符号的缩略集合：o集合：oSPXS被声
5、明为X的集合。oxSx是S中的成员。oxS x不是S中的成员。oST S是T的子集：S中每个元素均在T中。oSTS和T的并：包含在S或T或两者中的每个元素。oSTS和T的交：包含同时在S和T中的元素。Date9广东工业大学计算机学院oSTS和T的差：包含在S中的而不在T中的每个元素。o空集：不包含任何成员。ox单元素集：仅仅包含x元素。oN自然数集合：0，1，2，oSFXS被声明为X的有限集。oMax(S)数的非空集合S中的最大元素。Date10广东工业大学计算机学院o功能：ofxyf被声明为从x到y的部分内射。odomff的定义域:f(x)有定义的值x的集合oranff的值域:x在f的定义域
6、上变化而形成的f(x)值的集合。ofxy一个和f相同的函数，除了x被映射到y(x)值的集合。oxf一个和f相似的函数，除了x被从定义域中去除。Date11广东工业大学计算机学院o逻辑：oPQP与Q同时为真时才为真。oPQP蕴含Q：或者Q为真或者P为假时为真。oS=S在操作中schemaS中没有成分改变。Date12广东工业大学计算机学院例14-2o例14-2：下面用Z语言schema的例子描述了块处理器的状态和数据不变式：Date13广东工业大学计算机学院14.2有限状态机（FSM）o很多实时系统，特别是实时控制系统，其整个分析机制与系统的状态有相当大的关系。有限状态机由有限的状态和相互之间的
7、转移构成，在任何时候只能是给定数目的状态中的一个。o主要有两种方法来建立有限状态机，一种是“状态转移图”，另一种是“状态转移表”，分别用图形方式和表格方式建立有限状态机。Date14广东工业大学计算机学院有限状态机的组成如下：o（1）一个有限的状态集合Q。o（2）一个有限的输入集合I。o（3）一个变迁函数：QIQ变迁函数也是一个状态函数，在某一状态下，给定输入后，FSM转入该函数产生的新状态。的定义域内的某些数值可以是未定义的。Date15广东工业大学计算机学院简单有限状态机简单有限状态机图14-2中的左图表明该FSM有q0、q1、q2、q3四个状态，输入集中有a、b、c、四个元素；右图中各个
8、状态之间的转换关系则更清晰。有限状态机非常适合于描述这样的系统：系统含有有限个状态，不同事件的发生可以用不同状态之间的转换来模拟。Date16广东工业大学计算机学院有限状态机的特点o有限状态机的优点在于简单易用，状态间的关系能够直观看到。o但应用在实时系统中时，其最大的缺点是：任何时刻系统只能有一个状态，无法表示并发性，不能描述异步并发的系统。另外，在系统部件较多时，状态数随之增加，导致复杂性显著增长。Date17广东工业大学计算机学院14.3Petri网基本原理oPetri网在软件分析中，是一种系统的数学和图形的描述与分析的方法。对于具有并发、异步、分布、并行、不确定性或随机性的信息处理系统
9、，都可以利用Petri网构造出要开发的Petri网模型。这种模型可以表示系统结构和动态行为方面的信息。Date18广东工业大学计算机学院o由于Petri网的表示方法是用图形工具。因此其表示形式与传统方法的结构图、流程图具有同样的直观、形象效果。其特别之处在于可以使用标记模拟系统的动态行为和并发活动。另一方面，作为一种数学工具，便于计算和验证系统的数学方程。它可以建立状态方程、代数方程以及系统行为的其他数学模型。因此，系统开发人员和理论研究工作者都可以根据需要利用Petri网。Date19广东工业大学计算机学院14.3.1静态结构oPetri网的基本成分可以表示为一个三元组：N=（P，T；F）o
10、并满足以下条件：（1）PT。（2）PT=。（3）F（PT）（TP）。（4）DOM（F）COD（F）=PT。Date20广东工业大学计算机学院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网的图形表示。Date21广东工业大学计算机学院例14-3:N的Petri网o例14-3：N的Petri网N=（P，T；F） P= p1，p2，p3，p4，p5
11、，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所示。Date22广东工业大学计算机学院图14-3 N的Petri网的图形表示Date23广东工业大学计算机学院14.3.2动态特征o具有动态特征的Petri网就可以表示为六元组：=（P，T；F，K，W，M0）o其中：（P，T；F）的含义与前面静态结构中的含义相同。oK：PN+w，是位置上容量函
12、数，N+=1，2，3，；若K(p)=w，表示位置p的容量为无穷。oW：FN+，是弧集合上的权函数。oM：PN0，是Petri网的标识（marking），M0为初始标识，N0=0，1，2，3，pP，必须满足M（p）K（p）。Date24广东工业大学计算机学院o在Petri网的图形表示中，弧（x，y）上的W值标在弧（x，y）上，M(p)的值不是用数字，而是用实心点表示，即在位置P对应的圆圈中标注M(p)个实心点，每个实心点称为一个标记（token）。同一位置中的诸多标记代表同一类完全等价的个体。Date25广东工业大学计算机学院例14-4：具有M0和W的Petri网可以表示为如图14-4所示。图1
13、4-4 具有M0和W的Petri网 Date26广东工业大学计算机学院对于图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）=1Date27广东工业大学计算机学院14.3.3转移启动规则o前面介绍的Petri网的动态特征是Petri网的动态行为的特性描述。这种动态行为是通过转移启动引起标识改变的变化来体现的。而转移启动则要有可以启
14、动转移（转移有效）的条件和启动规则。Date28广东工业大学计算机学院1.转移t有效的条件o若在标识M下，p1，p1*tM（p1）W（p1，t），且：op2，p2t*M（p2）W（t，p2）K（p2）o此时称t在M下有效，记为Mt。o在定义转移有效的条件时，如果一个没有任何输入位置的转移叫源转移，一个源转移的有效是无条件的。Date29广东工业大学计算机学院2.转移t启动的结果o若t在M下有效，t就可以启动。启动后将M变成新标识M，记为MtM或MM，并称M为M的后继标识。o在定义转移t启动的结果时，如果一个没有任何输出位置的转移叫潭转移，一个潭转移的启动将消耗标记，而不产生任何标记。Date3
15、0广东工业大学计算机学院转移启动规则例图o图14-5 转移启动规则的Petri网Date31广东工业大学计算机学院图14-6混惑的Petri网Date32广东工业大学计算机学院并发与冲突o1）并发o设M为Petri网的一个标识，若存在t1和t2使得Mt1和Mt2，并满足Mt1M1M1t2，且Mt2M2Mt1，则称t1和t2在M下并发。就是说在M标识下，t1和t2都有效，且它们当中任一个转移，启动都不会使另一个转移无效。Date33广东工业大学计算机学院o2）冲突o设M为Petri网的一个标识，若存在t1和t2使得Mt1和Mt2，并满足Mt1M1M1t2，且Mt2M2M2t1，则称t1和t2在M
16、下冲突，就是说在M标识下，t1和t2都有效，但t1和t2中只有一个能启动，而且其中任一个转移启动都会使另一个转移无效。Date34广东工业大学计算机学院14.3.4行为特性o1.可达性o2.有界性o3.活性o4.可逆性o5.可覆盖性o6.持久性o7.同步距离o8.公平性Date35广东工业大学计算机学院14.3.5行为特性分析方法o行为特性分析方法分为三类：o（1）可覆盖性（可达性）树。这种方法实质上包含了所有可达标识或它们的可覆盖标识的枚举，适用于所有类型的网。但由于“状态空间的爆炸”的问题，它只限制于规模较小的网。o（2）矩阵方程求解。这种方法求解能力强，但在许多情况下，它仅适用于Petri网的一些特殊子类或特殊情况。o（3）分层或化简。这种方法是在保证网系统要分析的性质不变的情况下进行分层或化简，它涉及一些变换方法的研究，许多问题有待探索。Date36广东工业大学计算机学院1.不变量o所谓不变量是指网系统中有S-不变量和T-不变量。例14-5：如图14-7所示的是不变量的Petri网。o图14-7 不变量的Petri网 Date37广东工业大学计算机学院例14-6：如图14-8所
