实时系统作为一种在现实中广泛使用的反应型系统，因其大多使用于安全攸关的领域，所以必须保证它的安全可靠。为了它到这个目的，必须使用具有严格数学基础的形式化方法。在本文中，我们首先对形式化方法作了一个概要的介绍。但是因为它又有别于一般的反应型系统，所以我们接着介绍了实时系统的特殊性，并且介绍了形式化方法面向实时系统的扩展。 为了描述实时系统的性质和行为，各种不同的实时逻辑如MITL、RTTL、TPTL等相继提出，在本文中，我们对此作了一个较为细致的回顾。但是不论是基于点语义的实时逻辑还是基于区间语义的实时逻辑，均不能以很直观的方式来描述实时系统，特别是对那些有事件反复出现的反应式实时系统更难于描述。 基于上述考虑，在本文中，我们提出了由区间的无限序列组成的区域的概念，定义了区域的一些一元运算和二元关系。在此基础上，我们对于基本的命题线性时态逻辑PLTL的核心进行了实时扩展，给出了一个具有连续语义的实时区域时态逻辑(Real-time Region Temporal Logic)，简记为RRTL，定义了RRTL的语法和语义，并且给出了一个形式化的公理系统，建立了RRTL的形式化语义模型，在我们给出的语义解释下，证明了公理系统的合理性。作为它的一次实际应用，我们用它对于实时系统中的一个典型实例：GRC(Generalized Railroad Crossing)进行了描述，给出了它的系统规约，在此基础上，演绎式的证明了系统的一个安全性和活性命题。最后简要介绍了我们开发的一个简单的区域求解工具来辅助我们的演绎式推理。