基于MSC与UPPAAL的列控系统等级转换场景形式化验证

摘要

等级转换是C3级列控系统的重要场景，是列控系统兼容性的集中体现，转换的成功与否直接关系到列车的运行安全和行车效率。因此，有必要对设计规范中所描述的转换过程进行形式化建模和验证，以保障系统的安全性和实时性。为保证设计规范与所建模型的一致性，采取消息顺序图( MSC)与时间自动机相结合的方式，建立等级转换场景中C2级向C3级转换过程的MSC模型，并将其转换为时间自动机模型。应用UPPAAL对模型的安全性和受限活性进行仿真验证，结果表明设计规范中所描述的转换过程是安全可靠的，可以满足C3级列控系统的兼容性和安全性要求。%Level transition is one of the most important scenarios in CTCS-3 control system and the very reflection of its compatibility. The successful transition is directly related to train operation safety and transportation efficiency. Therefore, in order to guarantee the security and real-time performance of the system, it is necessary to formally build and verify a model of transition process described in the design specification. To ensure the consistency between of the design specification, the message sequence configure ( MSC) is combined with timed automata, the MSC model is established for C2 to C3 transition process in level transition scenario and is transformed to timed automata model. Then the security and restricted activity of the model are simulated and verified by applying UPPAAL validation tool. The results show that the transition process described in the design specification is safe and reliable to meet the requirements of compatibility and security in CTCS-3 system.