实时系统被广泛地应用在一些重大、紧急的事件的处理中,例如智能机器人、航天系统和铁路调度系统等。实时系统一旦发生错误,后果往往是十分危险甚至可能是灾难性的,这要求实时系统必须具备较高的正确性保证系统中各模块具体的响应时间。模型检测技术对于实时系统的可靠性的检测有很好的帮助。但目前已有的模型检测时态部分的实时拓展主要是基于传统时态逻辑之上进行拓展的,缺乏正则属性的表达能力,无法描述复杂实时系统的一些行为。为此,本文在线性动态逻辑(Linear Dynamic Logic,LDL)的基础之上添加时间区间约束,提出一种具有表达离散实时性质和所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL),因此它能够很容易地描述一些复杂实时系统的行为。然后基于构造测试器的方法提出离散实时线性动态逻辑的符号化模型检测算法,接着将所构造的测试器翻译成具体的smv程序模块,在著名模型检测工具nuXmv上运行该测试器的smv模块,实现所提出的算法。本文的主要工作如下:(1)提出离散实时线性动态逻辑RTLDL,它是LDL实时性的扩展,使得LDL能够表达和分析系统的实时行为;(2)借鉴程序控制流标记的思想为基本的时态算子构造时态测试器,解决LDL的模型检测问题。在此基础上进一步构造有界时态公式的测试器,提出了一种基于测试器的RTLDL符号化模型检测算法;(3)在模型检测器nuXmv上使用翻译方法实现并验证我们的算法。实验结果表明,在验证RTLDL公式时,我们的方法在变量、状态空间以及时间方面均明显优于目前唯一实现LDL模型检测的模型检测工具MCMAS-LDLK,特别是对于不包含有界的测试公式嵌套在柯林星中的RTLDL公式验证,我们的算法效果指数级地优于MCMAS-LDLK。