C语言是一门通用的高级程序设计语言。C语言以其灵活高效、功能丰富和可移植性强等优点,广泛应用于系统软件与应用软件的开发中。然而程序错误在C程序中屡见不鲜,有些错误甚至会导致严重的后果。随着软件规模日益庞大,提高C程序的正确性和可靠性变得愈发重要。MSVL是基于投影时序逻辑的时序逻辑编程语言。可以用于较大规模的软硬件系统建模、仿真和验证。MSVL语言执行效率高,逻辑表达能力强,提供了一种程序验证的新途径。通过将C程序转化为同语义的MSVL程序,再对MSVL程序进行建模、仿真和验证,可以间接验证源C程序的正确性。本文主要研究C-to-MSVL转换系统实现中的关键问题,主要工作如下:1.研究了C语言和MSVL语言的异同,定义了适用于转换系统的C语言标准——Xd-C,并对Xd-C与ANSI C主要的差别进行了阐述,为后续转换提供了理论基础。2.对转换系统的设计框架和执行流程进行优化,并对优化后的转换系统进行了详细的介绍。依照功能将C-to-MSVL转换系统分成预处理模块、词法分析和语法分析模块、转换模块、后期处理模块和集成模块五大模块,并对各个模块的功能及实现细节进行了详尽的说明。3.解决了转换系统实现过程中遇到的问题,对函数指针问题、结构体问题和自定义类型问题等关键问题进行了具体的描述,对解决方案进行详尽的解释说明并悉数实现。4.通过快速排序的例子介绍了C-to-MSVL转换系统的使用方法,并通过对anti_collisionRFID和cJSON两实例进行转换并对比结果,证明了本转换系统的可用性与实用性。