高级软件工程(第5章：形式化开发方法_1)课件

《高级软件工程(第5章：形式化开发方法_1)课件》由会员分享，可在线阅读，更多相关《高级软件工程(第5章：形式化开发方法_1)课件（35页珍藏版）》请在金锄头文库上搜索。

1、第5章 形式化开发方法,形式化方法：是建立在严格数学基础上，具有精确数学 表达形式和语义的开发方法。 其中：形式化方法的基本含义是借助数学的方法来研究软 件工程中的有关问题。 特点： 1. 可以用数学方法进行验证。如代数方法； 2. 可以用算法进行识别和变换。 例如： 形式语言（BNF）、有限自动机（FA）等是形式化方法 描述算法的程序流程图、类pascal、类C等算法描述语言 则是非形式化方法。,形式化方法分类 1. 根据说明目标软件系统的方式，可以分为两类： 1) 面向模型的形式化方法 通过构造一个数学模型来说明系统的行为。 2) 面向属性的形式化方法 通过描述目标软件系统的各种属性来间接

2、定义系统行为。 2. 根据表达能力，可以分为五类： 1) 基于模型的方法 给出系统状态和状态变换操作的显式但亦是抽象的定义，即通 过定义系统状态和操作建立系统模型。但对于并发没有显式的表 示。 如：Z语言，VDM，B方法等。 2) 基于逻辑的方法 用逻辑描述系统预期的性能，包括底层规约、时序和可能性行 为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。 用具体的编程构造扩充逻辑从而得到一种广谱形式化方法，通过 保持正确性的细化步骤集来开发系统。 如： ITL (区间时序逻辑), TAM (时序代理模型)，RTTL (实时时序逻辑)等,3) 代数方法 通过联系不同操作间的行为关系而给出操作

3、的显式定 义，而不定义状态，同样它亦未给出并发的显式表示. 如：OBJ，Clear，Larch族代数规约语言等 4) 进程代数方法 给出并发过程的一个显式模型，并通过进程间允许的可观察的通讯上的限制（约束）来表示行为. 如：CSP（通信顺序过程） ACP（通信过程代数） CCS（通信并发系统/通信系统演算 ）等 5) 基于网络的方法 该方法采用具有形式语义的图形语言，根据网络中的 数据流显式地给出系统的行为模型，包括数据在网中从 一个结点流向另一个结点的条件、并发行等。 如：Petri 网、谓词变换网,Petri网的提出： 1962年由德国人C.A.Petri在他的博士 论文：“用自动机通讯”

4、 (Communication with automata) 中首次提出的“网状结构的信息模型” 其中“有限自动机Finite automata”定义为： FAA=（S，S0，F） 其中：S-状态集 -字母表 -SS的映射 S0-开始状态/状态集 F-终止状态集 FAA可用三种方式描述： 集合法：定义方法； 矩阵法：状态转换矩阵/表 状态图法：状态转换图,5. 1 Petri网概述,例子： 一个保险箱上装了一把复合锁，锁有三个位置，分别 标记为1、2、3，转盘可向左（L）或向右（R）转动。 这样，在任意时刻转盘都有6种可能的运动如下： L1、R1、L2、R2、L3、R3 保险箱的组合密码是：

5、L1、R3、L2 转盘的任何其他运动都将引起报警。,1,2,3,则保险箱拨动密码的状态转换情况如DFA的状态转换图所示：,其中：初态 S：保险箱锁定 终态 T：保险箱解锁 终态 E：报警 符号 ：转盘的任何其他移动,保险箱DFA的状态转换表：,其优点：1. 简洁、直观 2. 严谨、无二义性 3. 可以从代数角度进行进一步的分析,如上述DFA可以转换成如下代数方程组进一步进行分析讨论 x = L1y y = R3z z = L3 解该线性方程组得：L1R3L3,说明： 1. Petri网是利用FA的状态图发展起来的网系统 2Petri网是一种系统的数学和图形的描述和分析工具,（密码）,Petri

6、网的特点： 1. 作为一种图形工具，直观形象，便于使用 注：同软件设计中的状态图、结构图、程序流程图类 似，直观形象，便于使用； 如：用Petri网可直观描述具有并发、并行、异步、分 布、不确定性和随机的信息处理系统，即模拟系 统的动态性和并发性。 2. 作为一种数学工具，便于计算和验证 如：它可以建立状态方程、代数方程以及系统行为的 其他数学模型，便于计算和验证； 3. 作为一种理论与实际工作的中介（桥梁），相互借鉴 如： 实际工作者可以从中学到如何使他们的建模条理化 理论工作者可以从中学到如何使他们的建模更实用化,5. 2 Petri网的定义及基本原理,一、Petri网的静态结构（或称具有

7、静态特征的Petri网） Petri网 N=（P，T；F），并满足以下条件： (1) PT (2) PT (3) F （PT）（TP） /双向映射关系 (4) DOM(F)COD(F)=PT /表明PT中的元素 / 在N中均被使用到 其中: P=p1,p2,pn 是N的有穷位置集合(表示状态的元素) T=t1,t2,tn 是N的有穷转移集合(表示状态变化的元素) F是由一个P元素和一个T元素组成的二元组的集合 DOM(F)= x |y:(y , x)F /代表F的后集;存在量词 COD(F)= x |y:(x , y)F /代表F的前集； 注：位置(Place)有人译为“库所”，转移(Tran

8、sition)译成“变迁”,例1：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) , ( t1 , p1) , ( p1 , t3) , ( t3 , p3) , ( t3 , p4) , ( p3 , t4) , ( p4 , t5) , ( t4 , p5) , ( t5 , p6) , ( p5 , t6) , ( p6 , t6) 其中： DOM(F)=t1, p2, t2, p1, t3, p3, p4, t4, t5, p5, p6,

