SIGNAL+DRAHT | Issue 01-02/2004
Spezifikation von Stellwerkslogik mit formalen Methoden
Das schwedische Eisenbahninfrastrukturunternehmen Banverket hat in Kooperation mit der Firma Industrilogik eine vollständige Spezifikation der schwedischen Regeln für die Signaltechnik mithilfe von formalen Methoden erstellt. Die Spezifikation wurde erfolgreich genutzt, um die Software für das elektronische Stellwerk Alister von Vossloh zu generieren und zu verifizieren. Dies beinhaltet neben den Vorteilen in neuen Projekten den Prozess zur Harmonisierung der Regeln im ganzen Land und die volle Dokumentation der nunmehr existierenden Regeln. Die Bandbreite der unterschiedlichen Interpretationen der Spezifikation wurde beträchtlich reduziert.