在众多计算机应用领域中，铁路车站联锁系统不仅是实时系统，而且还是安全—关键系统。这种系统和航天、核工业、军事等应用系统具有一个重要的共同特征，就是它们的正确运行与否关系到人的生命安危和大量财产损失或生态环境的破坏。这种系统的时间参量非常重要，但是系统运行是否安全更关键。因此，在计算机技术和智能控制技术得到充分发展和应用的今天，对铁路车站联锁系统进行完备的形式化描述越来越受到重视。现有对铁路车站联锁系统的形式化描述工具主要是petri网和扩展petri网相关技术。但是现有技术大多数限于满足逻辑的准确性及模型的简化，添加时间约束的建模和模型分析还鲜见报道。本文主要研究铁路车站联锁系统的形式化建模和模型分析。在现有的时间petri网模型和有色petri网模型基础上，结合区间时间有色petri网(IntervalTimed Colored Petri Nets，简称ITCPN)对铁路车站联锁逻辑进行建模和模型分析。ITCPN使模型更接近实际系统(加入运行时间区间，即时延用上、下边界来规定)。本文主要以铁路车站联锁系统作为实际研究案例，但是同时也不失一般应用的案例描述。文中用充分的理论认证和实践案例证明了ITCPN是适合描述安全—关键系统的，并且可以对其模型进行分析。