显式状态迁移模型课件

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

2、0,0s1,t1,1,1,1s1,t2,1,1,16s0,t0,0,0,0s0,t1,1,0,0s1,t0,0,1,1s2,t0,0,1,1s3,t0,0,0,1s1,t1,1,1,0s0,t2,1,0,0s0,t3,0,0,0s1,t1,1,1,1状态变化图:s2,t1,1,1,0s1,t2,1,1,1s0,t0,0,0,0s0,t1,1,0,0s1,t0,0,1,1s2,t0,0,1,1s3,t0,0,0,1s1,t1,1,1,0s0,t2,1,0,0s0,t3,0,0,0s1,t1,1,1,1s2,t1,1,1,0s1,t2,1,1,1s3,t1,1,0,0s1,t3,0,1,1s3,t

3、2,1,0,0s3,t3,0,0,01096s2,t3,0,1,1s3,t3,0,0,15131213125691012138z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55z0z12z35z67z97z46z20z24z47z78z55z108z59z116z1201096z91z121513121312569101213z0z12z35z67z97z46z20z24z47z78z55z108z59z116z120z55z78z47z91z121z46z59z108z59z10811 Kripke 模型12 Kripke 模型系统状态状态变化初始状态抽象状态二

4、元组状态集合 Kripke 模型13Kripke模型：例子状态集合：迁移关系：初始状态集： z0, z1, z2, z3, , z127 (z0,z35), (z0,z12), z0 14Kripke模型：例子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/32b(i)=(i%32)/8x(i)=(i%8)/4y(i)=(i%4)/2t(i)=(i%2)15Kripke模型：例子互斥协议的卫式迁移模型表示的8条迁移对应:16Kripke模型：可达状态的迁移迁移关系包括能到可达状态

5、的迁移26个:17Kripke模型：可达状态可达状态17个:18Kripke模型：安全性质系统的互斥性质表示为安全性质19Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)20标号Kripke模型21s0,t0,0,0,0s0,t1,1,0,0s1,t0,0,1,1s2,t0,0,1,1s3,t0,0,0,1s1,t1,1,1,0s0,t2,1,0,0s0,t3,0,0,0s1,t1,1,1,1状态变化图:s2,t1,1,1,0s1,t2,1,1,122z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55a=s0: z0,z12, b=t0: z0,

6、z35,23z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55p,q,rp: a=s0 q: b=t0 r: t=0 s: a=s0b=t0ppp,rqqqrr24标号Kripke模型系统状态状态变化初始状态状态信息抽象状态二元组状态集合命题标号Kripke模型25标号Kripke模型：例子状态集合：迁移关系：初始状态集：标号函数： z0, z1, z2, z3, (z0,z35), (z0,z12), z0 L: L(z0)=p,q,r,L(z12)=p,命题集合 p, q, r 的子集 26标号Kripke模型：命题定义命题:27标号Kripke模型：标号函数

7、可达状态的标号:状态的标号:28标号Kripke模型：安全性质系统的互斥性质表示为安全性质29标号Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)30扩展标号Kripke模型31z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55p,q,rp: a=s0 q: b=t0 r: t=0 s: a=s0b=t0ppp,rqqqrr32z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55pqrp: a=s0 q: b=t0 r: t=0 s: a=s0b=t0pqrpqrpqrpqrpqrpqrpqrpqrpqrpqr33z0

8、z12z35z67z97z46z20z24z47抽象状态变化图:z78z55pqrp: a=s0 q: b=t0 r: t=0 s: a=s0b=t0pqrpqrpqrpqrpqrpqrpqrpqrpq34扩展标号Kripke模型系统状态状态变化初始状态状态信息抽象状态二元组状态集合公式扩展标号Kripke模型35扩展标号Kripke模型：例子状态集合：迁移关系：初始状态集：标号函数： z0, z1, z2, z3, (z0,z35), (z0,z12), z0 L: L(z0)=pqr,命题公式36s01s0s1s2s11s02s12p,qppqpq扩展标号Kripke模型：例2p,qqs2

9、p,q37扩展标号Kripke模型：例2状态集合：迁移关系：初始状态集：标号函数： s0, s1 ,s2 (s0,s1),(s1,s1),(s1,s2),(s2,s2) s0 L: L(s0)=p, L(s1)=q, L(s2)=pq38公平Kripke模型39z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z5540z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55进程A的运行 进程B的运行41公平Kripke 模型系统状态状态变化初始状态公平性约束抽象状态二元组状态集合状态集合的集合公平Kripke 模型42公平Kripke 模型：例子状态集合