实时系统的形式模型与形式验证.ppt

文档介绍：:形式化方法Untimedsystems的形式模型(状态迁移系统)Untimedsystems的性质表示(时序逻辑LTL)实时系统的形式模型(时间自动机)实时系统的性质表示(实时逻辑)实时系统的形式验证(模型检测)模型检测工具UPPAAL简介我们正在进行的部分工作介绍导言:系统分析的形式化方法形式化方法:一系列基于严格数学理论的用来描述和分析系统性质和行为的符号、技术和手段。:系统的数学模型及建模语言(一般基于状态迁移系统、自动机等):性质描述及规约语言(一般基于逻辑):定理证明或模型检测Untimedsystems:系统建模(1)迁移系统(TransitionSystems)(Q,Q0,T),其中:Q是状态集合,Q0Q为初始状态集,TQ(无穷)计算序列:q0,q1,q2,…..,满足:(1)q0Q0;(2)对于任意i0有,(qi,q(i+1)):迁移系统(Q,Q0,T)Q={on,off}Q0={on}T={(on,on),(on,off),(off,on),(off,off)}计算序列:On,on,off,…..,On,off,….所有以on开头,:系统建模(2)标号迁移系统(LabeledTransitionSystems,LTS)(Q,Q0,,T)其中:Q是状态集合,Q0Q为初始状态集,S是一个有限的标号集合(字母集),通常用来事件、动作或变量的取值,TQS….这里:q0Q0,且对任意非负整数i有:(qi,ai,q(i+1))T(无穷)计算序列:举例2:标号迁移系统:(Q,Q0,,T)Q={on,off},Q0={on},={a,b}(设想a表示‘开灯’事件,b表示‘关灯’事件)T={(on,a,on),(on,b,off),(off,a,on),(off,b,off)}计算序列:aabboffonaonbonboffaoff….Untimedsystems:系统建模(3)-automata(无穷字上的有限状态自动机)Büchiautomata:(Q,Q0,,T,F),其中:Q是有穷的状态集,Q0Q为初始状态集,S是一个有限字母集,TQSQ为迁移关系F::Büchiautomata(Q,Q0,,T,F)Q={on,off},Q0={on},={a,b},T={(on,a,on),(on,b,off),(off,a,on),(off,b,off)}F={off}计算序列:(状态off要出现无穷次)接受:不接受:abboffonabonaoffbonaoff….aonaonaonaon….Untimedsystems:性质表示时序逻辑(TemporalLogic)用于表示时序关系的逻辑语言线性时序逻辑(LTL,LinearTemporalLogic)putationTreeLogic),(省略)-演算(省略)