Um die Präzision und Überprüfbarkeit der Systemanforderungsspezifikationen zu erhöhen, empfehlen die CENELEC-Normen für die Eisenbahnsysteme den Einsatz von formalen Methoden, die über eindeutige Syntax und Semantik verfügen. In der vorliegenden Arbeit werden für die Spezifikation und Verifikation von Eisenbahnsicherungssystemen formal fundierte grafische Beschreibungsmittel zur Verfügung gestellt. Diese Beschreibungsmittel sind eine Auswahl von Diagrammen der Unified Modeling Language (UML), die unterschiedliche Sichten in der Systemanforderungsspezifikation darstellen. Durch die Klassendiagramme kann die Systemstruktur beschrieben werden. Die Zustandsdiagramme und die Sequenzdiagramme werden für die Spezifikation des dynamischen Systemverhaltens verwendet. In den Klassendiagrammen werden für die Relationen Assoziation, Aggregation, Komposition und Vererbung formale Definitionen eingeführt, die die präzise Spezifikation von Beziehungen unter den Systemkomponenten ermöglichen. Weiter werden auf Basis dieser Definitionen Kriterien für die Konsistenzüberprüfung zwischen den verschiedenen Teilen der Systemspezifikation eingeführt. In den Zustandsdiagrammen werden die Aktionen, ihre Ausführung, unterschiedliche Zustandsarten und ihre Aktivierung formal definiert. Transitionen zwischen den Zuständen und deren Ausführung sind weitere Punkte, die dabei präzisiert werden. Über die eingeführten formalen Semantiken für angewendete Notationen werden Schemata für die Transformation von Zustandsdiagrammen der UML in eine formal verifizierbare Form definiert. Dadurch ist eine formale Verifikation der Systemanforderungsspezifikation durchführbar, die auf der Technik Model-Checking basiert. Die Anwendbarkeit der präsentierten Spezifikationsmittel und die formale Verifikation über die Technik Model-Checking werden am Beispiel des eingleisigen Bahnübergangs im Funkfahrbetrieb demonstriert. Dadurch sind für die Erstellung einer formal verifizierbaren Systemanforderungsspezifikation Beschreibungsmittel bereitgestellt, die aufgrund ihrer grafischen Gestalt für die Ingenieure der Eisenbahnsicherungstechnik handhabbar sind, und die Forderung der CENELEC-Normen nach Erhöhung der Präzision und Verifizierbarkeit erfüllen.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal verifizierbare objektorientierte Systemspezifikationen mit UML für Eisenbahnsicherungssysteme


    Contributors:


    Publication date :

    2005


    Size :

    105 Seiten, Bilder, Tabellen, Quellen




    Type of media :

    Theses


    Type of material :

    Print


    Language :

    German