随着计算机技术的蓬勃发展,各种应用软件已经成为人们生活中的重要组成部分,如何提高软件的可靠性与安全性则成为了计算机领域中的重要挑战。验证作为一类用以说明一个系统是否满足其性质描述的技术,被广泛的应用于软件可靠性与安全性的检查中,其中,测试与模型检测已经应用于软件系统的验证中,并成功攻克了很多难题,但目前仍然存在一些不足:测试只能证明软件中存在错误,而不能证明其中不存在错误,且测试用例较难设计;模型检测中模型较难提取,且抽象出的模型与实际系统可能存在不一致的问题,并且在系统规模庞大的时候,容易产生状态空间爆炸问题。针对上述问题,一种轻量级的自动化验证技术被提出来,在运行时验证（Runtime Verification,RV）中,利用时序逻辑公式描述系统应满足的性质,并据此构建监控器,然后监控系统的运行轨迹,该轨迹信息的获取方式可分为在线获取与离线获取两种,在实际应用中,所对应的方法分别是代码插桩与查看日志文件,最终根据监控到的数据来验证系统的本次运行是否满足该性质。由于在RV的应用中,是通过检查系统运行轨迹的有穷前缀来进行验证,在获取的数据不足时,无法给出明确的验证结果,因此传统的二值语义并不适用,需要将其扩展为三值语义。此外,还存在着性质描述语言表达能力不足的问题,这会导致一些性质无法被描述。相对而言,命题投影时序逻辑（Propositional Projection Temporal Logic,PPTL）的表达能力较强,且带星操作的PPTL具有完全正则表达能力。在此基础上,本文提出了一种基于三值语义PPTL（PPTL₃）的运行时验证方法:对于软件系统,不需抽取建立其相应的模型,只需获取其运行时产生的信息即可;而对于根据系统需求所抽象出的待验证性质,利用上述定义的PPTL₃公式来描述,然后利用范式以及自动机相关的理论将其转化为监控器。基于上述的理论研究,本文提出了一个基于PPTL₃的运行时验证中监控器的构造方法:首先,根据系统需求抽象出需要验证的性质φ;然后根据范式与范式图的理论,将φ与?φ重写为等价的范式并进一步表示为范式图的形式;进一步通过对范式图中结点添加一个有穷的标记来说明因chop操作符之前的公式只存在无穷模型而导致整个公式不存在相对应模型的问题;在转换得到打结Büchi自动机之后,通过改变其接收状态集来重新定义一个非确定有穷自动机,进而求得与其等价的确定的有穷自动机;最终将两个有穷自动机做乘积以得到最终的监控器。根据该流程,本文利用Java语言编程实现了该工具,并通过一个文件操作相关的例子说明了监控器构造算法的可用性。