1、显式状态迁移模型中国科学院软件研究所张文辉http:/ 初始状态：迁移集合：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,0 s1,t0,0,1,1 s1,t1,1,1,0 s2,t1,1,1,0 s3,t1,1,0,0 s3,t2,1,0,0 s3,t3,1,0,0 s0,t1,1,0,0
2、s1,t1,1,1,1 s1,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,t2
3、,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模型：可达状态的迁移迁移关系包括能到可达状态的迁移26个:1
5、7Kripke模型：可达状态可达状态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,z35,23z0z
6、12z35z67z97z46z20z24z47 抽象状态变化图: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模型：标号函数可达状态的标号:状态的标号:28标
7、号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=t0pqrpqrpqrpqrpqrpqrpqrpqrpqrpqr33z0z12z35z67z97z46z20z24z4
8、7 抽象状态变化图: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,qqs2p,q37扩展标号Kripke模型：例2 状态集合：迁移关
9、系：初始状态集：标号函数：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 模型：例子 状态集合：迁移关系：初始状态集：公平性约束：z0,z1,z2,z3,(z0,z35),(z0,z12),z0 z35,z67,z12,z20,43Kripke模型：安全性质系统的互斥性质表示为安全性质44Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)
