[vc_empty_space][vc_empty_space]
Model Checking-based Safety Verification of a Petri Net Representation of Train Interlocking Systems
Aristyo B.a, Pradityo K.a, Tamba T.A.b,c, Nazaruddin Y.Y.a,c, Widyotriatmo A.a
a Institut Teknologi Bandung, Instrumentation and Control Research Group, Bandung, Indonesia
b Dept. of Electrical Engineering (Mechatronics), Parahyangan Catholic University, Bandung, 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]© 2018 The Society of Instrument and Control Enginners – SICE.This paper describes an implementation of formal methods for safety verification of a railway interlocking system model based on model checking techniques. In the proposed method, a model for the interlocking system is constructed using timed-arc petri net and the safety specifications are expressed as computation tree logic formulas. These model and specification are then used in TAPAAL model checker to perform the model checking of safety verification task. Simulation results are presented to illustrate the advantages of the proposed verification method.[/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,Interlocking systems,Model-checking techniques,Petri net representations,Railway interlocking system,Safety specifications,Safety verification,Verification method[/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-arc petri net,Train interlocking system[/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 supported by the Indonesia’s Ministry of Research, Technology & Higher Education (Ke-menristekdikti) under 2018 Competency-Based Research scheme and also supported in part by USAID through the 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.23919/SICE.2018.8492661[/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]