Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems

被引:1
作者
Fantechi, Alessandro [1 ,2 ]
机构
[1] DTU Compute, Lyngby, Denmark
[2] Univ Florence, DINFO, Florence, Italy
来源
CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION | 2016年 / 9933卷
关键词
VERIFICATION;
D O I
10.1007/978-3-319-45943-1_16
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
The technological evolution of railway signalling equipment promises significant increases in transport capacity, in operation regularity, in quality and safety of the service offered. This evolution is based on the massive use of computer control units on board trains and on the ground, that aims at improving the performance of rail transport and maintaining high safety figures. A brief review of possible innovation trends of signalling systems shows that they will be more and more based on the exchange of accurate and secure complex information, in order to ensure safe operation. For this reason we want to advocate the adoption of a novel, datadriven safety certification approach, based on formal verification techniques, focusing on the desired attributes of the exchanged information. A discussion on this issue is presented, based on some initial observations of the needed concepts.
引用
收藏
页码:231 / 245
页数:15
相关论文
共 32 条
[1]  
[Anonymous], INTEGRITY CONSIDERAT
[2]  
[Anonymous], LOGIC GROUP PREPRINT
[3]  
Bergenhem C., 2012, ITS WORLD C VIENN 22
[4]   A formal verification environment for railway signaling system design [J].
Bernardeschi, C ;
Fantechi, A ;
Gnesi, S ;
Larosa, S ;
Mongardi, G ;
Romano, D .
FORMAL METHODS IN SYSTEM DESIGN, 1998, 12 (02) :139-161
[5]  
Binbin Chen, 2015, Computer Safety, Reliability and Security. SAFECOMP 2015 Workshops, ASSURE, DECSoS, ISSE, ReSA4CI and SASSUR. Proceedings: LNCS 9338, P277, DOI 10.1007/978-3-319-24249-1_24
[6]  
Bock U., 2000, 9 IFAC S CONTR TRANS, P410
[7]   Validation of Railway Interlocking Systems by Formal Verification, A Case Study [J].
Bonacchi, Andrea ;
Fantechi, Alessandro ;
Bacherini, Stefano ;
Tempestini, Matteo ;
Cipriani, Leonardo .
SOFTWARE ENGINEERING AND FORMAL METHODS, 2014, 8368 :237-252
[8]   Non-Markovian Performability Evaluation of ERTMS/ETCS Level 3 [J].
Carnevali, Laura ;
Flammini, Francesco ;
Paolieri, Marco ;
Vicario, Enrico .
COMPUTER PERFORMANCE ENGINEERING, 2015, 9272 :47-62
[9]   Unreliable failure detectors for reliable distributed systems [J].
Chandra, TD ;
Toueg, S .
JOURNAL OF THE ACM, 1996, 43 (02) :225-267
[10]  
DaSilva Clara, 1992, P IFIP TC6 WG61 5 IN, V10, P199