随着计算机技术的发展,各种应用软件逐渐深入到人们日常生活的各个领域。但是应用软件的微小错误都可能对人们造成极其负面的影响,为此提高软件系统的可靠性和安全性是非常重要的。运行时验证作为一种轻量级验证技术,弥补了传统验证技术的缺陷,使用形式化方法描述性质并将其转换为对应的监控器,然后从被验证系统中提取运行轨迹并交予监控器,最终监控器将判断性质给出结果与反馈。各种时序逻辑被广泛用来描述运行时验证性质,命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)具有完全正则表达能力,由于运行时验证只能获取系统的有限轨迹,为此一种基于PPTL三值语义(Three-valued PPTL,PPTL3)的运行时监控器构造方法被提出,相应的PPTL3性质监控器生成工具(Property Monitor Generation of PPTL property,PMG_PPTL)被实现并分别应用到离线和在线监控的社交网络系统中。本文对基于PPTL3的运行时验证监控器进行了研究,提出了监控器的改进方案并在PMG_PPTL中实现。首先,直接地证明了监控器构造算法的正确性,保证了构造算法生成的监控器与PPTL三值语义的一致性。其次,提出了监控器构造算法需要解决的两个关键问题,分别是打结Buchi自动机(Stutter BuchiAutomaton,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的可用性。