一种基于活性顺序图的运行时验证研究

摘要

随着计算机技术的发展，软件系统的可靠性问题越来越受到人们的重视。尤其对于安全关键系统，如何提高此类软件系统的可靠性已成为一个非常重要的研究方向。测试方法可以提高系统的可靠性，但其存在不完备性问题。模型检测具有完备性，但是需要建立系统的抽象模型，而且对于复杂系统来说，模型检测容易产生“状态空间爆炸”等问题。运行时验证技术是传统验证方法的有效补充，能够尽早地发现软件系统故障，有助于提高软件系统的可靠性。运行时验证关注的是软件系统的实际执行是否满足待验证的需求规约，使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点，目前基于可视化需求规约场景的运行时验证技术还存在以下不足:
　　(1)已有的验证方法容易产生冗余性质，验证开销较大，且二值语义的验证结果是不准确的。
　　(2)已有的基于Maude工具引擎的重写逻辑运行时验证算法的效率较低，不利于快速的发现系统故障。
　　针对现有的运行时验证技术存在的不足之处，本文的主要工作有:
　　(1)分析已有的验证方法的不足，提出一种基于活性顺序图的运行时验证的改进方法。该方法使用代码插装获取系统执行轨迹，使用活性顺序图描述需求规约场景，为了支持现有的运行时验证技术，基于活性顺序图到LTL公式的基本转换过程，利用图中性质的传递性化简转换所得的LTL公式的规模，然后基于有穷轨迹上LTL三值可执行语义，实现针对系统执行轨迹的离线方式的运行时验证。
　　(2)针对基于Maude工具引擎的重写逻辑运行时验证算法的效率较低问题，使用轨迹状态消耗的思想，根据Maude工具引擎的特点，引入操作符的缓存机制，提高公式重写的效率，以便快速的发现系统故障。
　　(3)设计验证工具和完整的实验实例，为了证明本文提出的改进方法的可行性，本文设计并实现了运行时验证工具RVT4LSC，并使用该工具验证ETCS-2级列车运行控制系统中RBC/RBC切换场景，实验结果证明了本文改进方法的可行性。然后进行了对比性实验，实验结果表明，本文采用的转换方法将产生更小规模的LTL公式，能有效降低运行时验证的开销。

目录

声明

摘要

第一章 绪论

1．1 课题研究背景

1．2 当前的研究现状

1．2．1 国外的研究现状

1．2．2 国内的研究现状

1．2．3 存在的问题

1．3 本文的研究目标与工作

1．4 论文的组织结构

第二章 研究基础

2．1 运行时验证理论

2．1．1 运行时验证方法

2．1．2 在线验证与离线验证

2．2 活性顺序图

2．2．1 活性顺序图的基本组成

2．2．2 活性顺序图的形式化定义

2．3 线性时序逻辑

2．3．1 LTL语法

2．3．2 有穷轨迹上的LTL语义

2．3．3 有穷轨迹上的LTL三值语义

2．4 活性顺序图到LTL的基本转换

2．5 面向方面编程

2．6 Maude工具引擎

2．7 本章小结

第三章 基于活性顺序图的运行时验证框架

3．1 获取系统执行轨迹

3．2 获取需求规约

3．3 运行时验证

3．4 本章小结

第四章 基于活性顺序图的运行时验证方法

4．1 插装获取系统的执行轨迹

4．2 获取活性顺序图描述的需求规约

4．2．1 化简顺序性性质对应的LTL公式的规模

4．2．2 化简唯一性性质对应的LTL公式的规模

4．2．3 活性顺序图到LTL转换过程的化简

4．3 基于LTL三值可执行语义的公式重写算法

4．4 基于Maude的验证算法实现

4．5 相关工作对比

4．6 本章小结

第五章 一种离线方式验证工具的设计与实现

5．1 工具架构

5．2 插装获取系统执行轨迹模块实现

5．3 需求规约导入模块实现

5．4 运行时验证模块实现

5．5 本章小结

第六章 实验及其结果分析

6．1 功能性实验

6．1．1 实验样例设计

6．1．2 需求规约建模

6．1．3 验证过程

6．2 对比性实验

6．3 本章小结

第七章 总结和展望

7．1 本文工作的总结

7．2 进一步的研究工作

参考文献

附录

在校期间参加的科研项目和发表的论文

致谢