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.
Umschreibung von Zustandsdiagrammen der UML für das Model-Checking
2003
17 Seiten, 12 Bilder, 16 Quellen
Conference paper
German
Probleme bei der Übersetzung, Umschreibung osteuropäischer Führerscheine
Online Contents | 1994
|FLIGHT TRAINING - Umschreibung von FAA-Lizenzen: Scheingefecht
Online Contents | 2001
VGH Mannheim 9.12.2003 - 10 S 1908/03 : Umschreibung einer ausländischen Fahrerlaubnis
Online Contents | 2004