显式状态迁移模型

《显式状态迁移模型》由会员分享，可在线阅读，更多相关《显式状态迁移模型（44页珍藏版）》请在金锄头文库上搜索。

1、显式状态迁移模型 显式状态迁移模型 中国科学院软件研究所 张文辉 张文辉 http:/ http:/ zwh/pv互斥协议：卫式迁移模型 迁移集合： 初始状态： 2互斥协议：示意图 t0 s0 x=1,t=0 y=1,t=1 t1 s1 初始状态 x=0|t=0 y=0|t=1 s0 t2 s2 t0 x=0 x=0 y=0 y=0 t=0 3 t3 s3系统状态及状态变化关系 系统状态及状态变化关系 系统状态有5 个分量 系统状态有5 个分量 用五元组(a,b,x,y,t) 表示 ( y ) 进程A 执行位置 变量t 的值 变量x 的值 进程B 执行位置 变量y 的值 的值 执行位置 的值

2、4运行：状态变化序列 s0t0000 s0,t0,0,0,0 s1,t0,0,1,1 s0,t1,1,0,0 s1,t1,1,1,0 s2t1110 s2,t1,1,1,0 s3,t1,1,0,0 s3,t2,1,0,0 3t3100 s1,t1,1,1,1 1t2111 s3,t3,1,0,0 s 1,t2,1,1,1 5 状态变化图: s0,t0,0,0,0 s0,t1,1,0,0 s1,t0,0,1,1 s2,t0,0,1,1 s0,t2,1,0,0 s1,t1,1,1,0 s1,t1,1,1,1 s3,t0,0,0,1 s0,t3,0,0,0 s2,t1,1,1,0 s1,t2,1,1

3、,1 s3,t0,0,0,1 6s0,t0,0,0,0 s0,t1,1,0,0 s1,t0,0,1,1 s2,t0,0,1,1 s1,t1,1,1,0 s0,t2,1,0,0 s1,t1,1,1,1 5 6 s3,t0,0,0,1 s0,t3,0,0,0 s2,t1,1,1,0 s1,t2,1,1,1 9 10 s3,t1,1,0,0 s1,t3,0,1,1 12 13 s3,t2,1,0,0 s2,t3,0,1,1 s3,t3,0,0,0 s3,t3,0,0,1 10 9 6 5 13 12 13 12 抽象状态变化图: z0 z12 z35 z67 z20 z46 z47 z97 z24

4、z78 z55 z97 8z0 z12 z35 z67 z46 z20 z47 5 6 z97 z24 z78 z55 9 10 z108 z59 12 13 z116 z91 z120 z121 10 9 6 5 13 12 13 12z0 z12 z35 z67 z46 z20 z47 z97 z24 z78 z55 z108 z59 z116 z91 z120 z121 z55 z78 z47 z46 z59 z108 z59 z108Kripke 模型 11Kripke 模型 系统状态 状态变化 抽象状态 二元组 状态变化 初始状态 二元组 状态集合 模型 Kripke 模型 12Kr

5、ipke 模型：例子 状态集合： 迁移关系 z0,z1,z2, z3, , z127 (z0 z35) (z0 z12) 迁移关系 ： 初始状态集： (z0,z35), (z0,z12), z0 13Kripke 模型：例子 z0,z127 , 代表根据字母顺序排列的128 个(a,b,x,y,t) 状态 zi 代表(a,b,x,y,t) i= 32*a+8*b+4*x+2*y+t 定义 a(i)=i/32 b(i) (i%32)/8 b(i)=(i%32)/8 x(i)=(i%8)/4 y(i)=(i%4)/2 t(i)=(i%2) 14Kripke 模型：例子 互斥协议的卫式迁移模型表示的

6、8 条迁移对应: 15Kripke 模型：可达状态的迁移 迁移关系包括能到可达状态的迁移26 个: 16Kripke 模型：可达状态 可达状态17 个: 17Kripke 模型：安全性质 系统的互斥性质表示为安全性质 系统的互斥性质表示为安全性质 18Kripke 模型：响应性质 系统具备的部分性质包括响应性质( 不满足) 系统具备的部分性质包括响应性质( 不满足) 19标号Kripke 模型 20 状态变化图: s0,t0,0,0,0 s0,t1,1,0,0 s1,t0,0,1,1 s2,t0,0,1,1 s0,t2,1,0,0 s1,t1,1,1,0 s1,t1,1,1,1 s3,t0,0

