随着计算机系统的广泛应用,软件系统的正确性和可靠性对人类的安全生产和生活至关重要。随着软件系统规模的增长以及复杂性的增加,传统的软件测试方法已经不能满足保障软件可靠性的需求。经过几十年的发展,形式化验证已成为软件可靠性保障的重要方法。在诸多形式化验证方法中,基于时序逻辑的软件系统验证得到了广泛的应用。时序逻辑程序设计语言MSVL由投影时序逻辑发展而来,可用于软硬件系统的建模、仿真和验证。本文主要研究了基于Linux平台的MSVL编译器和MSVL集成开发环境的实现方法。MSVL语言的执行方式不同于常规程序设计语言,其编译器的实现也与常规编译器有着显著区别。MSVL编译器基于LLVM框架开发,使用LLVM中间表示作为中间代码。MSVL程序到中间代码的转换是本文的核心内容,也是MSVL编译器实现过程中的难点所在。本文首先介绍了编译器的框架设计和实现,随后介绍了MSVL语句到LLVM中间表示的转换方法。MSVL集成开发环境的实现是本文另一项工作内容。MSVL集成开发环境基于Eclipse平台开发,为Linux平台上MSVL工具提供了图形界面。在本文的最后展示了通过命令终端和MSVL集成开发环境使用MSVL编译器的方法和效果。