张坤-华中师范大学硕士论文答辩（最终版）.ppt

* * * Computer Science | Software Engineering Information System Computer Science | Software Engineering Information System * 华中师范大学硕士论文答辩 * 一种基于活性顺序图的 运行时验证研究 姓名：张坤 专业：计算机软件与理论 指导教师：叶俊民教授 内容提纲 绪论 3 4 研究基础 基于活性顺序图的运行时验证方法 一种离线方式验证工具的设计与实现 5 实验及其结果分析 基于活性顺序图的运行时验证框架 1 3 2 4 6 5 总结和展望 7 1、安全关键系统的故障会造成灾难性后果。 2、测试只能发现系统错误，不能保证系统一定正确。 3、模型检测等形式化方法针对的是抽象系统，且容易产生状态空间爆炸问题。 研究背景 运行时验证是一种轻量级的验证方法，它从高层规约中自动综合出监控器，监控器监控系统的执行状态，并给出执行状态是否满足需求规约的判定。 研究现状与存在的问题 研究现状： 在需求规约描述方面，如何方便地使用形式化语言描述需求规约是运行时验证领域的一个研究方向 在监控器构造方面，基于重写逻辑[10-12]、基于自动机[13-16] 目前运行时验证技术还存在以下不足： 已有的基于可视化需求规约场景的验证方法容易产生冗余性质，验证开销较大，且二值语义的验证结果是不准确的 已有的基于Maude工具引擎的重写逻辑运行时验证算法效率较低，不利于快速的发现系统故障 拟解决的关键问题 1、使用AOP技术进行代码插装获取目标系统执行轨迹。 2、研究一种基于活性顺序图的运行时验证的改进方法。 3、设计原型工具进行运行时验证，验证本文改进方法的可行性和有效性。 活性顺序图 实例 实例线 前置图 主图 消息 条件 活性顺序图[26]具有基于轨迹的形式化语义，根据图中消息事件的执行轨迹可以将其描述的需求规约转换为对应的LTL公式 基于活性顺序图的运行时验证框架 首先获取目标系统执行轨迹，然后获取活性顺序图描述的需求规约，在获取这两者之后，实现基于重写逻辑的运行时验证。 基于活性顺序图的运行时验证框架 1获取系统执行轨迹 2获取需求规约 3运行时验证 基于活性顺序图的运行时验证方法 1插装获取系统的执行轨迹 使用AOP的横切技术在目标系统源代码中设置若干横切关注点实现代码插装，获取系统执行轨迹。 基于活性顺序图的运行时验证方法 2获取活性顺序图描述的需求规约 活性顺序图描述的需求规约包括两种性质：顺序性性质和唯一性性质。文献[48]中的转换过程产生的LTL公式的规模较大。利用图中性质的传递性化简文献[48]转换所得的LTL公式的规模，包括： （1）化简顺序性性质对应的LTL公式的规模 （2）化简唯一性性质对应的LTL公式的规模 基于活性顺序图的运行时验证方法 （1）化简顺序性性质对应的LTL公式的规模 U模态算子引起的偏序关系的化简 同一个消息所引发的多重顺序性性质化简为单个顺序性性质 定义函数 与 函数化简顺序性性质 基于活性顺序图的运行时验证方法 （2）化简唯一性性质对应的LTL公式的规模 建立图中消息事件的唯一性性质时会产生冗余性质，通过以下过程消除冗余性质：给定消息集合 ，其顺序是 ，如果消息 ei从其发生到消息 ek(ik)之间没有重复发生，则 从其产生到任一中间消息 ej(ijk) 之间都不会重复发生，即有： 基于活性顺序图的运行时验证方法 利用（1）和（2）中的化简过程，可以化简因等式2.1转换所得的LTL公式的规模。 使用等式4.3转换产生的LTL公式的规模是图中最大消息规模的平方复杂度。相对等式2.1而言，使用等式4.3的转换过程将有效减少转换所得的LTL公式的规模。 基于LTL三值可执行语义的公式重写算法 为了制定适合重写逻辑的运行时验证算法，重新定义有穷轨迹t上LTL三值可执行语义。 基于LTL三值可执行语义的公式重写算法 算法第1-7行是算法的输入、输出与变量声明。然后根据轨迹 上的状态迭代进行重写过程，第11-16行是操作符的声明，其中，根据Maude工具引擎的特点，在第16行引入“_{_}”操作符的缓存机制提高公式重写效率。第18-19行使用“_{_}”操作符定义可满足操作符，第20-27行是时序操作符的重写过程。 基于Maude的验证算法实现 第一，定义轨迹类型 第二，声明LTL三值逻辑的基本元素 第11行声明公式重写过程中使用的“_{_}”操作符，其memo属性表明在重写过程中将启动该操作符的缓存机制，提高LTL公式重写效率。 基于Maude的验证算法实现 第三，定义布尔逻辑运算符 第四，定义时序逻辑运算符 一种离线方