9、 t6 COD(F)= )=p1, t1, p2, t3, p3, p4, t4, t5, p5, p6 显然 DOM(F)COD(F)=PT =p1, p2, p3, p4 p5, p6, t1, t2, t3, t4, t5, t6 注：此为关系集合表示法,Petri网的图形表示： 1用圆形 表示位置(库所)p: 作用是决定转移能否发生 2用矩形 表示转移(变迁)t: 作用是改变位置的状态 3用有向弧表示位置与转移的有序偶 例如上述Petri网N的图形表示:,位置或转移的前集和后集定义： 设XPT , 令 *x = y | (y , x)F /前集（亦称x的输入集） x*= y | (x

10、, y)F /后集（亦称x的输出集） 说明：定义两个特殊的Petri网 1. 纯网：如果对所有xPT ，都有 *xx* 注：表明x无自循环（仅通过一个结点的循环） 2. 简单网：如果对所有x，yPT ,，都有 (*x=*y)(x*=y*)( x=y) 即：不存在两个不同的结点，它们的前集和后集相同。 例如：上例是纯网且是简单网,非纯网例：,其中： *t1= p1 t1*=p1，p2 *t1t1*= p1 p1，p2= p1 ,其中： * p2 =t1 p2*=t1 *p2p2*= t1 t1= t1 ,其中： *t1= p1 ， *t2=p1 ，t1*= p2 ， t2*=p2 然而 t1t2

11、,非简单网例：,二、Petri网的动态特征 具有动态特征的Petri网是一个六元组： =（P，T；F，K，W，M0） 其中：（P，T；F）同前 K: PN+，是位置上的容量函数，表示一个位置 的总容量 N+=1，2，3， = ：即，若K(P)=，表示位置的容量为无穷 W: FN+，是弧集合上的权函数 M: PN0，是的标识（Marking），M0为初始标识 N0=0，1，2，3， pP M(p)K(p) 其中：M(p): 表示当前位置p的实际存储数量。,说明：在Petri网的图形表示中 1W（x , y）= i 标在弧（x , y）上，即：,其中：i=1 可省略,如：,2M(p)= i 用在位

12、置p对应的圆形中标注i个实心点标记,其中： 1) 实心点“”称作标记（Token） 2) 同一位置中的诸多标记代表同一类完全等价的个体 如：其中一个标记代表人，则其他标记也代表人,3K(p)标记在位置p的圆形外面，如K(p)=10 则有：,其中：K(p)=时省略不标,例：设有Petri网,则有：M0=(1，0，0，0，0，0) W(t2 , p1)= W(t5 , p6)= W(t6 , p1)=2 W(t3 , p3)=4 W(t4 , p5)=3 W(p1 , t1)=W(t1 , p2)=W(p2 , t2)=W(p1, t3)=W(t3 , p4) = W(p4 , t5)= W(p3

13、 , t4)= W(p5 , t6)= W(p6 , t6)=1 p: K(P)=,3转移发生规则 Petri网的动态行为: 是通过转移t发生引起标识M改变来 体现的，下面是转移可发生的条件: （1）转移 t 可发生的条件 若在标识M下，p1，p1*t=M(p1)W(p1，t)， 且p2，p2t*= M(p2) +W(t，p2) K(p2)， 此时称 t 在M下可发生，记为M t 例如: 可发生例：,其中：M(p1)=1 M(p2)=0 W(p1，t)=1 W(t，p2)=1 K(p2)=1 则有：M(p1)=1W(p1，t)=1 且M(p2)+W(t，p2)=0+1=1K(p2)=1,不可发

14、生例：,条件1不成立：,条件2不成立：,2,(2)转移t发生的结果 若Mt，t就可以发生，发生后将M变成新标识M， 记为MtM，(或MM)，并称M为M的后继标 识。对pP均进行如下操作：,t,例：（关于转移t发生的结果）,a.,则：M=M0=(1，0，0) Mt1M M(p1)=M(p1)-W(p1,t1)+W(t1,p1) p1t1*t1 M=(1, 1, 0) M(p2)= M(p2)+W(t1，p2) p2t1* M(p3)= M(p3),b.,c.,说明： 1. 一个没有任何输入位置的转移叫做源转移，一个源转移的发生是无条件的且它的发生只会产生标记，而不消耗任何标记。,2一个没有任何输

15、出位置的转移叫做潭转移，一个潭转 移的发生将消耗标记，而不产生任何标记。,利用下例Petri网进一步讨论,在该Petri网中，初始标记为： M0=(1，0，0，0，0，0) 1由转移t发生条件，这时有 M0t1和M0t3 2转移t发生的结果和现象 冲突(Conflict)： 由于M0t1且M0t3，表明t1和t3同时可以发生，而 M0(p1)=1，即t1和t3共享一个“资源”，则t1和t3不能同时发 生，网论中称这种情况为“冲突”。,网论解决冲突的办法可以是：通过环境对系统进行控制 其中：环境：指具体情况。 控制：指给出一定的条件和限制。 如：启动次数（权1）+ 优先级（权2） 令：t1的优先级t3的优先级 且 t1发生次数t3发生 次数，则此时：M0t1 但M0t3 t1发生有：M0t1M1=(0，1，0，0，0，0) M1t2M0=(1，0，0，0，0，0) 此时M0t1且M0t3 但t1发生次数t3发生次数，则 M0t3 但 M0t1 t3发生有：M0t3M2=(0，0，1，1，0，0) 这时出现（产生）并发：,并发(Concurrent) M2(p3)=1和M2(p4)=1两件事同时出现，此时t4和t5同时可以发