随着计算机在人类社会各个领域的普及,软硬件系统的正确性问题已经备受关注,在过去的几十年里,形式化验证方法已成为保障软硬件系统正确性的重要途径。其中,时序逻辑由于其简洁和无二义的特性,已经被广泛的应用于形式化验证中。作为一种时序逻辑程序设计语言,MSVL是投影时序逻辑(PTL)的一个可执行子集,可用于对软硬件系统进行仿真、建模以及验证。其中,建模功能作为验证的基础,是MSVL语言中极其重要的一部分。程序设计语言的实现工具主要包括编译器与解释器。其中,编译器的运行速度与内存占用率均优于解释器。本文主要研究如何在编译器结构下为MSVL程序建立模型。MSVL程序模型的建立,一方面以图的形式呈现出程序的执行流程,简单明了;另一方面,模型可以更精准地刻画出程序中的状态迁移,便于后续验证工作的开展。本文的主要贡献在于提出了建模方法的设计框架,并解决了该框架在实现中的关键问题。该框架借助于LLVM编译系统平台,基于MSVL语义,将MSVL语句转化为中间代码(IR)并引入动态控制机制,随后经由链接器生成可执行文件,最终得到程序模型。在框架实现过程中,针对MSVL程序的特点,提出了四种关键技术,包括时序性质的体现、多路径程序的执行、MSVL特有语句的实现以及程序模型的绘制。最后,本文介绍了MSVL建模工具的使用方法,并给出了对经典问题建模的示例,验证了建模框架的可行性。