《时间迁移系统》PPT课件.ppt

《《时间迁移系统》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《时间迁移系统》PPT课件.ppt（51页珍藏版）》请在三一办公上搜索。

1、时间迁移系统,中国科学院软件研究所张文辉http:/,自动售茶机,s0,1,1,1,2,1,取茶,s1,s3,s5,2,s2,2,s4,找钱/取钱,2,退钱,s6,s7,出茶,取钱,x,x10,x=10,量的变化,3,时间迁移系统,x=0|t=0,4,系统运行过程描述：例子,t0,x=1,t=0,t1,t2,y=0|t=1,t3,x=0,s0,y=1,t=1,s1,s2,s3,y=0,无约束,1,5,无约束,无约束,2,8,无约束,5,z0,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,b,u,true,b,u,u1,b,u5,a,v,tru

2、e,a,v,true,b,u,u1,6,时间变化,5.05.15.75.910.4 ba abbz0 z12z12z12z20z24u=5.0,u=0.1 u=0.7 u=0.9u=4.5u=0.0,u=0.1 u=0.7 u=0.0 u=4.5v=5.0 v=5.1v=0.6v=0.2v=4.7v=5.0 v=0.0v=0.0v=0.2v=4.7,7,时间迁移系统,动作信息系统状态时钟变量状态变化初始状态,符号抽象状态变量集合五元组状态集合,时间迁移系统,8,时间迁移系统：例子,标号集合：状态集合：时钟变量集合：迁移关系：初始状态集：,a,b z0,z1,z2,z3,u,v(z0,a,v,t

3、rue,z12),z0,时钟变量相关公式,9,时间迁移系统：例子,S0,S1,a,S2,S3,d,y2,x:=0,b,y:=0,c,x1,10,时间迁移系统：例子,11,时间迁移系统：运行,12,时间Buchi自动机1,S1,S0,b,S2,S3,S2,a,a,x:=0,a,x:=0,b,x2,13,时间Buchi自动机1,14,时间Buchi自动机1：运行/语言,15,时间Buchi自动机2,S0,S1,S2,S3,S2,a,y:=0,a,x:=0,x=1,b,y:=0,y1,a,x:=0,x=1,16,时间Buchi自动机2,17,时间Buchi自动机2：运行/语言,混成迁移系统/混成自动

4、机,混成迁移系统/混成自动机,水箱,x=2,x=5x:=x+1,x=1x=9,x=-1,on,off,混成迁移系统/混成自动机,水箱,x=1,x=-1,on,off,on2off,x:=x+1,x=5,off2on,x=2,x=9,21,混成迁移系统/混成自动机,动作信息系统状态变量状态状态变化初始状态,符号抽象状态变量集合五元组混合状态集合,混成自动机,混成自动机,混成自动机,24,Petri网,x=0|t=0,25,系统运行过程描述：例子,t0,x=1,t=0,t1,t2,y=0|t=1,t3,x=0,s0,y=1,t=1,s1,s2,s3,y=0,初始状态s0t0 x=0y=0t=0,2

5、6,系统资源模型,s0s1s2s3,t0t1t2t3,27,系统资源模型,t0t1t2t3,s0s1s2s3,28,系统资源模型,t0t1t2t3,s0s1s2s3,29,系统资源模型,t0t1t2t3,s0s1s2s3,30,Petri网,位置迁移状态变化描述初始状态,抽象元素抽象元素边（两种）位置标号,Petri网,31,系统资源模型,t0v0t1v1t2v2t3v3,s0u0s1u1s2u2s3u3,ts,32,Petri网：例子,位置集合：迁移集合：边的集合：初始状态：,s0,s3,t0,t3,ts u0,u3,v0,v3(s0,u0),(u0,s1),(s1,u1),(ts,u1),

6、M:M(s0)=1,M(s1)=0,M(s2)=0,33,有问题的系统资源模型,s0u0s1u1s2u2,t0v0t1v1t2v2,34,通信系统,35,系统资源模型,t0v0t1v1t2v2t3v3,s0u0s1u1s2u2s3u3,ts,36,系统资源模型,ts!1ts?1,ts!1ts?1,ts,37,系统资源模型,ts!1ts?1,ts!1ts?1,ts,38,系统资源模型,1,ts!1ts?1,ts!1ts?1,ts,39,系统资源模型,ts!1ts?1,ts!1ts?1,ts,40,通信系统,状态通道状态变化初始状态,抽象状态二元组三元组给定状态,通信系统,41,系统资源模型,t0

7、t1ts!1t2ts?1t3,s0s1ts!1s2ts?1s3,ts,42,通信单元：例子,状态集合：通道集合：迁移关系：初始状态：,s0,s3 ts:(s0,s1),(s1,ts?1,s2),s0,通信系统：通信单元的组合,43,通信系统：例子,q0,q1,q2,q3,q4,q5,!0,?1,?0,!1,?1,?0,!0,!1,44,通信系统：例子,q2,q0,q1,q3,q4,q5,?0,!0,?1,!1,?0,?1,!0,!1,45,通信系统：例2,rw()=1,2y+x=(y+x)%4,s0,t1,S!B,t0,B+1=b,B+,B+1!=b,R!(A+rw(),s1,S?A,R?b,

8、46,通信系统：例2,s0,s1,m1!1,m1!2,m2?1,m2?2,m2?0,s3,s2,m2?2,m2?3,m2?0,m1!2,m1!3,m2?3,m2?0,m2?1,m1!3,m1!0,m2?0,m2?1,m2?2,m2?3,m1!0,m1!1,m2?1,m2?2,m2?3,47,通信系统：例2,t0,t1,m2!0,m1?1,m1?2,m1?0,t3,t2,m1?2,m1?3,m1?0,m2!1,m1?3,m1?0,m1?1,m2!2,m1?0,m1?1,m1?2,m1?3,m2!3,m1?1,m1?2,m1?3,48,通信系统：例2,rw()=1,2,W,s0,t1,S!B,t0

9、,B+1=b,B+,B+1!=b,R!(A+rw(),s1,S?A,R?b,49,通信系统：例2,Window Protocol InvariantB W Ri B+W for 1 i r,50,通信系统：例2,Window Protocol InvariantB W Ri B+W for 1 i r,引理1：A S1 Ss B,引理2：设 R0=B,Rr+1=A+1 则 Ri Rj+W for 0 i r,ij r+1,51,有限状态变量与自动机,q0,q1,mi?r,mi?0,mi?0,(mi?2),mi?2,mi?r,q2,mi?1,r0,mo!0,r1,mo!1,mi?r,r2,mo!2,m 0,1,2,