建模仿真验证语言(Modeling,Simulation and Verification Language,简称MSVL)是一种时序逻辑程序设计语言,是投影时序逻辑(Projection Temporal Logic,简称PTL)的可执行子集,其包含丰富的数据结构、函数调用以及同步和异步通信机制,已成功应用于并发系统、反应式系统和嵌入式实时系统的模型描述、路径仿真和形式化验证。作为PTL的命题形式,命题投影时序逻辑(Propositional PTL,简称PPTL)具有完全正则表达能力,能够方便地对顺序、并行、区间相关和周期重复的性质进行描述。基于统一的PTL逻辑框架,现有的方法已经实现了对MSVL程序的运行时验证,用于检测程序的动态执行轨迹是否满足期望的PPTL性质。然而,目前的验证方法存在一些不足:首先,针对单条执行路径的时序逻辑性质验证,没有充分利用当前已经广泛普及的多核设备和分布式网络,导致验证效率不高;其次,针对程序执行中分配的内存区域,没有进行动态追踪,使得程序中存在的内存泄漏问题无法被及时发现;最后,针对含有分支路径的时序逻辑性质验证,不能保证发现的反例是所有路径中最短的,导致验证过程需要探索更多的状态空间。为了解决以上问题,本文围绕MSVL程序的高效运行时验证展开,主要工作概括如下:首先,提出了基于单机多核系统的MSVL程序并行运行时验证方法。该方法将程序执行生成的状态序列分为若干个被同时验证的片段,每个片段由一个线程池负责,线程池中的多个线程同时对一个片段进行验证,当一定数目的片段被验证后,这些片段的验证结果会被及时汇总以检测能否得到最终的验证结果。基于LLVM平台,开发了验证器PPTLCheck,实验结果表明相较于目前的验证工具,PPTLCheck的验证效率更高,并适用于大规模程序的完全正则性质的验证。作为验证实例,研究了多线程程序中多个子线程是否正确交替执行的验证问题,在对问题进行建模和性质描述后,使用PPTLCheck工具对多线程程序的动态执行进行验证。然后,提出了基于分布式网络的MSVL程序并行运行时验证方法。该方法利用分布式网络中性能各异的多核机器对程序执行产生的状态序列片段同时进行验证,在每台机器中,一个片段进而又被分为若干个能够被并行验证的子片段。为了多台机器高效合作,建立了用于消息传递的通信机制和任务分配的调度机制,并给出了一种自适应算法以自动调节不同机器中验证线程的数量。开发了基于局域网的PPTLCheck~+工具,实验结果表明,PPTLCheck~+比PPTLCheck具有更高的验证效率。作为验证实例,研究了SQLite3数据库提供的API在调用过程中是否符合规范的验证问题,为此,开发了SQLite3Check工具,其通过分析网页上描述的API调用规范,得到相应的PPTL公式描述后,使用PPTLCheck~+对调用SQLite3数据库API的程序进行检测。进而,提出了针对MSVL程序内存泄漏的运行时检测方法。该方法采用动态符号执行技术尽可能多地运行程序的不同路径,在每条路径的执行过程中,后端检测器跟踪每个被访问的动态分配的内存块,计算指向每个内存块的指针数量,判断其是否发生泄露,并记录内存泄露位置和指向每个泄露内存块的变量变化情况,在程序执行后,将相应的内存释放语句添加到代码合适位置。基于KLEE工具和MSVL编译器,开发了DEF LEAK工具,实验结果表明,DEF LEAK能够发现更多的内存泄露,并更有效地帮助开发人员理解泄露发生的原因以安全修复内存泄露。最后,提出了含有非确定选择语句的MSVL程序的统一限界运行时验证方法。该方法基于MSVL的统一运行时验证方法和PPTL限界语义,构造深度递增的有界带标记的范式图(Bounded Labeled Normal Form Graph,简称BLNFG),以发现所有分支上违反性质的最短前缀,在资源有限或者不要求整个路径满足性质的情况下,该方法可用于说明在一定的搜索深度内,程序中不存在反例路径。以经典的互斥问题、哲学家就餐问题和银行家算法为案例,说明了所提验证方法对实际问题的有效性。