Automatic generation of Petri Net supervisors for railway interlocking design

Interlocking design is one of the most crucial parts that provide safe travelling and transportation on railways especially in fixed block signaling systems (trains move through predetermined fixed railway blocks, where existence of a train can be determined.). In order to satisfy the requirements of CENELEC (European Committee for Electrotechnical Standardization) standards that are used for railways, formal methods such as Petri Nets are required to be used so as to decrease the possibility of logical errors. While providing these standards, Petri Net (PN) design method also brings simplicity on coding after the design stage. In this study, a Mathematica^© based program (PetriBox) that generates Petri Net supervisors automatically for a given sample railway yard will be described.