Formal modeling and parameter analysis method for train control system based on hybrid unified modeling language

被引：0
|
作者：
Zhao X. [1 ]
Cheng R. [2 ]
Cheng Y. [3 ]
Ma X. [2 ,4 ]
机构：
[1] Postgraduate Department, Chinese Academy of Railway Science Beijing, Beijing
[2] State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing
[3] Institute of Communication and Signaling, Chinese Academy of Railway Sciences, Beijing
[4] School of Traffic & Transportation, Beijing Jiaotong University, Beijing
来源：
Ma, Xiaoping (xpma123@163.com) | 1600年 / Science Press卷 / 38期
关键词：
Control parameter analysis; High speed train control system; Linear hybrid automata; Moving block control system; UML extensibility mechanism;
D O I：
10.3969/j.issn.1001-8360.2016.11.012
中图分类号：
学科分类号：
摘要：
In view of the hybrid characteristics of high speed train control system, a formal modeling and parameter analysis method was proposed based on Hybrid Unified Modeling Language. UML2.0 and its extensibility mechanism were used to model the hybrid behaviors of the train control system. The transformation rules from HUML model to HYTECH model were defined so as to convert HUML model into linear hybrid automata (LHA). Safety requirements of train control system were added into the established HYTECH model in order to set up safety HYTECH model. Then, the safety HYTECH models were automatically analyzed by a model checking tool HYTECH. In the light of the proposed modeling method based on UML Profile, the tracking model of “Moving Block System” was taken as the case study and HUML controller model for following train was set up. The corresponding value range of unknown control parameters was obtained through the calculation of the reachable set of safety HYTECH model. The verification results showed the effectiveness of HUML based train control system modeling and analysis method. © 2016, Editorial Office of Journal of the China Railway Society. All right reserved.
引用
收藏
页码：80 / 87
页数：7
相关论文
共 10 条
  • [1] Henzinger T.A., The Theory of Hybrid Automata, Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pp. 278-292, (1996)
  • [2] Franzle M., Herde C., HySAT: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems, Formal Methods in System Design, 30, 3, pp. 179-198, (2007)
  • [3] Bail L.J., Alla H., David R., Hybrid Petri Nets, Proceedings of the 1st International European Control Conference, pp. 1472-1477, (1991)
  • [4] Henzinger T.A., Kopke P.W., Puri A., Et al., What's Decidable About Hybrid Automata, Proceedings of the 27th Annual ACM Symposium on Theory of Computing, pp. 373-382, (1995)
  • [5] Platzer A., Differential Dynamic Logic for Hybrid Systems, Journal of Automated Reasoning, 41, 2, pp. 143-189, (2008)
  • [6] Lu J., Li K., Tang T., Et al., Formal Modeling and Verification Method for High Speed Train Control System Based on Hybrid Communicating Sequential Process, China Railway Science, 33, 5, pp. 91-97, (2012)
  • [7] Unified Modeling Language: Superstructure Version2.0, (2009)
  • [8] A UML Profile for MARTE: Modeling and Analysis of Real Time EmbeddedSystems, (2011)
  • [9] Berkenkotter K., Bisanz S., Hannemann U., Et al., The HybridUML Profile for UML 2.0, International Journal on Software Tools for Technology Transfer, 8, 2, pp. 167-176, (2006)
  • [10] Henzingert A., Ho P.H., Wong-Toi H., HyTech: The Next Generation, Proceedings of the 16th Annual Real-time Systems Symposium, pp. 56-65, (1995)
1