Die Firma INSY GmbH hat eine verteilte Stellwerkslösung zur dezentralen Zugsteuerung entwickelt. Im Unterschied zu bisherigen zentralen Stellwerken wird hier die Steuerlogik in mobile Bordcomputer, lokale Schaltstationen an Weichen und Bahnübergängen sowie optionale übergeordnete Überwachungsstationen aufgeteilt. Im Rahmen eines studentischen Projekts und als Fallstudie im Projekt UniForM wurde das System im Modell nachgebildet, simuliert und validiert. Die Software für die Einzelkomponenten wurde dabei im Sinne formaler Methoden zunächst spezifiziert, teilweise verifiziert, implementiert und getestet. Auf dieser Grundlage konnten schließlich weitergehende Tests durchgeführt werden und der vollständige Sicherheitsnachweis für das Gesamtsystem - von der Anforderungsspezifikation bis zum Softwarecode - erbracht werden. Im Projekt DRACOS mit der DTU wird nun das System für größere Anwendungsbereiche weiterentwickelt und bezüglich seiner Sicherheitseigenschaften verifiziert.

Die Ergebnisse dienen als Fallstudie im Teilprojekt "Effiziente Analyse von hybriden Systemen" (HYBRIS), welches von der DFG im Rahmen des Schwerpunktprogramms "Integration von Techniken der Softwarespezifikation für ingenieurwissenschaftliche Anwendungen" ab 1999 gefördert wird.