Detail Inovasi Perguruan Tinggi


Tema: Train interlocking system, safety verification, model checking, timed-arc petri net, computation tree logic
Judul: Model Checking-based Safety Verification of a Petri Net Representation of Train Interlocking Systems
Perguruan Tinggi: Universitas Katolik Parahyangan
Jenis/sdm: dosen/0418088202

Tahun: 2018

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.