摘要: 随着软件系统日益复杂，提高软件可靠性也迫在眉睫，在严重的情况下会给国家安全、经济带来不可估量的损失。然而在提高软件可靠性方面，传统的模型检测容易出现“状态空间爆炸”，测试技术容易出现测试用例不完备的情况，都不能保证程序能够正确运行。... 展开 随着软件系统日益复杂，提高软件可靠性也迫在眉睫，在严重的情况下会给国家安全、经济带来不可估量的损失。然而在提高软件可靠性方面，传统的模型检测容易出现“状态空间爆炸”，测试技术容易出现测试用例不完备的情况，都不能保证程序能够正确运行。而基于线性时序逻辑（LTL）的运行时验证技术，通过将系统的实际运行和形式验证有机的结合起来，构造运行时验证监控器以实现对程序的监控，保证程序能够正确的运行。但传统的监控器主要是依据LTL二值语义进行构造，其在语义一致性方面存在问题，因此论文将基于LTL三值语义（LTL3）构造运行时验证监控器。 首先，由于LTL只具备单个时态的时序运算符，导致在很多情况下对性质规约的描述不够简洁和自然，故论文在LTL的基础上融入了表示过去时间的时序运算符，与PLTL不同的是，对两种时态的运算符用移动时间的概念重新加以定义，使它们能够互相融合且具有统一的语义基础，从而得到基于移动时间的线性时序逻辑LTL-P，对性质规约的描述会更自然、更简洁。 其次，由于LTL-P具备两种时序逻辑运算符，不能直接转化为Büchi自动机，而构造运行时验证监控器需要使用Büchi自动机作为过渡，故论文首先将LTL-P公式转化为双向交换自动机，之后再转化为Büchi自动机。另外还对Büchi自动机采用MCS算法和RRS算法进行优化，有效降低了最终所生成监控器的规模。 最后，论文进行了基于LTL-P监控器的运行时验证实验。在实验中，首先根据第三章中基于LTL-P的监控器构造方法，实现了LTL-P公式与双向交换自动机之间以及监控器构造过程中的各种自动机之间的转化，构造了LTL-P运行时验证监控器，然后设计了一种运行时验证基本框架，实现了LTL-P公式到自动机的转化、监控器的构造、监控器的织入、对目标程序的运行时验证四个过程的统一，同时根据此框架开发了相应的便于操作的原型工具，完成了基于LTL-P监控器的运行时验证实验。另外，对工具JavaMOP采用添加LTL三值语义逻辑库的方式进行扩展，使得生成的运行时验证监控器能够依据LTL三值语义对目标程序进行运行时验证。 收起