Modeling and Verification of TSSM-Based CBTC Zone Controller for Urban Rail Transit
-
摘要: 针对安全状态机缺乏时间描述能力的缺点,利用反应式系统的同步设计方法,提出了时间安全状态机TSSM (timed safe state machine)建模方法,定义了弱变迁和同步变迁语法,建立了城市轨道交通ZC (zone controller)系统模型.首先,分析了ZC系统的运行环境、工作原理和功能需求,根据ZC反应式系统的特点,利用TSSM在SCADE (safety critical application development environment)中建立了ZC系统列车管理、ZC控制、MA计算和队列管理子模型;其次,通过ZC系统的TSSM网络模型,分析了子模型间的交互信息;最后,采用Lustre语言对ZC系统的安全特性进行了形式化描述,并利用Design Verifier模型检测工具,结合数据流验证了ZC系统的功能和性能需要.研究结果表明,ZC系统TSSM模型的安全性和受限活性均为有效,ZC系统完全满足预期的安全需求.Abstract: As a safe state machine lacks time property, a TSSM (timed safe state machine) modeling method was presented based on the synchronous design method of reactive system. The weak transition and synchronized transition were defined, and the ZC (zone controller) system model for urban rail transit was established. First, the operation environment, principle and functional requirements of ZC were analyzed, and according to the ZC features of reactive systems, the train management, ZC control, MA calculation and queue management sub-models of ZC system were built using TSSM in SCADE (safety critical application development environment). Then through the TSSM network model of ZC, the interaction information between the sub-models was analyzed. Finally, the safety features of ZC are formally expressed in Lustre, and the functional and performance requirements are examined by running data flow in Design Verifier. The result demonstrates the validity of the bounded liveness and safety properties of the TSSM model, which shows that ZC completely satisfies the functional and safety requirements.
-
Key words:
- ZC /
- TSSM /
- modeling /
- SCADE /
- verification /
- model checking
-
杨旭文. 基于UML的CBTC系统区域控制器的建模与安全性验证 [D]. 北京:北京交通大学,2008. 吕继东,唐涛,燕飞,等. 基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证 [J]. 铁道学报,2009,31(3): 59-64. LU Jidong, TANG Tao, YAN Fei, et al. UPPAAL-based simulation and verification of CBTC zone control subsystem in rail transportation [J]. Journal of the China Railway Society, 2009, 31(3): 59-64. 王露. 区域控制器移动授权的UML模型与验证. 成都:西南交通大学,2013. 高霖. CBTC区域控制系统中列车管理的建模与分析 [D]. 北京:北京交通大学,2007. 朱迪. 基于有色Petri 网的区域控制器子系统切换功能建模 [D]. 北京:北京交通大学,2008. ANDR C. Semantics of SSM. Nice: University of Nice Sophia Antipolis, 2003. ANDR C. Computing synccharts reactions [J]. Electronic Notes in Theoretical Computer Science, 2004, 1(88): 3-19. 高冠龙. 基于时间自动机模型验证方法优化研究 [D]. 郑州:郑州大学,2006. IEEE Vehicular Technology Society. IEEE Std 1474.1 IEEE standard for communications-based train control (CBTC) performance and functional requirements [S]. [S.l.]: IEEE, 2004. 陈荣武. CBTC 系统列车运行仿真与优化策略 [D]. 成都:西南交通大学,2011. 何成才,杨淘. CBTC系统中移动闭塞与后备模式追踪间隔研究 [J]. 西南交通大学学报,2012,47(3): 446-450. HE Chengcai, YANG Tao. Comparison of headways in moving block and fallback modes for CBTC system [J]. Journal of Southwest Jiaotong University, 2012, 47(3): 446-450. 刘晓磊. 城市轨道交通区域控制器的研究 [D]. 成都:西南交通大学,2011. 文艳军,王戟,齐治昌. 并发反应式系统的组合模型检验与组合精化检验 [J]. 软件学报,2007,18(6): 1270-1281. WEN Yanjun, WANG Ji, QI Zhichang. Compositional model checking and compositional refinement checking of concurrent reactive systems [J]. Journal of Software, 2007, 18(6): 1270-1281. ESTEREL Technologies. SCADE Suite [EB/OL]. (2012-11-1).http: //www.esterel-technologies.com/products/scade-suite/. 袁磊,王俊峰,康仁伟,等. CTCS-3 级列控系统临时限速建模与验证 [J]. 西南交通大学学报, 2013,48(4): 708-714. YUAN Lei, WANG Junfeng, KANG Renwei, et al. Modeling and verification of temporary speed restriction of CTC-S3 train control system [J]. Journal of Southwest Jiaotong University, 2013, 48(4):708-714. -
点击查看大图
计量
- 文章访问数: 1205
- HTML全文浏览量: 99
- PDF下载量: 650
- 被引次数: 0
下载: