列车监控系统在城市轨道交通中的应用

随着城市人口的不断增加,人民生活水平的不断提高,采用快捷、舒适的交通工具已成为人们出行的基本要求。因而,城市轨道交通以其快捷、高密度、高效率等特点成为城市交通的一个重要构成部分,正在中国的各个大中型城市快速发展。城市轨道交通包括地铁及轻轨交通,由于自身的特点,列车运行的人工管理很难适应它的要求,计算机自动化管理就成为城市轨道交通的必然要求。列车监控系统作为计算机自动调度管理控制系统,是城市轨道交通不可缺少的部分。列车监控系统在城市轨道交通中称为自动列车监控系统(ATS,Automatic Train Supervision)。

基于Event-B与ADT的TACS形式化开发方法与验证

为克服Event-B方法在开发全新一代列车自主运行控制系统(Train Autonomous Circumambulate System,TACS)中所出现的建模复杂性问题,提出将抽象数据类型(Abstract Data Types,ADT)实例化与Event-B相结合的方法,对TACS进行形式化开发和验证。首先,根据TACS的需求以及案例研究等相关内容,提取TACS的功能需求和安全需求,并将功能需求和安全需求以非形式化的语言进行描述;然后,根据TACS的功能需求和安全需求进行模型精化层次的设计,避免因在抽象模型中建模复杂的需求而导致证明困难;最后,在模型中使用形式化语言Event-B对TACS的功能需求和安全需求进行建模并验证其正确性,且在建模过程中,利用ADT的抽象概念将轨道网络、轨道区域以及移动授权(Movement Authority,MA)等复杂系统组件在初始模型中指定组件的必要属性,且在后续系统建模过程必要的精化阶段引入组件的具体定义,以降低系统开发和证明的复杂度。结果表明:提出的方法有助于在早期开发阶段减少TACS中复杂的细节部分,使得证明义务成功率为100%,自动证明成功率占比83%,手动证明成功率仅占比仅17%,在简化证明义务的同时有效提高了自动化证明的占比。