Einer, S.:
Petrinetzbasierte Spezifikation und Analyse operationaler Prozesse am Beispiel Eisenbahnsicherung.
Dissertation, Technische Universität Braunschweig, Institut für Verkehrssicherheit und Automatisierungstechnik, VDI Verlag Düsseldorf, 2003.
Im Kern der Arbeit wird eine Technik zur formalen Spezifikation und Analyse des betrieblichen Verhaltens von Automatisierungssystemen beschrieben. Diese Technik wurde vom Autor entwickelt, weil konventionelle Spezifikationen in diesem Bereich nur sehr schwer auf Vollständigkeit und Korrektheit überprüft werden können. Mit der entwickelten Technik ist es möglich, Spezifikationswissen zum einen Teil in ein formales Modell des Systemverhaltens und zum anderen Teil in eine Spezifikation bestimmter Anforderungen an die Eigenschaften des Systemverhaltens einzubringen. Die Erfüllung dieser Anforderungen durch das spezifizierte Systemverhalten kann dann verifiziert werden. Mit der automatischen Durchführung der Verifikation ist vordergründig ein Beitrag zur Entwurfsautomatisierung erreicht. Der eigentliche Beitrag zur Entwurfsautomatisierung liegt mit der entwickelten Technik aber darin, dass generische Anforderungen an die Eigenschaften der modellierten Verhaltensmodelle nicht für jeden Einzelfall expizit spezifiert werden müssen, sondern durch Anwendung der Technik automatisch ermittelt werden. Dies wird dadurch erreicht, dass die Anforderungsspezifikation nicht nur solche Eigenschaften beinhaltet, die mit dem Spezifikationswissen des Anwenders explizit gefordert werden, sondern auch solche, die sich ausschließlich aus der Form des modellierten Systemverhaltens ableiten lassen. Neben der Entwicklung der konkreten Spezifikationstechnik war außerdem ein Ziel, die formale Technik weniger mit den Mitteln der Mathematik als vielmehr gezielt aus Anwendersicht, d. h. ingenieurgerecht, zu beschreiben. Die Arbeit liefert dazu einen sogenannten Entwicklungsrahmen zur pragmatischen Festlegung von formalen Techniken. Dieser Rahmen ist ein Begriffsgebilde, das sturkturiert wesentliche Merkmale von formalen Techniken aufzeigt. Die erläuterte formale Spezifikations- und Verifikationstechnik basiert auf Petrinetzen. In der Dissertation wird diese spezielle Petrinetzanwendung auf der Basis des genannten Entwicklungsrahmens ausführlich beschrieben. Zu dieser Beschreibung zählt die Aufgabenstellung bzgl. der Anwendung der Technik, die allgemeinen und speziellen Aspekte des verwendeten bzw. entwickelten Beschreibungsmittels sowie die angewendeten und erarbeiteten Methoden. Schließlich wird die formale Technik an einem Fallbeispiel aus der Eisenbahnsicherung angewendet und damit validiert. Zusammenfassend ist die Arbeit im Ergebnis ein wissenschaftlicher Beitrag zur ingenieurgerechten Handhabung formaler Techniken im Allgemeinen sowie zur Spezifikation und Analyse operationaler Prozesse der Automatisierungstechnik im Speziellen.