CTCS-3级列控系统中临时限速服务器的建模与形式化验证

简介：
本文针对CTCS-3级列控系统的复杂性，开展对临时限速服务器的功能建模及形式化验证研究，以确保铁路运行的安全性和高效性。 CTCS-3级列控系统中的临时限速服务器（TSRS）对于高速铁路的安全运营至关重要。该系统的安全性直接影响到列车的运行安全，在研发过程中需要进行仿真建模与验证，以发现并修正设计错误，确保其可靠性。 论文首先分析了CTCS-3级列控系统中临时限速服务器的功能和性能规范，并提取出相应的结构组成。通过使用消息顺序图（MSC）来描绘TSRS与其外部系统的交互行为，清晰地展示了信息传递的流程与条件。接着将这些模型转化为UPPAAL中的时间自动机仿真模型进行形式化验证。 这种建模方法能够确保系统满足预定的安全性和性能标准，确认其在预期条件下能够正确运行且不会出现无限制的行为。通过这种方式，论文为TSRS的设计优化和开发提供了重要的参考依据，并对提升我国高速铁路运营安全水平具有重要意义。