Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL  

作　　者：AHMAD Ehsan DONG YunWei LARSON Brian Lü JiDong TANG Tao ZHAN NaiJun 

机构地区：[1]School of Computer Science, Northwestern Polytechnical University, Xi'an 710072, China [2]State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China [3]Computing and Information Systems, Kansas State University, Manhattan KS 66506, USA [4]State Key Laboratory of Rail TraJ~c Control and Safety, Beijing Jiaotong University, Beijing 100044, China

出　　处：《Science China(Information Sciences)》2015年第11期121-140,共20页中国科学（信息科学）（英文版）

基　　金：AHMAD Ehsan and ZHAN Nai Jun are supported by National Basic Research Program of China(973 Program)(Grant No.2014CB340701);National Natural Science Foundation of China(Grants Nos.91118007,91418204);CAS/SAFEA International Partnership Program for Creative Research Teams;DONG Yun Wei is supported by National Infrastructure Software Plan(Grant No.2012ZX01041-002-003);LüJi Dong and TANG Tao are supported by National Basic Research Program of China(973 Program)(Grant No.2014CB340703);National Natural Science Foundation of China(Grant No.61304185)

摘　　要：Train control systems like most digital controllers are, by definition, hybrid systems as they interact with or try to control some aspects of the physical world. Detailed behavior modeling with constraints specification and formal verification, required for reliability prediction, is a great challenge for hybrid system designers.Train control systems further intensify this challenge with extensive interaction between computing units and their physical environment and their mutual dependence on each other. In this paper, we investigate behavior modeling and formal verification of Chinese Train Control System Level 3（CTCS-3） using Architectural Analysis ＆ Design Language（AADL） to cope with this challenge. AADL is an architecture description language for embedded systems and is based on model-based engineering paradigm. Along with structural modeling of embedded systems using the core language constructs, AADL also provides support for language extension through annex sublanguages. In system requirements specification document, the behavior of the CTCS-3 is specified as a set of basic operation scenarios that cooperate with each other to achieve safe and secure functionality of trains.Movement Authority（MA） scenario, explored in this paper, is considered as a basic and most crucial scenario to prevent trains from colliding with each other. The detailed discrete behavior of control system is modeled and verified using the Behavior Language for Embedded Systems with Software（BLESS） annex sublanguage of AADL, and the continuous behavior of train with the cyber–physical interaction（communication between train and control system） is modeled using the Hybrid annex sublanguage. The behavior of the MA scenario at system level is verified using the Hybrid Hoare Logic theorem prover. Behavior constraints are specified as assertions using first-order logic formulas augmented with a simple temporal operator.Train control systems like most digital controllers are, by definition, hybrid systems as they interact with or try to control some aspects of the physical world. Detailed behavior modeling with constraints specification and formal verification, required for reliability prediction, is a great challenge for hybrid system designers.Train control systems further intensify this challenge with extensive interaction between computing units and their physical environment and their mutual dependence on each other. In this paper, we investigate behavior modeling and formal verification of Chinese Train Control System Level 3（CTCS-3） using Architectural Analysis ＆ Design Language（AADL） to cope with this challenge. AADL is an architecture description language for embedded systems and is based on model-based engineering paradigm. Along with structural modeling of embedded systems using the core language constructs, AADL also provides support for language extension through annex sublanguages. In system requirements specification document, the behavior of the CTCS-3 is specified as a set of basic operation scenarios that cooperate with each other to achieve safe and secure functionality of trains.Movement Authority（MA） scenario, explored in this paper, is considered as a basic and most crucial scenario to prevent trains from colliding with each other. The detailed discrete behavior of control system is modeled and verified using the Behavior Language for Embedded Systems with Software（BLESS） annex sublanguage of AADL, and the continuous behavior of train with the cyber–physical interaction（communication between train and control system） is modeled using the Hybrid annex sublanguage. The behavior of the MA scenario at system level is verified using the Hybrid Hoare Logic theorem prover. Behavior constraints are specified as assertions using first-order logic formulas augmented with a simple temporal operator.

关 键 词：AADL behavior modeling BLESS annex CTCS hybrid annex train control system 

分 类 号：U284.48[交通运输工程—交通信息工程及控制] TP273[交通运输工程—道路与铁道工程]