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

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.