Modellierung verteilter Systeme - fileBroy SS 12: Modellierung verteilter Systeme 4 . Technische...
Transcript of Modellierung verteilter Systeme - fileBroy SS 12: Modellierung verteilter Systeme 4 . Technische...
Technische Universität München
Broy SS 12: Modellierung verteilter Systeme 1
Modellierung verteilter Systeme Grundlagen der Programm und Systementwicklung
Sommersemester 2012
Prof. Dr. Dr. h.c. Manfred Broy
Unter Mitarbeit von Dr. M. Spichkova, J. Mund, P. Neubeck
Lehrstuhl Software & Systems Engineering
Technische Universität München
Broy SS 12: Modellierung verteilter Systeme 2
Sichtenintegration
Technische Universität München
Zustand und Ablauf
Broy SS 12: Modellierung verteilter Systeme 3
Technische Universität München
Lineare Temporale Logik
Zustandsmaschinen mit markierten Übergängen besitzen
sequentielle Abläufe
Ablauf endet, wenn keine Übergänge mehr möglich sind
endliche Berechnung
Bei totaler Übergangsrelation sind alle Abläufe unendlich
Jeder Zustand hat dann eine Menge von unendlichen Strömen von
Zuständen und eine Menge von unendlichen Strömen von
Aktionen
Ablauf auch als Strom von Paaren (i, ai+1) beschreibbar
Broy SS 12: Modellierung verteilter Systeme 4
Technische Universität München
Abläufe von Zustandsmaschinen
Gegeben eine Zustandsmaschine mit markierten Übergängen
Wir können jedem Zustand einfach eine Menge von sequentiellen
Abläufen zuordnen
Behandlung von nichtsequentielle Abläufe
Darstellung von Parallelität auf der Ebene der Zustandsmaschinen
Erweiterung der Übergänge auf Übergänge mit Mengen von Aktionen
Broy SS 12: Modellierung verteilter Systeme 5
Technische Universität München
Lineare Temporale Logik: Fairness
Broy SS 12: Modellierung verteilter Systeme 6
':' sss ¾®¾$a
Technische Universität München
Äquivalenz von Zustandsmaschinen
Verschiedene Systeme können in Hinblick auf bestimmte Beobachtungen
gleiches Verhalten realisieren
Es gibt unterschiedliche Definitionen für die Äquivalenz zweier Systeme (bei
Zustandsmaschinen zweier Anfangszustände)
Ein guter Äquivalenzbegriff erlaubt es, in einer Komposition/Architektur ein
Teilsystem gegen ein äquivalentes auszutauschen
Kongruenz
Kompatibilität
Schnittstellengleichheit (Verfeinerung, siehe später )
Äquivalenzbegriffe für Zustände (erweiterbar auf Mengen von Zuständen
und Zustandsmaschinen) von Maschinen mit markierten Übergängen:
Spuräquivalenz
Bisimulationsäquivalenz
Verweigerungs- bzw. Bereitschaftsäquivalenz
Broy SS 12: Modellierung verteilter Systeme 7
Technische Universität München
Definition: Spuräquivalenz
Zwei Zustandsmaschinen M1 und M2 mit Startzuständen 0 und
’0 heißen (aktions-) spuräquivalent, wenn ihre Mengen von
Aktionsspuren übereinstimmen.
Spuräquivalenz ist formal definiert durch:
wobei
Broy SS 12: Modellierung verteilter Systeme 8
)'()(~ 0021 ss spurenspurenMM Spur =Û
Technische Universität München
Definition: Simulation
Broy SS 12: Modellierung verteilter Systeme 9
M1 simuliert M2
Technische Universität München
Definition: Bisimulation
Broy SS 12: Modellierung verteilter Systeme 10
Technische Universität München
Beispiel: Vergleich Spur- und Bisimulationsäquivalenz
Die Zustandsmaschinen M1 und M2 sind spuräquivalent, aber nicht
bisimulationsäquivalent.
Broy SS 12: Modellierung verteilter Systeme 11
Technische Universität München
Vergleich Spur- und Bisimulationsäquivalenz
Bisimulationsäquivalenz impliziert Spuräquivalenz
Je nach gewähltem Kompositionoperator ist eine andere
Äquivalenz geeignet
Bei asynchroner Kommunikation Spuräquivalenz
Bei synchroner Kommunikation Bisimulationsäquivalenz
z.B. gilt die Kongruenz
Broy SS 12: Modellierung verteilter Systeme 12
Technische Universität München
Definition: Bereitschaftsäquivalenz
Broy SS 12: Modellierung verteilter Systeme 13
Technische Universität München
Vergleich Bereitschafts- und Bisimulationsäquivalenz
Die Zustände 1 und 2 sind spur- und bereitschaftsäquivalent, aber
nicht bisimulationsäquivalent
Broy SS 12: Modellierung verteilter Systeme 14
Technische Universität München
Vergleich der Äquivalenzbegriffe
Broy SS 12: Modellierung verteilter Systeme 15