《显式状态迁移模型》PPT课件.ppt
《《显式状态迁移模型》PPT课件.ppt》由会员分享,可在线阅读,更多相关《《显式状态迁移模型》PPT课件.ppt(44页珍藏版)》请在得力文库 - 分享文档赚钱的网站上搜索。
1、显式状态迁移模型中国科学院软件研究所张文辉http:/ 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,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,
2、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,1,0,0s3,t3,0,0,01096s2,t3,0,1,1s3,t3,0,0,15131213125691012138z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55z0z12z35z67z97z46z20z24z47z78z55z108z5
3、9z116z1201096z91z121513121312569101213z0z12z35z67z97z46z20z24z47z78z55z108z59z116z120z55z78z47z91z121z46z59z108z59z10811 Kripke 模型12 Kripke 模型系统状态状态变化初始状态抽象状态二元组状态集合 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,
4、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个:17Kripke模型:可达状态可达状态17个:18Kripke模型:安全性质系统的互斥性质表示为安全性质19Kripke模型:响应性质系统具备的部分性质包括响应性质(不满足)20标号Kripke模型21s0,t0,0,0,0s0,t1,1,0,0s1,t0,0,1,1s2,t0,0,1,1s
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 显式状态迁移模型 状态 迁移 模型 PPT 课件
限制150内