Die Entwicklung der Informatik und der Automatisierung ist (und war schon immer) Quelle stets neuer und effizienterer Lösungen, aber auch neuer Komplexität; sie macht eine dauerhafte, wirtschaftliche Gestaltung und Überprüfung der Sicherheit der Anlagen und der Verkehrssysteme nur noch schwieriger. Die Echtzeitinformatik ist heutzutage in die Systeme integriert, die das Leben von Menschen verwalten. Es stellt sich heraus, dass die derzeitigen Methoden und Normen nicht immer den Anforderungen nach Verfügbarkeit und nach Sicherheit entsprechen. Es sind so systematische Fehler der Software zu befürchten. Die vorliegende Arbeit besteht darin, eine Konzeptions- und Überprüfungsmethode zu definieren und zu instrumentalisieren. Sie zeigt, dass es möglich ist, formale Überprüfungsmethoden auf industrielle Steuerungen anzuwenden. Die Eisenbahnsteuerungen werden besonders behandelt. Die vorgeschlagene Methode beruht auf mehreren Konzeptionsideen: - so weit wie möglich das berufliche Umfeld berücksichtigen, die Sicherheitseigenschaften und die Funktionsanforderungen identifizieren - 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 erlaubt eine Formulierung von Petrinetzen und eine deterministische Interpretation. Unter diesen Bedingungen ist es möglich, eine formelle Überprüfung einer Eisenbahnsteuerung, 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 Hilfsprogramm für die Formulierung der funktionellen Graphen ist für Fachleute bestimmt, die nicht über besondere Informatikkenntnisse verfügen. Die Petrinetze sind eine Konzeptualisierungssprache. Diese Netze, die in der AEFD Sprache formuliert sind, werden als interpretierbare Spezifikationen benützt. Die Sicherheitseigenschaften und die Anforderungen sind auch auf dieselbe Art formuliert. Die vorgeschlagene Methode erlaubt es unter diesen Bedingungen, einen formalen Beweis der Funktionen des Systems durchzuführen.


    Zugriff

    Download

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Petrinetzbasierte Validierung von Eisenbahnsicherungssystemen


    Weitere Titelangaben:

    Petrinet-based Validation of Railway Signalling and Safety Systems


    Beteiligte:
    Antoni, Marc (Autor:in) / Universitätsbibliothek Braunschweig (Gastgebende Institution) / Schnieder, E. (Akademische:r Betreuer:in)

    Erscheinungsdatum :

    2009



    Medientyp :

    Sonstige


    Format :

    Elektronische Ressource


    Sprache :

    Deutsch


    Klassifikation :

    DDC:    625



    Validierung

    Lehmann, Lukas Maximilian | Springer Verlag | 2023


    Validierung

    Klemm, David | Springer Verlag | 2019


    Validierung einer Fahrzeugposition

    PETER PRILLER DIPL ING | Europäisches Patentamt | 2022

    Freier Zugriff

    VALIDIERUNG ELEKTRISCHER LADEMUSTER

    O'GORMAN RYAN / STACHURA MIKOLAJ / VELAMPUDI APARNA | Europäisches Patentamt | 2022

    Freier Zugriff

    Validierung von Messplätzen

    Hirsch, Holger / Schwing, Christoph | VDE-Verlag | 2013