Design of signal control structures using formal methods for railway interlocking systems

Today the relay based railway interlocking systems are changing into programmable software interlocking systems. Looking at the hardware aspect, safety certified components can be used in order to satisfy the safety requirements of railway interlocking systems. But to satisfy the software requirements, the design and the programming of the interlocking system must be made by formal methods. To do this, preparing function blocks for each kind of the field equipments can be a method in order to realize a railway interlocking system. The purpose of this paper is to develop a Programmable Logic Controller (PLC) program for the signal function blocks by using formal methods and make a comparison between them.