为了提高大规模软件系统的可靠性和安全性,程序的形式化验证受到广泛关注。传统模型检测方法需要从源代码中提取模型,然而,随着程序规模增大以及结构的复杂化,从程序中提取模型变得异常困难,任何一个错误都可能造成模型和源程序的不一致。近年来,源代码级别的形式化验证已成为一个重要的研究课题。其研究主要分为以下三个方向:第一,可达性分析方法,该方法在待验证程序中插桩错误标签,然后通过分析错误标签的可达性来验证程序是否满足指定性质,然而该方法仅能进行安全性验证,而无法验证诸如活性的其他时序性质。第二,静态软件模型检测方法,该方法不执行程序,静态检测程序所有路径,从而使得较小规模程序都可能产生很大的状态空间,因此很难验证大规模程序,且验证效率不高。而且由于没有程序的执行信息,导致精确性不够,可能产生误报。第三,运行时验证方法,在执行程序时提取事件信息,构造监控器来检测当前的执行路径是否满足指定性质,由于每次只验证一条路径,避免了状态空间爆炸问题。尽管在代码级别程序验证方面已有一些研究工作,然而现有技术并不成熟,现有验证工具仍无法处理大规模应用程序。本文围绕代码级别的形式化验证方法进行研究,主要工作如下:1.为了对大规模的程序进行时序性质的验证,提出了一种基于动态执行的程序时序性质验证方法,该方法使用建模、仿真和验证语言（Modeling,Simu-lation and Verification Language,简称MSVL）编写程序₈),以命题投影时序逻辑（Propositional Projection Temporal Logic,简称PPTL）公式来描述性质,然后将性质的非?转换成程序^′₈),因此,验证₈)是否满足即为检测新的程序“₈)and^′₈)”是否存在可接收的执行路径。使用MSVL编译器对“₈)and^′₈)”进行编译,生成可执行码（69）（9^′.0）0),使用动态符号执行工具产生“₈)and^′₈)”的输入,执行（69）（9^′.0）0),最终可以得到验证结果。进一步,我们采用并行机制处理程序的不同执行路径以提高效率。基于该方法开发了工具UMC4M,将其集成到了MSV工具平台,并分别对23个小规模程序、6个中等规模程序以及10个大规模程序进行验证,实验结果表明,使用MSV对程序进行时序性质验证时,其效率优于现有工具如T2、RiTHM和LTLAutomizer。2.为了使用验证工具UMC4M对C程序进行验证,提出了将C程序转换成MSVL程序的转换方法。我们将C语言的语法限定在一个合适的子集上,该子集称为Xd-C,Xd-C去除了C语言中容易出现错误的、冗余的结构,表达能力和C语言相同。由于MSVL语言的数据类型和语句包含Xd-C中的所有数据类型和语句,因此,Xd-C程序到MSVL程序的转换可以一对一进行。针对Xd-C程序的声明、表达式以及语句,我们分别提出了对应的转换算法,从而得到了将Xd-C程序转换为MSVL程序的转换算法。另外,我们定义了Xd-C和MSVL状态、表达式和语句之间的等价关系,并且基于Xd-C和MSVL的操作语义,分别采用了结构归纳法以及规则归纳法证明转换前后表达式和语句的等价性,进一步证明了原Xd-C程序和转换后得到的MSVL程序的等价性。基于这些算法,我们开发了Xd-C程序到MSVL程序的转换工具C2M,并且通过转换13个实际的大规模Xd-C应用程序对工具的有效性进行评估。实验表明,该方法可以正确且高效地进行程序转换。3.将动态执行程序的形式化验证方法应用于软件系统的验证,包括虚拟内存管理系统和安全攸关软件系统的调度协议的验证。本文对虚拟内存管理系统进行研究,使用MSVL对虚拟内存管理系统的内存管理单元处理程序、页面失效处理程序以及外部页面调度程序进行形式化描述,从而得到整个虚拟内存管理系统的描述。进一步,对该系统的安全性、可靠性等性质进行验证,如用户进程不允许访问内核空间,用户进程访问用户空间时,虚拟地址总是可以成功转换成物理地址。此外,本文将提出的方法应用到安全攸关系统的调度协议中,使用MSVL程序分别对系统的时钟模块、任务模块、中断模块和调度模块进行建模,然后根据各模块之间的逻辑关系,得到系统的模型,进一步,通过定理证明和基于动态执行的程序验证两种方法,验证了该系统的可调度性、任务调度互斥性、最高优先级任务最先调度等性质。