Synchronizing Automata and Petri Net based controllers

In designing safe and reliable interlocking systems for railways which are compatible with the related CENELEC (European Committee for Electrotechnical Standardization) standards semi-formal methods and diverse programming techniques are highly recommended (HR). EN 50128 (where methodologies to build failsafe software for railway applications are defined) recommends the use of Automata and Petri Nets (PNs) as semi-formal methods to build failsafe interlocking software for railway applications. In this paper interlocking software design which is achieved by using automata and PNs is explained where they were used synchronously as a voting system.