作为一种规范语言,时序逻辑已经被广泛用于计算机程序、数字电路和通信协议的验证以及人工智能的时序推理中。此外,时序逻辑也被用作程序设计语言来编写程序。一个时序逻辑程序设计语言编写的程序称作是一个时序逻辑程序,其本质上是一个时序逻辑公式。跟传统的非形式化编程语言(如Pascal,C等)不同,时序逻辑程序的执行过程是根据给定的规则对公式进行化简的过程。通常时序逻辑程序的执行过程更加复杂,执行效率已经成为影响时序逻辑程序能否应用于实际大型复杂系统的一个关键因素。为此,本文以建模、仿真和验证语言MSVL(Modeling,Simulation and Verification Language)为研究对象,提出了一种MSVL程序的编译执行方法并实现了一个MSVL编译器。在此基础上,研究了基于MSVL和MSVL编译器的C程序验证方法以及自动规划方法。此外,为了支持对C程序的时序性质验证,研究了时序性质自动挖掘方法从程序中挖掘PPTL(Propositional Projection Temporal Logic)性质。本文主要工作概括如下:第一,为了高效执行MSVL程序,提出了一种MSVL程序的编译执行方法并基于该方法实现了一个MSVL语言的编译器,包括词法和语法分析、预处理、语义分析、中间代码生成以及运行时系统实现等。其中针对MSVL中的时序操作符的预处理和并发语句的运行时系统实现是MSVL编译器实现的重点。MSVL编译器可以将一个形式良好的MSVL程序编译为平台对应的可执行码,从而对其进行执行。实验结果表明,对于大型复杂的MSVL程序,编译器的效率要明显高于现有的解释器的效率。基于MSVL编译器,我们实现了对MSVL程序的仿真、建模和验证。最重要的是,编译器的实现为其它工作,例如MSVL的高效运行时验证和MSVL统一动态验证等提供了坚实的基础,反过来,这些工作又为本文中的C程序验证方法提供了基础。第二,提出了一种基于MSVL的动静结合方法来验证C程序的时序性质。该方法采用具有完全正则表达能力的PPTL公式描述期望的性质,从而可以验证一些现有的工具无法验证的性质。此外,在静态分析阶段采用了抽象技术,可以在一定程度上缓解验证过程中的状态空间爆炸问题。最后也是很重要的一点,因为采用了静态的方法查找可能的反例,因此不会产生假阴性(漏报),又因为采用了动态的方法检查虚假反例,因此也不会产生假阳性(误报)。我们基于该方法实现了一个工具SDMC并做实验和现有的相关工具进行了对比。实验结果表明,SDMC在验证一些简单的安全性和活性性质时,比现有的工具效率更高,且可以应用于实际大规模程序的验证,同时SDMC可以验证区间相关和周期重复的性质。第三,性质获取是目前程序验证领域面临的一个难题。为了支持对C程序的性质验证,本文提出了一种动态性质挖掘方法从C程序中自动挖掘时序性质。和现有方法不同的是,该方法采用具有完全正则表达能力的PPTL公式作为性质描述语言,因此可以支持更加复杂的性质,如区间相关性质和周期重复性质。此外,该方法采用了不变式探索工具Daikon挖掘程序中的不变式,因此可以支持挖掘数据相关的时序性质。由于该方法从程序的执行轨迹中挖掘时序性质,而不依赖源程序,因此可以用于其它语言(如JAVA,C++等)程序的性质挖掘。理论上该方法可以挖掘任意长度和复杂度的PPTL性质。为了提高挖掘效率,提出了一种分布式并行性质挖掘方法。第四,将MSVL应用于自动规划领域,提出了一种基于MSVL程序的自动规划方法。该方法同时用MSVL程序描述规划问题和搜索控制知识(Search Control Knowledge,简称SCK),并可以通过对程序编译执行的方式进行规划求解。为了方便用MSVL程序对规划问题进行描述,实现了一种从标准规划域描述语言(Planning Domain Description Language,简称PDDL)到MSVL程序的自动转换方法。我们选取国际规划竞赛中具有代表性的标准规划问题进行了实验,实验表明,在一些依赖SCK的规划问题中,基于MSVL的自动规划方法比现有的大多数规划器所采用的方法效率更高。