摘要: 随着计算机技术的发展，各种应用软件逐渐深入到人们日常生活的各个领域。但是应用软件的微小错误都可能对人们造成极其负面的影响，为此提高软件系统的可靠性和安全性是非常重要的。运行时验证作为一种轻量级验证技术，弥补了传统验证技术的缺陷，使... 展开 随着计算机技术的发展，各种应用软件逐渐深入到人们日常生活的各个领域。但是应用软件的微小错误都可能对人们造成极其负面的影响，为此提高软件系统的可靠性和安全性是非常重要的。运行时验证作为一种轻量级验证技术，弥补了传统验证技术的缺陷，使用形式化方法描述性质并将其转换为对应的监控器，然后从被验证系统中提取运行轨迹并交予监控器，最终监控器将判断性质给出结果与反馈。各种时序逻辑被广泛用来描述运行时验证性质，命题投影时序逻辑(Propositional Projection Temporal Logic，PPTL)具有完全正则表达能力，由于运行时验证只能获取系统的有限轨迹，为此一种基于PPTL三值语义(Three-valued PPTL，PPTL3)的运行时监控器构造方法被提出，相应的PPTL3性质监控器生成工具(Property Monitor Generation of PPTL property，PMG_PPTL)被实现并分别应用到离线和在线监控的社交网络系统中。 本文对基于PPTL3的运行时验证监控器进行了研究，提出了监控器的改进方案并在PMG_PPTL中实现。首先，直接地证明了监控器构造算法的正确性，保证了构造算法生成的监控器与PPTL三值语义的一致性。其次，提出了监控器构造算法需要解决的两个关键问题，分别是打结Büchi自动机(Stutter Büchi Automaton，SBA)转换NFA过程中NFA可接受状态的判空操作和构造监控器之前的最小化DFA操作，为此给出了基于强连通分量（Strong Connected Component，SCC）的判空算法和最小化确定有穷自动机状态算法，并且研究分析了改进后PPTL3监控器构造算法的时间复杂度以及空间复杂度。然后，介绍了PMG PPTL中两个算法的实现以及其他改进细节，并将改进前后的监控器进行了一定的对比，结果明显的表明了改进的必要性。随后，提出了基于PMG_PPTL的命题式轨迹监控系统(Propositional Trace Monitoring System，PTMS)和数据式轨迹监控系统(Data-based Trace Monitoring System，DTMS)。PTMS每次离线监控只包含一个性质的监控器，监控的轨迹形式是原子命题的合取，对目标系统的语言没有任何限制。DTMS的一次在线或离线监控均可包含多个性质的监控器，监控的轨迹形式是数据对象，其中离线监控对目标语言没有限制，而在线监控必须是Java。最终，将PMG_PPTL与其他运行时验证监控器进行对比，表明了PMG_PPTL的可用性。 收起