Logic Verification of Collision Avoidance System in Train Control Systems

被引：1

作者：

Xu, Tianhua ^{[1
]}

Tang, Tao ^{[1
]}

Gao, Chunhai ^{[1
]}

Cai, Baigen ^{[1
]}

机构：

[1] Beijing Jiaotong Univ, State Key Lab Rail Traff Control & Safety, Beijing 100044, Peoples R China

来源：

2009 IEEE INTELLIGENT VEHICLES SYMPOSIUM, VOLS 1 AND 2 | 2009年

关键词：

D O I：

10.1109/IVS.2009.5164402

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We formally verify hybrid safety properties of Automatic Collision Avoidance System (ACAS) in the European Train Control System (ETCS). We present a formal requirements, design decision, discrete design and the real-time program for ACAS and verify correctness using compositional verification rules based Weakly monotonic time extension of DC* (WDC*). The advantage of compositional proof rule is that it decomposes a large system into more manageable pieces and to prove the correctness of the whole system from that of its immediate constituents. WDC* provides an essential simplification in reasoning about the design of real-time properties in ACAS by means of true synchrony hypothesis and the super-dense computation.

引用

页码：918 / 923

页数：6

共 50 条

[21] Collision Avoidance Radar System for the Bullet Train: Implementation and First Results
Liu, Aihua
Yang, Qiang
Zhang, Xin
Deng, Weibo
[J]. IEEE AEROSPACE AND ELECTRONIC SYSTEMS MAGAZINE, 2017, 32 (05) : 4 - 17
[22] Verification of collision avoidance algorithms in open sea and full visibility using fuzzy logic
Nguyen, Dong Trong
Trodahl, Marius
Pedersen, Tom Arne
Bakdi, Azzeddine
[J]. OCEAN ENGINEERING, 2023, 280
[23] A control authority transition system for collision avoidance
Acarman, T
Pan, Y
Ögüner, Ü
[J]. 2001 IEEE INTELLIGENT TRANSPORTATION SYSTEMS - PROCEEDINGS, 2001, : 466 - 471
[24] Probabilistic verification and synthesis of the next generation airborne collision avoidance system
von Essen, Christian
Giannakopoulou, Dimitra
[J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2016, 18 (02) : 227 - 243
[25] Probabilistic verification and synthesis of the next generation airborne collision avoidance system
Christian von Essen
Dimitra Giannakopoulou
[J]. International Journal on Software Tools for Technology Transfer, 2016, 18 : 227 - 243
[26] Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System
Jeannin, Jean-Baptiste
Ghorbal, Khalil
Kouskoulas, Yanni
Gardner, Ryan
Schmidt, Aurora
Zawadzki, Erik
Platzer, Andre
[J]. 2015 PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE (EMSOFT), 2015, : 127 - 136
[27] APPLICATION OF DECISION TREE ON COLLISION AVOIDANCE SYSTEM DESIGN AND VERIFICATION FOR QUADCOPTER
Chen, Chun-Wei
Hsieh, Ping-Hsun
Lai, Wei-Hsiang
[J]. INTERNATIONAL CONFERENCE ON UNMANNED AERIAL VEHICLES IN GEOMATICS (VOLUME XLII-2/W6), 2017, 42-2 (W6): : 71 - 75
[28] Fuzzy Formation Control and Collision Avoidance for Multiagent Systems
Chang, Yeong-Hwa
Chen, Chun-Lin
Chan, Wei-Shou
Lin, Hung-Wei
Chang, Chia-Wen
[J]. MATHEMATICAL PROBLEMS IN ENGINEERING, 2013, 2013
[29] Formation control and collision avoidance in mobile agent systems
De Gennaro, MC
Iannelli, IL
Vasca, F
[J]. 2005 IEEE INTERNATIONAL SYMPOSIUM ON INTELLIGENT CONTROL & 13TH MEDITERRANEAN CONFERENCE ON CONTROL AND AUTOMATION, VOLS 1 AND 2, 2005, : 796 - 801
[30] Control and optimization in a collision avoidance problem in oscillating systems
Avetisyan, V. V.
Chakhmakhchyan, R. E.
[J]. JOURNAL OF COMPUTER AND SYSTEMS SCIENCES INTERNATIONAL, 2016, 55 (02) : 163 - 178

← 1 2 3 4 5 →