《航空电子系统模型检查技术——时态逻辑建模与分析》由会员分享，可在线阅读，更多相关《航空电子系统模型检查技术——时态逻辑建模与分析（117页珍藏版）》请在金锄头文库上搜索。
1、1,实时系统的形式化 验证技术,研讨课2013-11,2,引言形式化方法的定义,形式化（formal method）方法： 广义有精确数学语义的系统工程方法； 狭义 形式化规格（specification）方法； 形式化验证（verification）方法。,3,引言形式化验证方法,基于（形式化）模型的开发过程 基于模型的规格说明基于规格化模型的验证 形式化验证主要包括： 模型检查（model checking） 形式语言推理证明,4,引言形式化验证方法（续）,模型检查 基于有限状态模型，检查该模型的期望特性是否得到满足； 状态空间的蛮力（brute）搜索，理论上是指数复杂度的，但可以采用较合
2、理的数据结构在一定的程度上提高效率； 当所检查的性质未被满足的时候，终止运行，给出反例和状态变化轨迹； 可以用于系统的部分的规格说明的检查； 无限状态可抽象为有限状态描述。,5,引言形式化验证方法（续）,计算复杂度 时间：EXPTIME 空间：PSPACE,引用自 Ruys Theo. Formal Methods and Tools.System Validation course, dept. of CS, Univ. of Twente. 2006.5,6,引言形式化验证方法（续）,模型检查与时间自动机 Time Automata时间自动机模型 逻辑时态逻辑 操作并发操作,7,引言形式化
3、验证方法（续）,模型检查工具 SPIN, HyTech, UPPAAL, Kronos, EMC, BOOST, Hybrid 模型检查工具与项目开发方法的结合 如：以色列IAI的ESM 如：欧洲的ASDE 如：用于AFDX端到端延迟抖动的分析,8,提纲,时态逻辑与行为建模 时间自动机模型检查及UPPAAL工具 *模型检查工具的实现技术 *模型检查工具的扩展 *应用案例,9,时态逻辑与行为建模 时间自动机模型检查及工具,实时系统形式化验证技术 时间自动机和模型检查,2013,10,时态逻辑与行为建模,命题逻辑、一阶逻辑、模态逻辑、时态逻辑行为建模 以CTL（计算树逻辑）为例，说明时态逻辑的行为
4、建模能力；并且综述 各种时态逻辑的比较与评价规则。,11,经典逻辑,命题逻辑 命题（proposition）：对事物作出确定性判断的陈述语句。 真、假 原子命题：非 复合命题： 二元连接词 合取（和） 、析取（或） 蕴含 （if then）,12,经典逻辑（续）,逻辑推理 P, Q |- R ，P, Q的关系不仅仅是和关系 对原子命题进行分解 个体（域） 研究对象所构成的非空集合 确定的个体 常元 泛指的个体 变元 函词 谓词（predication） 量词：用来约束变元，表示个体数量 存在量词 （Existence） 全称量词（All）,13,经典逻辑（续）,“零阶”：命题逻辑 一阶：（一阶
5、）谓词逻辑 FOL: first order logic 高阶：允许将谓词也作为可量化的变元 HOL: higher order logic高阶表现力强，但逻辑的完备性与可判定性差,14,模态逻辑,模态 Modal moudl 不涉及本质的执行模式；“情境” 描述“可能世界” 模态词： 必然（necessary） 可能（possibility） 模态逻辑 命题/FOL/HOL + 模态词扩展,15,模态逻辑（续）,模态逻辑的模型Kripe结构 三元组 M = ( W, R, L ) World 可能的“世界”集合（或者说不同状态的世界） Relation 二元关系 wi 到 wj 的迁移 La
6、beling （或 evaluation func.） L: W 2P ； P 原子公式的集合,16,时态逻辑,对模态（Modal）的时态（Temporal）解释 R: 时间先后关系 必然 ： always 算子 （ henceforth ） 可能 ：sometimes 算子 （eventually ） 命题成立与否具有时间依赖性 事件发生的顺序（event ordering） 逻辑变元取值发生改变的时间关系next 算子： , A， mAuntil 算子: （ since 算子 ）,17,时态逻辑（续）,时间域的结构 离散 / 连续 线性 / 分支线性时态逻辑LTI PLTI FOLTI 应
7、用案例： 数字电路分析 工具：e.g. HYBIRD, BOOST - SPL SCADE / Signal Property Language,任意当前时刻只存在唯一的可能未来时刻,分支时态逻辑可以较好地处理不确定性,18,时态逻辑（续）,计算树逻辑 CTL 和 CTL* CTL: computational tree logic Clarke E M, Emerson E A, 1980s “Automatic verification of finite-state concurrent systems using temporal logic specifications” Model
8、 checking - also by Clarke & Emerson “For verifying CTL specification, a model-checking approach is typically used since the specification can be modeled as a state machine”,19,时态逻辑（续）,Model checking （续） 基于有限状态模型， 对模型的状态空间进行蛮力搜索， 检查该模型是否具有某种性质。 e.g. 利用Kriple结构的标号算法（labeling algo.），NP，bruteFSM - 由 co
9、mputational tree 折叠而成 Time Automata 并发，实例化，事件同步 by Alur R 1990s 组合爆炸 EXPTIME, PSPACE 如：有序二叉决策图（Ordered Binary Decision Diagrams），：100200状态变量，状态数目10120的系统,思考：时间（时钟）状态如何表达？,20,行为建模,时态逻辑关注系统行为建模，而不是功能或结构Functional modeling 负责处理系统的数据传输，输入输出的内容 Structural modeling 如何将系统分解为子系统和组件 Behavior modeling 行为是指系统对
10、外部激励和内部事件的响应，这是反应式（reactive）和实时系统的关键方面。 典型地，系统的行为由一系列的关系（relationship）的集合表达，这些关系枚举了事件和动作之间的时态约束。,将时态逻辑用于行为建模,21,行为建模（续）,Assessing the capabilities of TL 时态逻辑的行为表达能力 时态逻辑模型的自动验证能力评价准则 逻辑阶 时态结构 事件顺序 时间度量 显式时钟/隐式时钟 逻辑可判定性,22,时态逻辑的行为建模能力,以CTL为例作主要讲解，结合与其它TL的比较1. 逻辑阶 Logic order CTL 是 命题逻辑 “分支时态逻辑中则需要提供对
11、分支的时间特性下多种未来行为描述的量化词” 1 未来路径：A - 某一路径：E - 对于状态公式 ，存在路径树,详见工具部分,23,时态逻辑的行为建模能力（续）,2. 时态结构 Temporal Structure Clarkes CTL: 离散、时间点实体、树状分支结构3. 事件顺序 Ordering of events Clarkes CTL: 因果关系：由经典逻辑继承了蕴含（imply）算子： Ordering of events：必须定义until算子,24,时态逻辑的行为建模能力（续）,4. 时间度量 Metrics for time 对于Clarkes CTL，没有定义时间度量，只
12、有时间的顺序可以判别 其它TL或是CTL的改进，可以引进时间度量 CTL的改进有时间度量5. 显式时钟/隐式时钟 Explicit / implicit Clarkes CTL，隐式时钟,25,时态逻辑的行为建模能力（续）,5. 显式时钟/隐式时钟（续） 隐式时钟：只考察事件之间的时间先后次序 全局的显式时钟： 逻辑关系式中有时钟变元T，这样，很多情况下，式中甚至不用考虑时间域的结构，如： ( ( )( ) )显示时钟必然要求 时间度量,量词,26,时态逻辑的行为建模能力（续）,5. 显式时钟/隐式时钟（续） Alur R and Henzinger T. A s Observations 2
13、 如果不允许用显式的量词修饰时间变元，将使规范定义的风格更加自然；（1990） 如果找到实际可用的验证（verification）方法，必然不可能使用显式的量词修饰时间变元。 换言之，“用显式的量词修饰时间变元”实际上超过了FOL（对PL更是如此）的表达能力，同时是不可决定的。,27,时态逻辑的行为建模能力（续）,5. 显式时钟/隐式时钟（续） 局部的时钟 如果有时间度量，可以用Kriple(W, R, L)结构模型对时钟建模； e.g. UPPAAL Formal Spec. 每个实例可以申明多两个clock var. Formal Verif. 没有修饰时间的量词，所谓的“时钟”相当于计时
14、器，并不是抽象的物理时间。 e.g. UPPAAL的可判定性 UPPAAL 的Formal Spec. Time Automata Time Automata (TA) created by Alur R !,28,时态逻辑的行为建模能力（续）,6. 可判定性 Logic decidability Formal Spec. Formal Verification 特例：symbolic model checking 例 Clarkes CTL Yes 例 CTL的扩展 - CTL* 可用Labeling Algo.检查其它的TL: 线性： PTL, Choppy, ITL, PMLTI, IL
15、, EIL, RTIL, TILCO 分支：BTTL, PMLTI, 实时系统需要什么样的TL？ 具体问题具体分析 有工具支持工程师可用 不要被名称迷惑，e.g. RTTL 允许量词修饰时间，如果在这种情况下就是 un-decidable,29,时态逻辑与行为建模 时间自动机模型检查及工具,实时系统形式化验证技术 时间自动机和模型检查,2013,计划2013-11-15,30,时态逻辑建模与模型检查工具,UPPAAL“Modeling language” Time Automata 并发的TA，相当于networks of TA “Query language” a subset of CTL
16、 Model Checking Enginesince 1995 LARSEN K G, PETTERSON P, WANG Y,31,时间自动机,timed graph timed Bchi automata timed safety automataAlur Rajeev, Dill David L 1990 clock variables constraints on the clock var.s restrict the behavior of the TA constraints on properties of process by: Bchi Accepting Theorem,
