[vc_empty_space][vc_empty_space]
Safety verification of a train interlocking timed automaton model
Nazaruddin Y.Y.a,c, Tamba T.A.b,c, Pradityo K.a, Aristyo B.a, Widyotriatmo A.a
a Instrumentation and Control Research Group, Institut Teknologi Bandung, Indonesia
b Department of Electrical (Mechatronics) Engineering, Parahyangan Catholic University, Indonesia
c National Center for Sustainable Transportation Technology, Bandung, Indonesia
[vc_row][vc_column][vc_row_inner][vc_column_inner][vc_separator css=”.vc_custom_1624529070653{padding-top: 30px !important;padding-bottom: 30px !important;}”][/vc_column_inner][/vc_row_inner][vc_row_inner layout=”boxed”][vc_column_inner width=”3/4″ css=”.vc_custom_1624695412187{border-right-width: 1px !important;border-right-color: #dddddd !important;border-right-style: solid !important;border-radius: 1px !important;}”][vc_empty_space][megatron_heading title=”Abstract” size=”size-sm” text_align=”text-left”][vc_column_text]© 2019, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd. All rights reserved.This paper presents an application of formal methods based on model checking techniques for safety verification of a railway interlocking system. The proposed model checking techniques are implemented on a timed automaton model of the considered interlocking systems and with respect to safety operational specification that are expressed as computation tree logic formulas. The freely available UPPAAL model checker is used to perform the model checking task and simulation results of the performed verification are presented.[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Author keywords” size=”size-sm” text_align=”text-left”][vc_column_text]Computation tree logic,Model-checking techniques,Operational specifications,Railway interlocking system,Safety verification,Timed Automata,Train interlocking,Uppaal model checkers[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Indexed keywords” size=”size-sm” text_align=”text-left”][vc_column_text]Computation tree logic,Model checking,Safety verification,Timed automaton,Train interlocking[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Funding details” size=”size-sm” text_align=”text-left”][vc_column_text][{‘$’: ‘This work was funded by KEMENRISTEKDIKTI of the Republic of Indonesia and in part by USAID through SHERA program. This work was supported by the Indonesian Ministry of Research, Technology, and Higher Education (MORTHE) under the 2019 Competency-Based Research scheme, and in part by USAID through SHERA program under grant no. IIE00000078-ITB-1.’}, {‘$’: ‘This work was supported by the Indonesian Ministry of Research, Technology, and Higher Education (MORTHE) under the 2019 Competency-Based Research scheme, and in part by USAID through SHERA program under grant no. IIE00000078-ITB-1.’}][/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”DOI” size=”size-sm” text_align=”text-left”][vc_column_text]https://doi.org/10.1016/j.ifacol.2019.11.696[/vc_column_text][/vc_column_inner][vc_column_inner width=”1/4″][vc_column_text]Widget Plumx[/vc_column_text][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row][vc_row][vc_column][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][/vc_column][/vc_row]