1
Computergestützte Verifikation
19.4.2002
2
Inhalt
System Abstraktion
Spezifikation
Simulation
Formalisierung
Model Checker
Gegenbeispiel
Modell
log. Formel
+
-
VerfeinerungFehler-beseitigung
Präzisierung
Überlauf
Kapitel 1: Systeme
3
Konstruktion des Transitionssystemsist Aufgabe des Model Checkers
Als Modell wird dem Model Checker eine implizite Systembeschreibung übergeben
Hinter jeder impliziten Beschreibung stecktein Transitionssystem
Zusammenfassung Kapitel 1
Es gibt viele Beschreibungssprachen
4
Kapitel 2
Temporale Logik
5
Inhalt
System Abstraktion
Spezifikation
Simulation
Formalisierung
Model Checker
Gegenbeispiel
Modell
log. Formel
+
-
VerfeinerungFehler-beseitigung
Präzisierung
Überlauf
Kapitel 1: Systeme
Kapitel 2: Temporale Logik
6
Warum nicht einfach PK 1?
Beispiel: Wenn Prozess A eine Nachricht an B sendet, sowird (irgendwann spaeter) Prozess B eine Bestätigungzurückschicken.
t (send(A,B,t) t’ (send(B,A,t’)))
Viel zu kompliziert Rechnen zu schwer
7
Was ist Temporale Logik?
Es geht nicht um Zeit
Es geht um Eigenschaften von Zuständen undderen Änderung in Systemabläufen
Es ist (bei uns) eine Erweiterung der Aussagenlogik
Real Time Logik
8
Die Temporale Logik CTL*(Computation Tree Logic)
Ausgangspunkt: Eigenschaften von Zuständen
Sei AP eine Menge von atomaren Aussagen.Jedes Element von AP ist eineZustandsformel in CTL*
Ein Zustand s erfüllt p AP gdw. s(p) = W.
a,c c a,c bs p
Jeder Zustand liefert eine Belegung der atomaren Aussagen mit Wahrheitswerten: s(p) {W,F}
9
Zustandseigenschaften
“Mailbox ist leer” “bin bei Anweisung k”
“x[17] > 35” “nil dereferenziert”
k,q,nq,n
q
x,k
Annahme: s(p) mit vernachlässigbarem Aufwandberechenbar aus Repräsentation von s im Rechner
10
Pfade in Transitionssystemen
s1
s2
s3
s4
s5
s6
s1s2 s3 s4 s5 s6 s4s1
s1
s5 s6 ...
s1
s1 s5 s6 s4 s5 s6 ...s4 s5 s6 s4
Wir betrachten nur unendliche Pfade(ggf. unendliche Wiederholung des Endzustandes)
11
CTL* -Triviale Pfadformeln
: a a,q b c c c,d .....
Jede Zustandsformel ist eine Pfadformel
Ein Pfad erfüllt eine Zustandsformel gdw. seinerster Zustand sie erfüllt.
a c true
a
12
CTL* - Der NACHFOLGER-Operator
: a a,q b c c c,d .....
Wenn eine Pfadformel ist, so auch X
Ein Pfad (s0 s1 s2 s3 ... ) erfüllt X gdw. (s1 s2 s3 s4 ... ) erfüllt .
X a
a,q b c c c,d .....
X X X b
a,q b c c c,d .....
XX X
b c c c,d .....
b
b
Tautologien: X X X ( X X
13
CTL* - Der IRGENDWANN-Operator
: a a,q b c c c,d .....
Falls eine Pfadformel ist, so auch F
Ein Pfad (s0 s1 s2 s3 ... ) erfüllt F gdw. (s[i] s[i+1] s[i+2] s[i+3] ... ) erfüllt , für ein i0.
F b X a F( b X c)
Tautologien: F X F F F F X F F X FFFF X FFFF
...... b c c c,d .....
14
CTL* - Der IMMER-Operator
: a a,q b,q a,c q,c q .....
Wenn eine Pfadformel ist, so auch G
Ein Pfad (s0 s1 s2 s3 ... ) erfüllt G gdw. (s[i] s[i+1] s[i+2] s[i+3] ... ) erfüllt , für alle i0.
G (a q)
Tautologien: G G X G F G G G GF G G G (G G G ( GX G
...... q
15
Kombinationen von F and G
G F = gilt unendlich oft
.......
F G = stabilisiert
..........
G ( F ) = führt zu
..........
Tautologien: F G F G F G F G F G
16
CTL* - Der BIS-Operator
: a a,q c,q a,c q,c q .....
Wenn und Pfadformeln sind, so auch U
Ein Pfad (s0 s1 s2 s3 ... ) erfüllt U gdw.(s[i] s[i+1] s[i+2] s[i+3] ... ) erfüllt , für ein i0,und (s[j] s[j+1] s[j+2] ... ) erfüllt , für alle j < i.
a U c
Tautologien: U Ftrue U U U X ( U ))
qa,d
17
Temporale Operatoren auf Pfaden –Zusammenfassung
X /
G /
U
Symbol engl. Namenextstep
eventually
always
until
Vergangenheitsversion
P / (previous)
F / O / (once)
B / (always been)
S (since)
+ atomare Aussagen + Boolesche Operatoren = Linear Time Temporal Logic (LTL)
18
Sicherheit und Lebendigkeit
Eine Pfadeigenschaft kann aufgefaßt werden als dieMenge derjenigen Pfade, die die Eigenschaft erfüllen
S ist eine Sicherheitseigenschaft, wenn zu jedem Sein (endl.) Anfangsstück ’ existiert, so daß jede unendlicheFortsetzung von’ ebenfalls S ist.
Also: Verletzung einer Sicherheitseigenschaft kannnach endlicher Zeit festgestellt werden und ist permanent.
Beispiele: G f X f
19
Sicherheit und Lebendigkeit
L ist eine Lebendigkeitseigenschaft, wenn zu jedem endlichenPfad eine Fortsetzung ’ L existiert.
Also: Für keinen Pfad kann ich mir nach endlicher Zeit sicher sein, daß er die Eigenschaft verletzt.
Beispiele: F f GF f FG f
Satz: Jede Pfadeigenschaft ist äquivalent zu einer Konjunktionaus einer Sicherheits- und einer Lebendigkeitseigenschaft.
20
Sicherheit und Lebendigkeit
in der Praxis: Unterteilung in Sicherheit und Lebendigkeitsehr natürlich
Sicherheit = nichts Schlimmes kann jemals passieren
Lebendigkeit = Etwas Erwünschtes wird irgendwann passieren
21
s5
Der Berechnungsbaum
s1
s2
s3
s4
s6
s1s1
s4s2
s4
s2
s5
s3
s3
s5
s1
s1
s5
s5 s6
s6
s2 s4 s6 s4
22
a,q
Der Berechnungsbaum
a,b
q
c
q
a,b
cq
a,q
a,b a,q q
q c q c
ist unendlich in jedem Zweig
Zu jedem (Anfangs-)zustand gibt es genau einen Berechnungsbaum
Berechnungsbaum hat die gleichenPfade wie zugrundeliegendes Transitionssystem (beim gleichen Anfangszustand)
23
CTL* -Pfadquantoren
s
Wenn eine Pfadformel ist, soist E eine Zustandsformel
s erfüllt E gdw. es einen Pfad gibt, der bei s beginnt und
a,b a,d
c
s E F c s A X aTautologien: A E AE
Wenn eine Pfadformel ist, soist A eine Zustandsformel
s erfüllt A gdw. für alle Pfade die bei s beginnen, gilt:
24
CTL* - Komplexe Formeln
G E F a
a a a
a a a
Zustandsformel
Pfadformel
CTL* = Atomare Zustandsaussagen + Boolesche Operatoren + Temporale (Pfad-) Operatoren + Pfadquantoren
25
CTL* - Zusammenfassung
sehr ausdrucksstark
Keine effizienten Algorithmen bekannt
Es gibt effiziente Algorithmen für Fragmentevon CTL*
CTL*
LTL CTL
nur Pfad-formeln
Nur Zust.-formeln
26
Computation Tree Logic (CTL)
CTL = atomare Zustandsaussagen + Boolesche Operatoren + Paare [ Pfadquantor , Temporaloperator ]
AG (invariant) AF (irgendwann)
AX (in allen Nachf.) A( . U . ) (bis)
EG (mgl.weise immer) EF (möglich)
EX (in einem Nachf.) E( . U . ) (bis)
27
CTL –AG und EF
s
s EF grün
s AG blau
Tautologien: AG EF AG AG AG EF EF EF EF AG AG EF AG EF AG EF EF AG EF AG EF AG
28
CTL –EG und AF
s
s AF grün
Tautologienb: EG AF EG EG EG AF AF AF AF EG
s EG blau
29
CTL –AX und EX
s
s EX grün
Tautologien: AX EX AXEX
s AX blau
30
CTL –AU und EU
s
Tautologien: EF E(true U) AF A(true U ) A( U ) EG E( U ( ))
s E(grün U gelb)
s A(blau U rot)
31
Einige relevante CTL-Eigenschaften
AG sicher - nichts Schlimmes passiert jemals
AG eine Aktion enabled - Verklemmungsfrei
AF Ziel - Irgendwann wird man es schaffen
EF Menüpunkt - man kann sich zu ihm durchklicken
AG(req AF ack) -Auf jeden Req folgt ein Ack
AG AF verfügbar - ...es macht Sinn zu warten
AG EF exit - man kann immer sauber beenden
32
Gegenbeispiele
System Abstraktion
Spezifikation
Simulation
Formalisierung
Model Checker
Gegenbeispiel
Modell
log. Formel
+
-
VerfeinerungFehler-beseitigung
Präzisierung
Überlauf
33
Gegenbeispiele für A-Formeln
Gegenbeispiel für... = Zeugenpfad für...
AG EF
AF EG
(AX ) (EX )
A( U )EG oderE( U ( ))
34
Basen für die Temporaloperatoren
LTL : X und U
F true U G F
CTL: (E/A)X und EU und AU
AX EX sonst analog LTL
oder
(E/A)X und EU und EG
A( U ) (EG E( U (
35
Gültigkeit in Transitionssystemen
Ein Transitionssystem erfüllt eine CTL*-Formel , fallszu jedem Anfangszustand der zugehörige Berechnungsbaum erfüllt.
Ein Transitionssystem erfüllt eine LTL-Formel , falls jeder bei einem Anfangszustand beginnende Pfad erfüllt.
Ein Transitionssystem erfüllt eine CTL-Formel , fallsjeder Anfangszustand erfüllt.
Tautologie: A
36
Interessante Probleme
1. Erfüllbarkeit: Geg.: Formel Frage: Gibt es ein Transitionssystem, in dem gilt?
2. Axiomatisierbarkeit: Frage: Gibt es eine endl. Menge von Formeln und Regeln, aus denen sich alle Tautologien ableiten lassen?
3. Model Checking: Geg.: Formel und Transitionssystem TS Frage: Erfüllt TS ?
CTL*: O(2|| |TS|) LTL: O(2|| |TS|) LTL: O(|| |TS|)
37
Übung 1
Gegeben ist folgender Pfad. Die Notation ( ... ) * soll bedeuten,daß sich die eingeklammerte Sequenz bis ins Unendlichewiederholt. Welche Pfadeigenschaften sind erfüllt?
a a,b d a,d b c a,c a,c b,c c( )*
G ((a d) X X G c) G (a F b)
G ( a X b ) ( c) U b (F b) U c
38
Übung 2
Welche der folgenden Formeln sind Tautologien?
F F ( U ) G ( U ) G F
U U X U ( U ) ( ) U
39
Übung 3
Formalisiere folgende Spezifikationen in CTL* (wähle dazu geeignete atomare Aussagen)!
Eine im Bahnhof stehende S-Bahn schließt die Türen,bevor sie abfährt
Es ist nie möglich, vom 2. Gang in den 4. Gang zu schalten,ohne zwischendurch in den 3. Gang geschaltet zu haben
Hinweis: Man braucht wirklich keine Vergangenheitsoperatoren!
Zwei parallele Prozesse schreiben nie gleichzeitig aufdie geteilte Variable x.
Jede Variable ist initialisiert, bevor sie das erste Malbenutzt wird.
Top Related