This paper describes a model for railway signals in the context of interlocking. Since the design and construction of the software models shall be obtained in a formal way, the models were created using Petri nets to allow automatic verification and validation. A generic model for railway signals was designed and further utilized for the German railway signaling systems (The Ks signaling system). Simplified Petri net models for points, track segments and signals are given as a frame. The obtained models are also applied to a real station layout.