由于计算机系统在各个领域的广泛使用,软硬件系统的可靠性和正确性对人类生产和生活至关重要。历经数十年的发展,形式化验证已经成为保证软硬件系统可靠性的关键方法。在诸多形式化验证方法中,基于时序逻辑的验证方法得到了普遍的运用。时序逻辑程序设计语言MSVL（Modeling,Simulation and Verification Language）是投影时序逻辑（Projection Temporal Logic,PTL）的一个可执行子集,可用于软硬件系统的建模、仿真和验证。目前,关于MSVL和PTL的研究比较成熟,已经开发了一个基于MSVL和PTL的形式化验证平台MSV。MSVL已有的编辑工具是简单的纯文本编辑器,缺少视觉增强的代码效果和智能感知编辑功能。为了使MSVL能够更好地服务于系统形式化验证,需要为MSVL开发一个功能完善且用户友好的智能辅助编辑器,以提高用户的编程体验和编程效率。针对以上问题,本文的主要工作是实现一个基于语法制导的MSVL智能编辑器VS Code-MSVL。构建在Visual Studio Code这一主流开源编辑器上,VS CodeMSVL是一个全新轻量级的集成开发环境,可用于MSVL程序的智能编辑、编译运行、建模验证和错误调试。MSVL编辑器的主要特点有:1.视觉增强的编辑效果:支持基于MSVL语法语义的高亮显示、括号环绕、代码折叠、提示错误或警告的代码装饰、代码建议的类型图标等增强效果。2.丰富的智能编辑体验:支持上下文感知的自动补全、动态函数签名、悬停提示信息、快速文件导航等编辑功能,提高了开发体验和效率。3.实时的动态代码诊断:基于语言服务器协议,将代码编辑进程和代码检测进程解耦,在正式编译前实现了动态的轻量级检测,提高了开发质量。MSVL编辑器的实现是本文的主要内容,编辑器有两大核心功能:智能编辑和错误诊断。通过VS Code的语言扩展为MSVL语言提供了上下文相关的智能感知编辑功能;基于开源的语言服务器协议,通过MSVL语言服务器将编辑进程和程序分析进程解耦,实现对MSVL代码的错误诊断。本文围绕着编辑器的核心功能,对编辑器的总体结构和具体实现进行详细的说明和介绍,并提出针对难点的解决方案。最后展示了MSVL编辑器的功能和效果,给出在该环境下开发MSVL程序的应用示例,并与基于的Eclipse的MSVL IDE进行比较,说明了该编辑器的可用性和实用性。