Model Checking-based Safety Verification of a Petri Net Representation of Train Interlocking Systems

Aristyo, B.; Pradityo, K.; Tamba, Tua Agustinus; Nazaruddin, Yul Yunazwin; Widyotriatmo, A.

dc.contributor.author	Aristyo, B.
dc.contributor.author	Pradityo, K.
dc.contributor.author	Tamba, Tua Agustinus
dc.contributor.author	Nazaruddin, Yul Yunazwin
dc.contributor.author	Widyotriatmo, A.
dc.date.accessioned	2019-03-06T05:06:51Z
dc.date.available	2019-03-06T05:06:51Z
dc.date.issued	2018
dc.identifier.isbn	978-490776460-9
dc.identifier.other	maklhsc428
dc.identifier.uri	http://hdl.handle.net/123456789/7587
dc.description	Makalah dipresentasikan pada 2018 57th Annual Conference of the Society of Instrument and Control Engineers of Japan (SICE). Nara, Japan, September 11-14, 2018.	en_US
dc.description.abstract	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.	en_US
dc.description.uri	https://doi.org/10.23919/SICE
dc.language.iso	en	en_US
dc.publisher	The Institute of Electrical and Electronics Engineers (IEEE) Inc.	en_US
dc.relation.ispartofseries	Proceesings of Annual Conference;2018
dc.subject	MODEL CHECKING	en_US
dc.subject	TRAIN INTERLOCKING SYSTEM	en_US
dc.subject	SAFETY VERIFICATION	en_US
dc.subject	TIMED-ARC PETRI NET	en_US
dc.subject	COMPUTATION TREE LOGIC	en_US
dc.title	Model Checking-based Safety Verification of a Petri Net Representation of Train Interlocking Systems	en_US
dc.type	Conference Papers	en_US