与轮轨交通技术相比,高速磁浮交通技术更加节能和环保,并且速度也更有优势,是21世纪非常有竞争力的运输系统。随着高速磁浮交通技术的日益成熟及上海磁浮列车的示范运营,磁浮长大干线应用是运输系统的新趋势。如果我国能率先开展长大干线磁浮项目,这将成为全世界的首例。为了更好地发展长大干线磁浮交通技术,本文对磁浮交通长大干线应用中必然产生的磁浮列车追踪安全问题进行研究。首先,本文通过一个简单RSL规约介绍了RAISE语言的一些基本概念,为了更充分地掌握RAISE语言的数学特性,本文还总结了RAISE语言中的固有类型、集合、表、函数、映射及其特殊操作符。同时对如何使用RSL进行系统建模与验证做出了阐述,并且介绍了RSL开发工具和RAISE的推理规则。其次,本文通过对高速磁浮运控系统的结构和功能的研究,发现为了将高速磁浮技术长大干线化,还需要对其功能进行增加,以提高系统的安全,因此本文增加了分区预约防护功能。结合高速磁浮交通的运行特点,总结出高速磁浮系统的多分区追踪场景,对磁浮列车在多分区追踪场景中的运行过程进行了描述。然后,本文对多分区追踪场景的安全需求进行了分析,为了简化模型,本文先对多分区追踪场景进行相应假设,并采用RAISE语言及模块化设计方法对长大干线高速磁浮系统的多分区追踪场景进行RSL建模,同时使用RAISE语言描述系统的安全需求。最后采用RSL验证方法对多分区追踪场景的安全特性进行验证,验证结果表明在长大干线高速磁浮系统的多分区追踪场景中,改进后的高速磁浮运控系统能够保证系统的安全。