显式状态迁移模型课件

显式状态迁移模型中国科学院软件研究所张文辉/~zwh/pv显式状态迁移模型中国科学院软件研究所2互斥协议：卫式迁移模型初始状态：迁移集合：互斥协议：卫式迁移模型初始状态：迁移集合：3互斥协议：示意图x==0||t==0t0x=1,t=0t1t2y==0||t==1t3x=0s0y=1,t=1s1s2s3y=0初始状态s0t0x=0y=0t=0互斥协议：示意图x==0||t==0t0x=1,t=0t1t4系统状态及状态变化关系系统状态有5个分量用五元组(a,b,x,y,t)表示进程A执行位置变量x的值进程B执行位置变量t的值变量y的值系统状态及状态变化关系系统状态有5个分量用五元组(a,b,x5运行：状态变化序列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,0,0s1,t1,1,1,1s1,t2,1,1,1运行：状态变化序列s0,t0,0,0,06s0,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,s0,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,1,0,0s3,t3,0,0,01096s2,t3,0,1,1s3,t3,0,0,1513121312569101213s0,t0,0,0,0s0,t1,1,0,0s1,t0,0,8z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55z0z12z35z67z97z46z20z24z47抽象状态z0z12z35z67z97z46z20z24z47z78z55z108z59z116z1201096z91z121513121312569101213z0z12z35z67z97z46z20z24z47z78zz0z12z35z67z97z46z20z24z47z78z55z108z59z116z120z55z78z47z91z121z46z59z108z59z108z0z12z35z67z97z46z20z24z47z78z11Kripke模型Kripke模型12Kripke模型系统状态状态变化初始状态抽象状态二元组状态集合Kripke模型Kripke模型系统状态抽象状态Kripke模13Kripke模型：例子状态集合：迁移关系：初始状态集：{

z0,

z1,

z2,

z3,…,

z127}{

(z0,z35),

(z0,z12),

…

}{

z0

}Kripke模型：例子状态集合：{z0,z1,z2,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/32 b(i)=(i%32)/8 x(i)=(i%8)/4 y(i)=(i%4)/2 t(i)=(i%2)Kripke模型：例子z0,…,z12715Kripke模型：例子互斥协议的卫式迁移模型表示的8条迁移对应:Kripke模型：例子互斥协议的卫式迁移模型表示的8条迁移对16Kripke模型：可达状态的迁移迁移关系包括能到可达状态的迁移26个:Kripke模型：可达状态的迁移迁移关系包括能到可达状态的迁17Kripke模型：可达状态可达状态17个:Kripke模型：可达状态可达状态17个:18Kripke模型：安全性质系统的互斥性质表示为安全性质Kripke模型：安全性质系统的互斥性质表示为安全性质19Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)Kripke模型：响应性质系统具备的部分性质包括响应性质(不20标号Kripke模型标号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,1s0,t0,0,0,0s0,t1,1,0,0s1,t0,0,22z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55a=s0:{z0,z12,…}b=t0:{z0,z35,…}z0z12z35z67z97z46z20z24z47抽象状态23z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55p,q,rp:a=s0q:b=t0r:t=0s:a=s0b=t0ppp,rqqqrrz0z12z35z67z97z46z20z24z47抽象状态24标号Kripke模型系统状态状态变化初始状态状态信息抽象状态二元组状态集合命题标号Kripke模型标号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}的子集

标号Kripke模型：例子状态集合：{z0,z1,z226标号Kripke模型：命题定义命题:标号Kripke模型：命题定义命题:27标号Kripke模型：标号函数可达状态的标号:状态的标号:标号Kripke模型：标号函数可达状态的标号:状态的标号:28标号Kripke模型：安全性质系统的互斥性质表示为安全性质标号Kripke模型：安全性质系统的互斥性质表示为安全性质29标号Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)标号Kripke模型：响应性质系统具备的部分性质包括响应性质30扩展标号Kripke模型扩展标号Kripke模型31z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55p,q,rp:a=s0q:b=t0r:t=0s:a=s0b=t0ppp,rqqqrrz0z12z35z67z97z46z20z24z47抽象状态32z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55pqrp:a=s0q:b=t0r:t=0s:a=s0b=t0pqrpqrpqrpqrpqrpqrpqrpqrpqrpqrz0z12z35z67z97z46z20z24z47抽象状态33z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55pqrp:a=s0q:b=t0r:t=0s:a=s0b=t0pqrpqrpqrpqrpqrpqrpqrpqrpqz0z12z35z67z97z46z20z24z47抽象状态34扩展标号Kripke模型系统状态状态变化初始状态状态信息抽象状态二元组状态集合公式扩展标号Kripke模型扩展标号Kripke模型系统状态抽象状态扩展标号Kripke35扩展标号Kripke模型：例子状态集合：迁移关系：初始状态集：标号函数：{

z0,

z1,

z2,

z3,…

}{

(z0,z35),

(z0,z12),

…

}{

z0

}L:L(z0)=pqr,…命题公式扩展标号Kripke模型：例子状态集合：{z0,z1,36s01s0s1s2s11s02s12p,qppqpq扩展标号Kripke模型：例2p,qqs2p,qs01s0s1s2s11s02s12p,qppqpq扩展标37扩展标号Kripke模型：例2状态集合：迁移关系：初始状态集：标号函数：{

s0,

s1,s2}{(s0,s1),(s1,s1),(s1,s2),(s2,s2)}{

s0

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

z0,

z1,

z2,

z3,…

}{

(z0,z35),

(z0,z12),

…

}{

z0

}{{z35,z67,…

},

{z12,z20,…}}公平Kripke模型：例子状态集合：{z0,z1,z43Kripke模型：安全性质系统的互斥性质表示为安全性质Kripke模型：安全性质系统的互斥性质表示为安全性质44Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)Kripke模型：响应性质系统具备的部分性质包括响应性质(不显式状态迁移模型中国科学院软件研究所张文辉/~zwh/pv显式状态迁移模型中国科学院软件研究所46互斥协议：卫式迁移模型初始状态：迁移集合：互斥协议：卫式迁移模型初始状态：迁移集合：47互斥协议：示意图x==0||t==0t0x=1,t=0t1t2y==0||t==1t3x=0s0y=1,t=1s1s2s3y=0初始状态s0t0x=0y=0t=0互斥协议：示意图x==0||t==0t0x=1,t=0t1t48系统状态及状态变化关系系统状态有5个分量用五元组(a,b,x,y,t)表示进程A执行位置变量x的值进程B执行位置变量t的值变量y的值系统状态及状态变化关系系统状态有5个分量用五元组(a,b,x49运行：状态变化序列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,0,0s1,t1,1,1,1s1,t2,1,1,1运行：状态变化序列s0,t0,0,0,050s0,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,s0,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,1,0,0s3,t3,0,0,01096s2,t3,0,1,1s3,t3,0,0,1513121312569101213s0,t0,0,0,0s0,t1,1,0,0s1,t0,0,52z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55z0z12z35z67z97z46z20z24z47抽象状态z0z12z35z67z97z46z20z24z47z78z55z108z59z116z1201096z91z121513121312569101213z0z12z35z67z97z46z20z24z47z78zz0z12z35z67z97z46z20z24z47z78z55z108z59z116z120z55z78z47z91z121z46z59z108z59z108z0z12z35z67z97z46z20z24z47z78z55Kripke模型Kripke模型56Kripke模型系统状态状态变化初始状态抽象状态二元组状态集合Kripke模型Kripke模型系统状态抽象状态Kripke模57Kripke模型：例子状态集合：迁移关系：初始状态集：{

z0,

z1,

z2,

z3,…,

z127}{

(z0,z35),

(z0,z12),

…

}{

z0

}Kripke模型：例子状态集合：{z0,z1,z2,58Kripke模型：例子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 x(i)=(i%8)/4 y(i)=(i%4)/2 t(i)=(i%2)Kripke模型：例子z0,…,z12759Kripke模型：例子互斥协议的卫式迁移模型表示的8条迁移对应:Kripke模型：例子互斥协议的卫式迁移模型表示的8条迁移对60Kripke模型：可达状态的迁移迁移关系包括能到可达状态的迁移26个:Kripke模型：可达状态的迁移迁移关系包括能到可达状态的迁61Kripke模型：可达状态可达状态17个:Kripke模型：可达状态可达状态17个:62Kripke模型：安全性质系统的互斥性质表示为安全性质Kripke模型：安全性质系统的互斥性质表示为安全性质63Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)Kripke模型：响应性质系统具备的部分性质包括响应性质(不64标号Kripke模型标号Kripke模型65s0,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,66z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55a=s0:{z0,z12,…}b=t0:{z0,z35,…}z0z12z35z67z97z46z20z24z47抽象状态67z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55p,q,rp:a=s0q:b=t0r:t=0s:a=s0b=t0ppp,rqqqrrz0z12z35z67z97z46z20z24z47抽象状态68标号Kripke模型系统状态状态变化初始状态状态信息抽象状态二元组状态集合命题标号Kripke模型标号Kripke模型系统状态抽象状态标号Kripke模型69标号Kripke模型：例子状态集合：迁移关系：初始状态集：标号函数：{

z0,

z1,

z2,

z3,…

}{

(z0,z35),

(z0,z12),

…

}{

z0

}L:L(z0)={p,q,r},L(z12)={p},…命题集合{p,q,r}的子集

标号Kripke模型：例子状态集合：{z0,z1,z270标号Kripke模型：命题定义命题:标号Kripke模型：命题定义命题:71标号Kripke模型：标号函数可达状态的标号:状态的标号:标号Kripke模型：标号函数可达状态的标号:状态的标号:72标号Kripke模型：安全性质系统的互斥性质表示为安全性质标号Kripke模型：安全性质系统的互斥性质表示为安全性质73标号Kripke模型：响应性质系统具备的部分性质包括响应性质(不满足)标号Kripke模型：响应性质系统具备的部分性质包括响应性质74扩展标号Kripke模型扩展标号Kripke模型75z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55p,q,rp:a=s0q:b=t0r:t=0s:a=s0b=t0ppp,rqqqrrz0z12z35z67z97z46z20z24z47抽象状态76z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55pqrp:a=s0q:b=t0r:t=0s:a=s0b=t0pqrpqrpqrpqrpqrpqrpqrpqrpqrpqrz0z12z35z67z97z46z20z24z47抽象状态77z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55pqrp:a=s0q:b=t0r:t=0s:a=s0b=t0pqrpqrpqrpqrpqrpqrpqrpqrpqz0z12z35z67z97z46z20z24z47抽象状态78扩展标号Kripke模型系统状态状态变化初始状态状态信息抽象状态二元组状态集合公式扩展标号Kripke模型扩展标号Kripke模型系统状态抽象状态扩展标号Kripke79扩展标号Kripke模型：例子状态集合：迁移关系：初始状态集：标号函数：{

z0,

z1,

z2,

z3,…

}{

(z0,z35),

(z0,z12),

…

}{

z0

}