实时系统经常被用在飞机、军事以及交通控制等安全攸关的领域，因此保证其正确性和安全性至关重要。建模、仿真及验证语言（MSVL）是一种基于投影时序逻辑（PTL）的时序逻辑程序设计语言，它可用于对计算机软、硬件系统进行建模、仿真和验证。但由于PTL和MSVL中缺乏对量化时间的描述能力，因此，很多实时系统及其性质无法被描述。本文通过对PTL和MSVL的实时扩展，得到的实时建模、仿真及验证语言（TMSVL）可以对实时系统进行建模、仿真和验证。首先，介绍了PTL和MSVL的语法和语义及其相关理论；然后，通过定义时间约束区间将PTL扩展为可以描述量化时间约束的实时投影时序逻辑（TPTL），形式化定义了TMSVL的语句和程序，并给出了TMSVL的操作语义，还利用TMSVL基本语句定义了实时系统中常见的中断、超时和延时等概念；接着，通过一个视频点播系统的例子来说明利用TMSVL对实时系统进行建模和性质验证的具体方法；最后简单介绍了为辅助建模和验证而开发的一个TMSVL解释器原型。