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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Contributors:


    Publication date :

    2003


    Size :

    17 Seiten, 12 Bilder, 16 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    German