MSVL（Modeling,Simulation and Verification Language）是一种时序逻辑程序设计语言,是投影时序逻辑（Projection Temporal Logic,PTL）的可执行子集。MSVL主要用于形式化建模、仿真和验证并发系统以及交互式系统,但其不能有效地建模和表达实时系统中的时间约束和中断等行为以及和时间相关的性质,使其在实时系统中应用受到限制。本文对MSVL语言进行扩展,得到了可以建模实时系统的语言TMSVL（Timed MSVL）,并为TMSVL开发了解释器（模型检测工具）。使用TMSVL实现了对单速率调度（Rate-monotonic Scheduling,RMS）算法、基于μC/OS-Ⅲ的实时系统、基于ROS（Robot Operating Systems）的人工智能系统以及多级中断系统的建模、仿真和验证。本文围绕定义TMSVL语言的逻辑、TMSVL语言的语义、工具实现以及对TMSVL语言的应用展开,主要工作概括如下:第一,针对PTL不能定义连续时间中的时间约束和强制终止或者超时的问题扩展PTL,从而得到其基于时间的扩展形式TPTL（Timed PTL）。TPTL主要从以下三方面扩展PTL:（1）在PTL中引入代表时间的变量T和代表时间长度的变量Ts来建模实时系统的时间,二者的取值均为非负实数;（2）定义时间约束操作符来限制被约束公式的时间长度,它可以描述连续时间概念下的时间约束;（3）定义cut操作符来描述强制终止或者超时。接着,本文给出并证明了 TPTL中包含时间约束和cut操作符的公式的逻辑规则。TPTL的提出为定义实时系统建模语言从而验证实时系统提供了形式化（模型）语义。第二,为了建模、仿真和验证实时系统,本文使用TPTL定义了扩展的MSVL语言,即TMSVL。TMSVL不仅包括了MSVL中的所有语句,还包含了建模实时系统的时钟语句、cut语句、延时语句、超时语句和中断语句。本文证明了所有的TMSVL语句都可以转化为范式,并给出了TMSVL语句转化范式的方法。定义了TMSVL语言的操作语义,给出了表达式的求值规则和扩展语句的语义等价规则,并通过证明TMSVL语言操作语义和模型语义的一致性来确保操作语义的正确性。使用TMSVL语句,可以建模实时系统中的延时、定时响应、任务截止时间、强制终止、超时和中断等时间约束行为。第三,为了自动化实时系统的建模、仿真和验证过程,本文基于TMSVL语言的操作语义,开发了TMSVL解释器。该工具通过扩展MSVL解释器而得到,使其支持了对时钟语句、cut语句、延时语句、超时语句和中断语句的词法分析、语法分析以及语义分析。该解释器具有三种工作模式（建模、仿真和验证）:在建模模式下,可以得到程序的带标记的范式图（Labeled Normal Form Graph,LNFG）,它描述了程序的状态空间;在仿真模式下,可以得到程序的一条执行路径;在验证模式下,可以验证系统是否满足给定性质。TMSVL解释器为模型检测实时系统提供了新的工具支持。第四,在实时系统的设计中,确保任务的实时性以及中断处理的安全性是一项关键且复杂的工作。本文以经典调度算法RMS为例,将TMSVL语言应用到基于RMS算法的任务集的可调度性检测上。该方法提供了检测RMS算法可行性的充分必要条件,而且可以解决一系列任务集的可调度性检测问题。此外,本文将提出方法应用到基于μC/OS-Ⅲ的实时系统的可靠性验证上。以基于μC/OS-Ⅲ的实时系统为研究案例,分别使用TMSVL建模了包含多任务同步的实时系统和包含中断的多任务实时系统,并成功地验证了这些系统中任务的实时性以及系统的安全性。接着,本文研究了如何将TMSVL语言及其模型检测方法应用到建模和验证基于ROS的人工智能系统上。最后,本文研究了如何使用TMSVL形式化建模多级中断系统。基于TMSVL中的基本中断语句,给出了建模多级中断系统的方法。该方法为多级中断系统提供了形式化语义,使得可以对这类系统进行模型检测,从而形式化验证其实时性和安全性。