基于运行时验证的监控器优化方法研究
发布时间：2021-10-07 16:16
随着计算机软件系统规模的不断扩大和复杂性的逐渐增加,验证软件系统正确性和可靠性的难度也越来越大,传统的验证技术已经无法满足需求。运行时验证是一种提高软件系统正确性和可靠性的轻量级验证技术,是传统验证技术的有效补充,它通过监控软件系统的实际运行状态来验证软件系统是否正确。然而,在运行时验证中,监控软件系统的运行状态通常会产生一些额外的运行时开销,这会对软件系统的性能造成一定的影响。因此,减少运行时验证的开销是运行时验证领域中一个重要的研究内容。本文围绕如何有效地减少运行时验证的开销问题进行研究,具体对运行时验证工具JavaMOP展开研究工作。对JavaMOP进行优化,降低JavaMOP运行时验证的时间和内存开销,提高运行时验证工具JavaMOP的验证效率。本文首先分析JavaMOP验证线性时态逻辑（Linear Temporal Logic,LTL）性质时监控器的构造过程,研究并提出了一种改进的监控器构造方法。该方法使用基于迁移的广义Büchi自动机（Transition-based Generalized Büchi Automaton,TGBA）作为中间的辅助自动机。将LTL性质直接...
【文章来源】：桂林电子科技大学广西壮族自治区
【文章页数】：53 页
【学位级别】：硕士
【部分图文】：
基于监控器的系统验证过程
基于运行时验证的监控器优化方法研究证；监控器与目标系统不同时运行的验证即为离线验证也称为脱机验证，主要是对标系统的历史记录进行分析，排查和修复系统故障。§2.2.3 JavaMOP面向监控编程（MOP）是一种用于软件开发和分析的形式化框架，很多运行验证是在该框架下完成的。在该框架中，使用形式化规范来指定需要的系统行为属性指定的属性自动生成监控器，并集成到目标系统中，验证系统程序的运行状态。当统在运行时违反某个属性时，将触发用户定义的操作，给出反馈信息。图 2-2 是面监控编程框架的分层体系结构。顶层是接口层，为用户提供编程环境；第二层中规处理器用于处理监控器集成；第三、四层包含逻辑插件，由第三层的语言脚本和第层的逻辑引擎组成，用户可以进行添加、删除和修改等操作。
图 2-3 面向监控编程框架的监控模型JavaMOP 是一种基于面向监控编程框架的 Java 软件开发与分析环境，是面向编程框架的一个实例，继承了面向监控编程框架的体系结构。JavaMOP 是一种的运行时验证工具，它为编辑和处理规范提供了 GUI 和命令行接口，支持多种形式的逻辑规范，将处理各种形式化逻辑规范语言的算法以逻辑插件的形式集成avaMOP 运行时验证工具中，如：LTL 插件、ERE 插件、FSM 插件和 CFG 插件等后根据给定系统行为属性的逻辑规范语言，调用对应的插件进行监控系统运行的。另外，JavaMOP 还支持参数化系统监控[19]，因为它支持多种形式化规范，在化监控上完全不受逻辑规范形式的限制。使用 JavaMOP 对系统进行运行时验证，首先根据需要选择合适的形式化逻辑描述系统行为属性，采用 mop 语法编辑生成 mop 格式的文档；然后 JavaMOP 将行为的属性规范转化生成用于监控系统运行情况的 AspectJ 监控代码；再由 Aspe译器[56]将 AspectJ 监控代码插装到目标程序中。图 2-4 即为 JavaMOP 运行时验证程序的过程。在系统运行时验证中，生成的监控器代码观察系统运行的程序，捕属性规范定义的事件，并检查系统程序的运行是否符合给定的属性规范。当出现
【参考文献】：
期刊论文
[1]运行时验证中的减少监控开销方法研究[J]. 徐胜,叶俊民,陈曙,金聪,陈盼. 计算机科学. 2016(05)
[2]运行时验证及其在列车运行控制系统中的应用[J]. 赵林,唐涛,徐田华,柴铭,李宪. 铁道学报. 2011(12)
[3]基于AOP的运行时验证中的冲突检测[J]. 张献,董威,齐治昌. 软件学报. 2011(06)
本文编号：3422371
【文章来源】：桂林电子科技大学广西壮族自治区
【文章页数】：53 页
【学位级别】：硕士
【部分图文】：
基于监控器的系统验证过程
基于运行时验证的监控器优化方法研究证；监控器与目标系统不同时运行的验证即为离线验证也称为脱机验证，主要是对标系统的历史记录进行分析，排查和修复系统故障。§2.2.3 JavaMOP面向监控编程（MOP）是一种用于软件开发和分析的形式化框架，很多运行验证是在该框架下完成的。在该框架中，使用形式化规范来指定需要的系统行为属性指定的属性自动生成监控器，并集成到目标系统中，验证系统程序的运行状态。当统在运行时违反某个属性时，将触发用户定义的操作，给出反馈信息。图 2-2 是面监控编程框架的分层体系结构。顶层是接口层，为用户提供编程环境；第二层中规处理器用于处理监控器集成；第三、四层包含逻辑插件，由第三层的语言脚本和第层的逻辑引擎组成，用户可以进行添加、删除和修改等操作。
图 2-3 面向监控编程框架的监控模型JavaMOP 是一种基于面向监控编程框架的 Java 软件开发与分析环境，是面向编程框架的一个实例，继承了面向监控编程框架的体系结构。JavaMOP 是一种的运行时验证工具，它为编辑和处理规范提供了 GUI 和命令行接口，支持多种形式的逻辑规范，将处理各种形式化逻辑规范语言的算法以逻辑插件的形式集成avaMOP 运行时验证工具中，如：LTL 插件、ERE 插件、FSM 插件和 CFG 插件等后根据给定系统行为属性的逻辑规范语言，调用对应的插件进行监控系统运行的。另外，JavaMOP 还支持参数化系统监控[19]，因为它支持多种形式化规范，在化监控上完全不受逻辑规范形式的限制。使用 JavaMOP 对系统进行运行时验证，首先根据需要选择合适的形式化逻辑描述系统行为属性，采用 mop 语法编辑生成 mop 格式的文档；然后 JavaMOP 将行为的属性规范转化生成用于监控系统运行情况的 AspectJ 监控代码；再由 Aspe译器[56]将 AspectJ 监控代码插装到目标程序中。图 2-4 即为 JavaMOP 运行时验证程序的过程。在系统运行时验证中，生成的监控器代码观察系统运行的程序，捕属性规范定义的事件，并检查系统程序的运行是否符合给定的属性规范。当出现
【参考文献】：
期刊论文
[1]运行时验证中的减少监控开销方法研究[J]. 徐胜,叶俊民,陈曙,金聪,陈盼. 计算机科学. 2016(05)
[2]运行时验证及其在列车运行控制系统中的应用[J]. 赵林,唐涛,徐田华,柴铭,李宪. 铁道学报. 2011(12)
[3]基于AOP的运行时验证中的冲突检测[J]. 张献,董威,齐治昌. 软件学报. 2011(06)
本文编号：3422371
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/3422371.html
