CTL-1
CTL Model Checking
Eine Einfhrung in den Proze derModellberprfung mit CTL
Uwe Bubeck15. Februar 2002
Hauptseminar Modellberprfung WS 2001/2002
CTL-2
Einleitung und Motivation
CTL Model Checking
CTL-3
Zeitbegriffe
Zeit -ein schwierig zu formalisierendes Phnomen
Unterschiedliche Zeitbegriffe:
zyklisch: historisch, vgl. Jahreszyklus
linear: ab 5. Jh. n.Chr. (Augustinus)
verzweigt: sptes Mittelalter
CTL-4
Logik mit verzweigter Zeit
Historische Entwicklung
Wilhelm von Ockham(1285 - 1349)
lange Epoche zeitloser Wahrheitsbegriffe
im 20. Jahrhundert wieder aufgegriffen
M. Clarke und E. Allen Emerson:
~1980 Modellberprfung mitComputation Tree Logic (CTL)
CTL-5
Die Temporallogik CTL
CTL Model Checking
CTL-6
Der Verifikationsproze
Genaue Beschreibungen sind Voraussetzungfr die formale berprfung eines Systems
Verifikationsproze umfat drei Phasen:
Systemmodellierung
Eigenschaften spezifizieren
berprfung der Eigenschaftengegen das Modell
CTL-7
Systemmodellierung
Wichtig fr die Systemmodellierung:geeignetes Abstraktionsniveau
Idee des Zustandsbergangssystems:
Zustnde: Zusammenfassung relevanterSystemvariablen zu einem Zeitpunkt
bergnge zwischen diesen
CTL-8
Kripke-StrukturBeschreibung eines Zustandsbergangssystemsdurch eine Kripke-Struktur mit
= (S, , L)
Verdeutlichung durch einen gerichteten Graphen
q,r r
p,q
s1
s2
s0
SS: bergangsrelationL: S (Atome) Markierungsfunktion
CTL-9
BerechnungspfadeAus dem Kripke-Modell ergeben sich direktdie mglichen Berechnungspfade.bergangsrelation linkstotal Pfade besitzen unendliche Lnge
q,r r
p,q
rr
rr
p,q
s0
s0
s1 s2
s2s2
s2s2
CTL-10
Modellbeziehung
Zu berprfende Eigenschaft wird in einerCTL-Formel ausgedrckt.
Frage: Formel im Startzustand s erfllt?
Dann: Kripke-Struktur in s Modell fr .Schreibweise
CTL-11
Syntax
Induktive Syntaxdefinition in BNF:
und : Wahrheitswerte falsch und wahrp: atomare Formel
CTL-12
Semantik 1/2Temporale Verknpfungen zusammengesetzt aus: dem Pfadquantor:
A: entlang aller Pfade (Always) E: entlang (mindestens) eines Pfades (Exists)
dem temporalen Operator: X: nchster Zustand (neXt) F: schlielich / in einem zuknftigen Zustand (Future) G: immer / in allen zuknftigen Zustnden (Globally) U: bis (Until)
Beispiel:EG : auf einem ausgehenden Pfad gilt in jedem Zustand
CTL-13
Semantik 2/2Modellbeziehung mit struktureller Induktion:
fr alle
genau dann, wenn
genau dann, wenn fr jedenNachfolgezustand gilt
reduzierte Operatormenge durch quivalenzen:
negierte Quantoren
Fixpunktdarstellung
CTL-14
Semantik: Beispiele
q,r r
p,q
s1
s2
s0
Beispiele fr gltige Formeln:
CTL-15
Anwendung undSystemmodellierung
CTL Model Checking
CTL-16
Spezifikationsmuster
Typische Spezifikationsmuster:
auf Anforderung folgt stets irgendwann die Bereitstellung
Proze wird auf jedem Pfad unendlich oft aktiviert
Auf jedem Pfad wird ein Endzustand erreicht
CTL-17
Mutual Exclusion 1/4
Problem gleichzeitiger Zugriffe auf Systemressourcen
Lsungsansatz: Kapselung in kritische Bereiche
Anforderungen an das Protokoll:
Sicherheit: nur ein Proze im kritischen Bereich
Lebendigkeit: Anforderung irgendwann erfllt
Blockierungsfreiheit: Anforderung jederzeit mglich
keine strikte Sequenzierung: nicht simples Abwechseln
CTL-18
Mutual Exclusion 2/4
Systemmodellierung:
Prozesse durchlaufen Zyklen
ni ti ci ni ti ci ...Bedeutung der Zustnde: ni (non-critical): auerhalb des kritischen Bereiches ti (trying): wartet auf Zugang ci (critical): durchluft kritischen Bereich
Zustandsbergnge unabhngig voneinander, abernicht gleichzeitig (asynchrones Interleaving)
CTL-19
Mutual Exclusion 3/4Formalisierung der Anforderungen in CTL:
Sicherheit
Lebendigkeit
Blockierungsfreiheit
keine strikte Sequenzierung
CTL-20
Mutual Exclusion 4/4
Beispielmodell erfllt alle Anforderungen, z.B.: Blockierungsfreiheit
Begrndung: alle Zustnde mit n1 besitzen einenNachfolgezustand mit t1
n1,n2
t1,n2 n1,t2
c1,n2 t1,t2 t1,t2 n1,c2
c1,t2 t1,c2
s0
s1
s2
s4
s3
s5
s8
s7
s6
CTL-21
Ausdruckskraft
CTL Model Checking
CTL-22
FairneErweiterung Mutual Exclusion:Schleifen erlauben Verweilen im kritischen Bereich
n1,c2
t1,c2 s7
s6n1,c2
t1,c2 s7
s6
Problem: Lebendigkeitsbedingung verletzt
Fairne-Bedingung:auf jedem zulssigen Pfad mu n2 unendlich oft gltig sein
CTL-23
CTL*
Ausdruckskraft von CTL begrenzt:
Fairne-Bedingung nicht in CTL formalisierbar
Abhilfe: Erweitern von
Semantik: nur ber faire Pfade quantifizieren
Syntax: erweiterte temporale Verknpfungen
CTL* erlaubt die unabhngige Verwendung vonPfadquantoren und temporalen Operatoren
Beispiele:
CTL-24
CTL* und Teilsprachen
Als Teilsprachen in CTL* enthalten: LTL CTL
Ausdruckskraft im schematischen Vergleich:
CTL*
CTL LTL
CTL-25
Algorithmus zurModellberprfung
CTL Model Checking
CTL-26
Markierungsalgorithmus 1/3Gegeben: Kripke-Struktur CTL-Formel Gesucht: Alle Zustnde mit
Realisierung durch Markierungsalgorithmus:
Fr jede Teilformel werden alle erfllenden Zustndeim Graphen markiert.
Ausnutzen des induktiven Formelaufbaus
CTL-27
Markierungsalgorithmus 2/3
Induktionsvoraussetzung:Graph bereits markiert fr die Teilformeln von
Fallunterscheidung: = p : Atom
markiere mit p, falls p L(s)
= 1 : Negationmarkiere mit 1, falls noch nicht mit 1 markiert
= 1 2 : Disjunktionmarkiere, falls bereits mit 1 oder 2 markiert
= EX1 : Exists neXtmarkiere, falls Nachfolger mit Markierung 1 existiert
CTL-28
Markierungsalgorithmus 3/3 = E [1 U 2]: Exists Until
1. Bestimme die mit 2 markierten Zustnde2. Gehe rckwrts zu allen Zustnden, die von dort mit
der invertierten bergangsrelation in einem berall mit1 markierten Pfad erreicht werden knnen
Test auf Erfllbarkeit von im Zustand s einer Kripke-Struktur = (S, , L) mit Laufzeit
O(|| (|S| + ||))Linear in der Lnge der Formel und der Gre des Modells
Aber Problem der Zustandsexplosion
CTL-29
Zusammenfassung
CTL - ein guter Kompromi zwischen
Ausdruckskraft Komplexittund+ Modellierung
nichtdeterministischerSysteme
- z. B. direkteModellierung vonFairne-Bedingungen
+ linear in der Gredes Modells
- Zustandsexplosion