Veröffentlichung

Antoni, M.:
Petrinetzbasierte Validierung von Eisenbahnsicherungssystemen.
Dissertation, Technische Universität Braunschweig, Institut für Verkehrssicherheit und Automatisierungstechnik, März 2010.

Kurzfassung:

Kurzfassung Die Entwicklung der Informatik und der Auto-matisierung ist (und war schon immer) Quelle stets neuer und effizienterer Lösungen, aber auch neuer Komplexität; sie macht eine dauer¬hafte, wirtschaft-liche Gestaltung und Überprü¬fung der Sicherheit der Anlagen und der Ver¬kehrssysteme nur noch schwieriger. Die Echt¬zeitinformatik ist heutzutage in die Systeme integriert, die das Leben von Menschen verwal¬ten. Es stellt sich heraus, dass die derzeitigen Methoden und Normen nicht immer den Anfor¬derungen nach Verfügbarkeit und nach Sicher¬heit entsprechen. Es sind so systematische Fehler der Software zu befürchten. Die vorlie¬gende Arbeit besteht darin, eine Konzeptions- und Überprüfungs¬methode zu definieren und zu instrumentalisieren. Sie zeigt, dass es mög¬lich ist, formale Überprüfungs¬methoden auf industrielle Steuerungen anzuwenden. Die Eisen-bahnsteuerungen werden besonders behan¬delt. Die vorgeschlagene Methode beruht auf mehre¬ren Konzeptions¬ideen: - so weit wie möglich das berufliche Umfeld berücksichtigen, die Sicherheitseigenschaften und die Funktionsanforderungen identifizie¬ren - die Funktionssoftware und die Grundsoftware (Verwaltung des physikalischen Materials und Interpretation der fachspezifischen Aufgaben) unterscheiden - die Funktionen in Form von Automaten in AEFD-Sprache schreiben. Diese Sprache er¬laubt eine Formulierung von Petrinetzen und eine deterministische Interpretation. Unter diesen Bedingungen ist es möglich, eine formelle Überprüfung einer Eisenbahnsteue¬rung, z.B. eines Stellwerks, zu verwirklichen. Die Hauptidee besteht in der Entwicklung eines industriellen Sicherheitsautomaten, der sich wie eine abstrakte Maschine verhält, damit dieser später formal validiert werden kann. Das Hilfs-programm für die Formulierung der funktionellen Graphen ist für Fachleute be¬stimmt, die nicht über besondere Informatik¬kenntnisse verfügen. Die Petrinetze sind eine Konzeptualisie-rungssprache. Diese Netze, die in der AEFD-Sprache formuliert sind, werden als interpretier-bare Spezifikationen benützt. Die Sicher¬heits-eigenschaften und die An¬forde¬rungen sind auch auf dieselbe Art for¬muliert. Die vorgeschlagene Methode erlaubt es unter diesen Bedingungen, einen formalen Be¬weis der Funktionen des Systems durchzuführen.