《软件工程第14章：形式化方法》由会员分享，可在线阅读，更多相关《软件工程第14章：形式化方法（79页珍藏版）》请在金锄头文库上搜索。
1、2018/9/11,广东工业大学计算机学院,1,软件工程 Software Engineering,2018/9/11,广东工业大学计算机学院,2,第14章 形式化方法,形式化方法提供了规约环境的基础，它使得所生成的分析模型比用传统的或面向对象的方法生成的模型更完整、一致和无二义性。 本章内容： 14.1 基础知识 14.2 有限状态机（FSM） 14.3 PETRI网基本原理,2018/9/11,广东工业大学计算机学院,3,14.1基础知识,形式化方法的定义： 定义14.1：用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术。这样的形式化方法提供了一个框架，人们可以在框架中以系统的
2、方式刻画、开发和验证系统。 形式化规约的目标：无二义性、一致性和完整性。注：使用形式化方法，完整性是难以达到的。,2018/9/11,广东工业大学计算机学院,4,14.1.1 形式化方法概念,例14-1：符号表：它由一组没有重复的项构成。如图14-1所示。程序被用于维护一个符号表，在许多不同类型的应用中使用此符号表。图14-1 符号表,2018/9/11,广东工业大学计算机学院,5,例14-1,如果对于上表有一个陈述：包括不多于MaxIds的用户名，那么就为表设定了一个限制，这就称为数据不变式的条件的一个构成成分。数据不变式是一个条件，它在包含一组数据的系统的执行过程中总保持为真。上面讨论的符
3、号表的数据不变式有两个构成成分： （1）表中包含的名字数不超过MaxIds。 （2）在表中没有重复的名字。在上面描述的符号表程序的情形下，这意味系统执行过程中无论什么时候检查符号表，它将总是包含不超过MaxIds的职员标识符，并且没有重复。,2018/9/11,广东工业大学计算机学院,6,形式化方法概念,状态的概念，在形式化方法的语言环境中，状态是系统访问和修改的存储数据。在上述符号表程序的例子中，状态是符号表。 操作的概念，这是在系统中发生的读或写状态数据的动作。如果对符号表程序考虑从符号表加入或移出职员名，则它将关联两个操作：一个是加一个指定名到符号表中的操作，另一个是从表中移出一个现存名
4、的操作。如果程序提供检查某指定名是否包含在表中的机制，则有一个返回某种表示名字是否在表中的指示值的操作。,2018/9/11,广东工业大学计算机学院,7,一个操作和两个条件相关联：前置条件和后置条件。前置条件定义某特定操作在其中合法的环境。操作的后置条件定义当操作完成后所产生的现象，是通过其对状态的影响来定义的。在加标识符到职员标识符符号表的操作的例子中，后置条件已经将数学的刻画表增加了新标识符。,2018/9/11,广东工业大学计算机学院,8,14.1.2 形式化规约语言,形式化规约语言通常由三个主要的成分构成： （1）语法，定义用于表示规约的特定符号。 （2）语义，帮助定义用于描述系统的“
5、对象的全域（universe of objects）”。 （3）一组关系，定义确定出哪个对象真正满足规约的规则。,2018/9/11,广东工业大学计算机学院,9,Z的符号的缩略集合：,集合： SP X S被声明为X的集合。 xS x是S中的成员。 xS x不是S中的成员。 ST S是T的子集：S中每个元素均在T中。 ST S和T的并：包含在S或T或两者中的每个元素。 ST S和T的交：包含同时在S和T中的元素。,2018/9/11,广东工业大学计算机学院,10,ST S和T的差：包含在S中的而不在T中的每个元素。空集：不包含任何成员。 x 单元素集：仅仅包含x元素。 N 自然数集合：0，1，2
6、， SF X S被声明为X的有限集。 Max(S) 数的非空集合S中的最大元素。,2018/9/11,广东工业大学计算机学院,11,功能： fxy f被声明为从x到y的部分内射。 dom f f的定义域:f(x)有定义的值x的集合 ran f f的值域: x在f的定义域上变化而形成的 f(x)值的集合。 fxy 一个和f相同的函数，除了x被映射到y(x)值的集合。 x f 一个和f相似的函数，除了x被从定义域中去除。,2018/9/11,广东工业大学计算机学院,12,逻辑： PQ P与Q同时为真时才为真。 PQ P蕴含Q：或者Q为真或者P为假时为真。 S=S 在操作中schema S中没有成分
7、改变。,2018/9/11,广东工业大学计算机学院,13,例14-2,例14-2：下面用Z语言schema的例子描述了块处理器的状态和数据不变式：,2018/9/11,广东工业大学计算机学院,14,14.2 有限状态机（FSM）,很多实时系统，特别是实时控制系统，其整个分析机制与系统的状态有相当大的关系。有限状态机由有限的状态和相互之间的转移构成，在任何时候只能是给定数目的状态中的一个。 主要有两种方法来建立有限状态机，一种是“状态转移图”，另一种是“状态转移表”，分别用图形方式和表格方式建立有限状态机。,2018/9/11,广东工业大学计算机学院,15,有限状态机的组成如下：,（1）一个有限
8、的状态集合Q。 （2）一个有限的输入集合I。 （3）一个变迁函数：QIQ变迁函数也是一个状态函数，在某一状态下，给定输入后，FSM转入该函数产生的新状态。的定义域内的某些数值可以是未定义的。,2018/9/11,广东工业大学计算机学院,16,简单有限状态机,图14-2中的左图表明该FSM有q0、q1、q2、q3四个状态，输入集中有a、b、c、四个元素；右图中各个状态之间的转换关系则更清晰。有限状态机非常适合于描述这样的系统：系统含有有限个状态，不同事件的发生可以用不同状态之间的转换来模拟。,2018/9/11,广东工业大学计算机学院,17,有限状态机的特点,有限状态机的优点在于简单易用，状态间
9、的关系能够直观看到。 但应用在实时系统中时，其最大的缺点是：任何时刻系统只能有一个状态，无法表示并发性，不能描述异步并发的系统。另外，在系统部件较多时，状态数随之增加，导致复杂性显著增长。,2018/9/11,广东工业大学计算机学院,18,14.3 Petri网基本原理,Petri网在软件分析中，是一种系统的数学和图形的描述与分析的方法。对于具有并发、异步、分布、并行、不确定性或随机性的信息处理系统，都可以利用Petri网构造出要开发的Petri网模型。这种模型可以表示系统结构和动态行为方面的信息。,2018/9/11,广东工业大学计算机学院,19,由于Petri网的表示方法是用图形工具。因此
10、其表示形式与传统方法的结构图、流程图具有同样的直观、形象效果。其特别之处在于可以使用标记模拟系统的动态行为和并发活动。另一方面，作为一种数学工具，便于计算和验证系统的数学方程。它可以建立状态方程、代数方程以及系统行为的其他数学模型。因此，系统开发人员和理论研究工作者都可以根据需要利用Petri网。,2018/9/11,广东工业大学计算机学院,20,14.3.1 静态结构,Petri网的基本成分可以表示为一个三元组：N =（P，T；F） 并满足以下条件：（1）PT。（2）PT=。（3）F（PT）（TP）。（4）DOM（F）COD（F）= PT。,2018/9/11,广东工业大学计算机学院,21,
11、其中：P=p1，p2，pn 是N的有穷位置集合。T=t1，t2，tn 是N的有穷转移集合。F是由N中一个P元素和一个T元素组成的有序偶的集合。DOM（F）= x y：（y，x）F，COD（F）= x y：（x，y）F。如果用圆圈表示位置，用矩形框表示转移，用有向边表示位置与转移的有序偶，那么就构成了Petri网的图形表示。,2018/9/11,广东工业大学计算机学院,22,例14-3:N的Petri网,例14-3：N的Petri网N=（P，T；F）P= p1，p2，p3，p4，p5，p6T= t1，t2，t3，t4，t5，t6F= (p1，t1)，(t1，p2)，(p2，t2)，(t2，p1)
12、，(p1, t3)，(t3，p3)，(t3，p4)，(p3，t4)，(p4，t5)，(t4，p5)，(t5，p6)，(p5，t6)，(p6，t6) N的Petri网图形表示，如图14-3所示。,2018/9/11,广东工业大学计算机学院,23,图14-3 N的Petri网的图形表示,2018/9/11,广东工业大学计算机学院,24,14.3.2 动态特征,具有动态特征的Petri网就可以表示为六元组：=（P，T；F，K，W，M0） 其中：（P，T；F）的含义与前面静态结构中的含义相同。 K：PN+w，是位置上容量函数，N+=1，2，3，；若K(p)= w，表示位置p的容量为无穷。 W：FN+，
13、是弧集合上的权函数。 M：PN0，是Petri网的标识（marking），M0为初始标识，N0=0，1，2，3，pP，必须满足M（p）K（p）。,2018/9/11,广东工业大学计算机学院,25,在Petri网的图形表示中，弧（x，y）上的W值标在弧（x，y）上，M(p)的值不是用数字，而是用实心点表示，即在位置P对应的圆圈中标注M(p)个实心点，每个实心点称为一个标记（token）。同一位置中的诸多标记代表同一类完全等价的个体。,2018/9/11,广东工业大学计算机学院,26,例14-4：具有M0和W的Petri网可以表示为如图14-4所示。,图14-4 具有M0和W的Petri网,201
14、8/9/11,广东工业大学计算机学院,27,对于图14-4所示的Petri网： M0=（1，0，0，0，0，0） W（t2，p1）= W（t5，p6）= W（t6，p1）= 4 W（t3，p3）= 6 W（t4，p5）= 5 W（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）= 1,2018/9/11,广东工业大学计算机学院,28,14.3.3 转移启动规则,前面介绍的Petri网的动态特征是Petri网的动态行为的特性描述。这种动态行为是通过转移启动引起标识改变的变化
15、来体现的。而转移启动则要有可以启动转移（转移有效）的条件和启动规则。,2018/9/11,广东工业大学计算机学院,29,1. 转移t有效的条件,若在标识M下，p1，p1*t M（p1）W（p1，t），且： p2，p2t* M（p2） W（t，p2）K（p2） 此时称t在M下有效，记为M t。 在定义转移有效的条件时，如果一个没有任何输入位置的转移叫源转移，一个源转移的有效是无条件的。,2018/9/11,广东工业大学计算机学院,30,2. 转移t启动的结果,若t在M下有效，t就可以启动。启动后将M变成新标识M，记为M tM或M M，并称M为M的后继标识。在定义转移t启动的结果时，如果一个没有任何输出位置的转移叫潭转移，一个潭转移的启动将消耗标记，而不产生任何标记。,2018/9/11,广东工业大学计算机学院,31,转移启动规则例图,图14-5 转移启动规则的Petri网,2018/9/11,广东工业大学计算机学院,32,图14-6混惑的Petri网,2018/9/11,广东工业大学计算机学院,33,并发与冲突,1）并发 设M为Petri网的一个标识，若存在t1和t2使得M t1和M t2，并满足M t1M1 M1t2，且M t2M2 M t1，则称t1和t2在M下并发。就是说在M标识下，t1和t2都有效，且它们当中任一个转移，启动都不会使另一个转移无效。,
