Formal Verification of Radio Communication Management in Railway Systems Using Model Checking Technique

被引：1

作者：

Borrelli, Antonio ^{[1
]}

Di Lucca, Giuseppe Antonio ^{[1
]}

Nardone, Vittoria ^{[1
]}

Santone, Antonella ^{[2
]}

机构：

[1] Univ Sannio, Dept Engn, Benevento, Italy

[2] Univ Molise, Dept Biosci & Terr, Pesche, IS, Italy

来源：

2019 IEEE 28TH INTERNATIONAL CONFERENCE ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE) | 2019年

关键词：

Formal methods; model checking; safety critical system; railway system;

D O I：

10.1109/WETICE.2019.00060

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

The European Railway Traffic Management System has the purpose to provide a common signaling system for all the European nations. It consists of two subsystems: the trackside subsystem (TSS) and the on-board subsystem (OBS) that communicate to exchange information about the state of the trackside and/or the train. Radio communication can take place according to the requirements specification reported in ERTMS/ETCS SUBSET-026-3. As the communication between TSS and OBS is a critical issue, we exploit model checking to verify the correctness of the communication process as specified in the SUBSET-026-3. The results achieved during the experimentation seem to be very promising.

引用

页码：249 / 254

页数：6

共 50 条

[1] Implicit model Checking: Formal verification technique for large-scale discrete systems
Park, T
[J]. PROCEEDINGS OF THE 2000 IEEE INTERNATIONAL SYMPOSIUM ON COMPUTER-AIDED CONTROL SYSTEM DESIGN, 2000, : 135 - 140
[2] Formal Verification of Heuristic Autonomous Intersection Management Using Statistical Model Checking
Chouhan, Aaditya Prakash
Banda, Gourinath
[J]. SENSORS, 2020, 20 (16) : 1 - 25
[3] Formal Verification of Business Processes using Model Checking
Stoica, Florin
[J]. INNOVATION MANAGEMENT AND EDUCATION EXCELLENCE VISION 2020: FROM REGIONAL DEVELOPMENT SUSTAINABILITY TO GLOBAL ECONOMIC GROWTH, VOLS I - VI, 2016, : 2563 - 2575
[4] A symbolic model checking approach in formal verification of distributed systems
Souri, Alireza
Rahmani, Amir Masoud
Navimipour, Nima Jafari
Rezaei, Reza
[J]. HUMAN-CENTRIC COMPUTING AND INFORMATION SCIENCES, 2019, 9 (01):
[5] Formal Verification of Concurrent Systems via Directed Model Checking
Gradara, Sara
Santone, Antonella
Villani, Maria Luisa
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 185 (93-105) : 93 - 105
[6] Formal Verification of a Partial-Order Reduction Technique for Model Checking
Ching-Tsun Chou
Doron Peled
[J]. Journal of Automated Reasoning, 1999, 23 : 265 - 298
[7] Formal verification of a partial-order reduction technique for model checking
Chou, CT
Peled, D
[J]. JOURNAL OF AUTOMATED REASONING, 1999, 23 (3-4) : 265 - 298
[8] On Applying Model Checking in Formal Verification
Hjort, Hakan
[J]. 2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, 2022, 3 : 3 - 3
[9] A model checking technique for the verification of fuzzy control systems
Intrigila, Benedetto
Magazzeni, Daniele
Tofani, Alberto
Melatti, Igor
Tronci, Enrico
[J]. INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE FOR MODELLING, CONTROL & AUTOMATION JOINTLY WITH INTERNATIONAL CONFERENCE ON INTELLIGENT AGENTS, WEB TECHNOLOGIES & INTERNET COMMERCE, VOL 1, PROCEEDINGS, 2006, : 536 - +
[10] Formal verification of a group membership protocol using model checking
Rosset, Valerio
Souto, Pedro F.
Vasques, Francisco
[J]. ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS 2007: COOPLS, DOA, ODBASE, GADA, AND IS, PT 1, PROCEEDINGS, 2007, 4803 : 471 - 488

← 1 2 3 4 5 →