基于UPPAAL的RBC系统控车流程建模分析-交通信息工程及控制专业论文.docxVIP

中文摘要 摘要：RBC系统是中国铁路CTCS一3级列控系统中的重要组成部分，UPPAAL是 基于时间自动机理论的实时系统建模分析验证工具，使用UPPAAL分析RBC系统 控车流程，可以验证流程的特性，对于保证RBC系统控车流程的安全性有着重要 的实际意义。 论文完成的主要工作如下： 1．介绍了时间自动机理论及其模型检验工具UPPAAL的使用方法。 2．通过分析列车在RBC系统控制下的运行过程，把RBC系统控车流程分为 五部分：列车登录流程，正常控车流程，RBC交接流程，列车注销流程和消息重 发流程。 3．基于时间自动机理论对RBC系统控车的五个流程以及其他外部设备分别 进行了建模：根据研究对象的特点，在合理的抽象和假设之后，确定了各个模型 的状态，状态跳转路径和状态跳转的约束条件，得到了RBC系统控车流程的时间 自动机模型。 4．使用UPPAAL对RBC系统控车流程的时间自动机模型进行了分析验证： 通过设置通道和全局变量，构造了时间自动机的积；使用模拟器，模拟了RBC控 制列车运行过程，分析RBC控制列车运行过程中的状态变化；使用验证器，通过 快速有哪些信誉好的足球投注网站整个系统的状态空间，验证RBC系统控车流程的活性和J下确性等各项特 性。 关键词：CTCS．3列控系统；RBC；时间自动机；UPPAAL；建模分析 分类号：U284．44  AB STRACT ABSTRACT：RBC system is an important component of Chinese Train Control System Lecel 3(CTCS-3)．UPPAAL is a modeling,analyzing and verifying tool for real—time system based on Timed Automata Theory．It is possible to verify some properties of RBC system train-control process of RBC by using UPPAAL，and it is significant for guaranteeing the safety of train-control process． The major works of this thesis are summarized as following： 1．This thesis introduces Timed Automata Theory and the method of using this model．test tool UPPAAL． 2． By analyzing train eontrol process，there al e 5 parts of train—control process： train login process，normal control process，RBC handover process，train logout process and message reserld process．Based on these 5 processes，RBC can control a train． 3．The models of these 5 processes and other external equipment based on Timed Automata Theory are established．After reasonable abstract and assumption，the states of each process，states transition path and constraints are determined based On Timed Automata Theory,SO as to obtain the timed automata model of the 5 process． 4． UPPAAL is used to analyse and verify these 5 timed automata models．By setting channel and global variables，the product of timed automata is obtained．By using Simulator,the process of RBC control train is simulated，and analyzing the state transition of RBC train control process is analyzed．By using Verifier，via q