7、,0,1 s0,t3,0,0,0 s2,t1,1,1,0 s1,t2,1,1,1 s3,t0,0,0,1 21 抽象状态变化图: z0 z12 z35 z67 z20 z46 z47 z97 z24 z78 z55 z97 0 01 2 bt 0 03 5 22 a=s0: z0,z12, b=t0: z0,z35, 抽象状态变化图: pqr z0 p,q,r z12 z35 p p q q z67 z20 p q r z46 z47 r r z97 z24 z78 z55 p,r q r z97 0 bt 0 t0 0 bt 0 23 p: a=s0 q: b=t0 r: t=0 s: a=

8、s0 b=t0标号Kripke 模型 标号 p 模型 系统状态 状态变化 抽象状态 二元组 状态变化 初始状态 二元组 状态集合 状态信息 命题 标号 模型 标号Kripke 模型 24标号Kripke 模型：例子 状态集合： 迁移关系 z0,z1,z2, z3, (z0 z35) (z0 z12) 迁移关系 ： 初始状态集： (z0,z35), (z0,z12), z0 标号函数： L: L(z0)=p,q,r,L(z12)=p, 命题集合 p, q, r 的子集 25标号Kripke 模型：命题 定义命题: 定义命题: 26标号Kripke 模型：标号函数 可达状态的标号: 状态的标号 2

9、7 状态的标号:标号Kripke 模型：安全性质 系统的互斥性质表示为安全性质 系统的互斥性质表示为安全性质 28标号Kripke 模型：响应性质 系统具备的部分性质包括响应性质( 不满足) 系统具备的部分性质包括响应性质( 不满足) 29扩展标号Kripke 模型 30 抽象状态变化图: pqr z0 p,q,r z12 z35 p p q q z67 z20 p q r z46 z47 r r z97 z24 z78 z55 p,r q r z97 0 bt 0 t0 0 bt 0 31 p: a=s0 q: b=t0 r: t=0 s: a=s0 b=t0 抽象状态变化图: p q r

10、z0 p q r pqr p q r z12 z35 pqr pqr p q r p qr z67 z20 p q pqr p qr p q r z46 z47 p q r p q z97 z24 z78 z55 p q r p q r z97 0 bt 0 t0 0 bt 0 p q r p q r 32 p: a=s0 q: b=t0 r: t=0 s: a=s0 b=t0 抽象状态变化图: p q r z0 p q r pqr p q r z12 z35 pqr pqr p q r p qr z67 z20 pqr p qr p q z46 z47 p q z97 z24 z78 z55

11、 p q r p q r z97 0 bt 0 t0 0 bt 0 p q r p q r 33 p: a=s0 q: b=t0 r: t=0 s: a=s0 b=t0扩展标号Kripke 模型 扩展标号 p 模型 系统状态 状态变化 抽象状态 二元组 状态变化 初始状态 二元组 状态集合 状态信息 公式 扩展标号 模型 扩展标号Kripke 模型 34扩展标号Kripke 模型：例子 状态集合： 迁移关系 z0,z1,z2, z3, (z0 z35) (z0 z12) 迁移关系 ： 初始状态集： (z0,z35), (z0,z12), z0 标号函数： L: L(z0)=p q r, 命题公

12、式 35扩展标号Kripke 模型：例2 pq p p s01 s0 s02 p,q p p s1 s11 s12 q p,q q s11 s12 s2 p q 2 p,q s2 s2 36扩展标号Kripke 模型：例2 状态集合： 迁移关系 s0,s1 ,s2 (s0 s1) (s1 s1) (s1 s2) (s2 s2) 迁移关系： 初始状态集： (s0,s1),(s1,s1),(s1,s2),(s2,s2) s0 标号函数： L: L(s0)=p, L(s1)=q, L(s2)=p q 37公平Kripke 模型 38 抽象状态变化图: z0 z12 z35 z67 z20 z46 z

13、47 z97 z24 z78 z55 z97 39 抽象状态变化图: z0 z12 z35 z67 z20 z46 z47 z97 z24 z78 z55 z97 进程A 的运行 进程B 的运行 40 进程A 的运行 进程B 的运行公平Kripke 模型 系统状态 状态变化 抽象状态 二元组 状态变化 初始状态 二元组 状态集合 公平性约束 状态集合的集合 公平 模型 公平Kripke 模型 41公平Kripke 模型：例子 公平 p 模型 例子 状态集合： 迁移关系 z0,z1,z2, z3, (z0 z35) (z0 z12) 迁移关系 ： 初始状态集： (z0,z35), (z0,z12), z0 公平性约束： z35,z67, , z12,z20, 42Kripke 模型：安全性质 系统的互斥性质表示为安全性质 系统的互斥性质表示为安全性质 43Kripke 模型：响应性质 系统具备的部分性质包括响应性质( 不满足) 系统具备的部分性质包括响应性质( 不满足) 44