Für eine formale Verifikation der in der Notation der UML erstellten Modelle müssen Teile dieser Modelle entsprechend umgeschrieben werden. Dabei werden die Zustandsdiagramme der UML, die meistens für die Beschreibung des dynamischen Verhaltens von Systemkomponenten eingesetzt werden, entweder in die direkt verifizierbaren Automaten übersetzt oder in eine Form umgeschrieben, die über einen weiteren Übersetzungsschritt verifiziert werden kann. In dem folgenden Beitrag wird ein Schema für die Umschreibung von Zustandsdiagrammen der UML in die Kripke-Strukturen präsentiert, die dann in die Eingangssprache des Model-Checkers SMV übersetzt werden können. Durch diese Umschreibung, die auch Plättung der Zustandsdiagramme genannt wird, werden alle Aktionen eines Objektes in der Anordnung auf eine Kripke-Struktur abgebildet, die in dem zugehörigen Zustandsdiagramm gegebenen sind. Dadurch wer den alle möglichen Ausführungspfade aufgestellt, die in einem gegebenen Zustandsdiagramm modelliert worden sind. Die hier zugrunde gelegten Zustandsdiagramme sind Teile einer objektorientierten Modellierung des FunkFahrBetriebs (FFB), die das dynamische Verhalten von Systemkomponenten dieses Eisenbahnbetriebsverfahrens abbilden.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Umschreibung von Zustandsdiagrammen der UML für das Model-Checking


    Beteiligte:


    Erscheinungsdatum :

    2003


    Format / Umfang :

    17 Seiten, 12 Bilder, 16 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Deutsch