随着计算机硬件技术和相关软件技术日益成熟,软件在人们日常生产生活中扮演着越来越重要的角色,并在工业、通讯业、医疗、军事和航空航天等方面也得到了广泛的应用。软件系统在很多重要领域的应用使得这些领域对软件系统的依赖不断增加,这就使得计算机的应用环境变得更加复杂,比如软件系统的规模变得越来越大,复杂度也变得越来越高。但是,计算机软件不可避免的存在着各种漏洞,这将严重影响人们在生产和生活中的各项活动。因此,提高软件的可信性和正确性,构建高可信性软件已经成为了近几年软件研究开发方向的热点问题。运行时验证作为一种轻量级的验证技术可以作为传统验证技术的有效补充,这也使得运行时验证技术在软件可信性的领域中得到了广泛的应用。它的主要特点是在软件系统的运行过程中进行验证,这也为实时纠正软件错误奠定了基础。本文对软件可信性运行时验证理论进行了细致的分析研究,对运行时验证的线性时序逻辑(Linear Temporal Logic,以下简称LTL)、自动机理论和运行时验证工具等部分进行了分析研究。针对运行时验证监控器的构造,本文采用了运行时验证工具面向方面编程中的JavaAOP技术和AspectJ技术实现了监控器的设计,这种方法基于自动机转化算法,利用自动机转化方法将语义表达的属性转化为运行时验证监控器。其中,使用JavaAOP技术实现了对软件系统的函数进行运行时的监控,使用AspectJ技术实现了对软件系统的变量进行运行时的监控。并具体实现了监控代码插装及事件、条件计算等问题。本文实验在Windows操作系统平台下对文中提到的运行时验证监控器进行具体实现,实验表明,该监控器在实现对软件系统中函数和变量进行运行时监控的同时也兼顾了软件运行速度等问题。