1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation...

39
1 Computergestützte Verifikation 19.4.2002

Transcript of 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation...

Page 1: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

1

Computergestützte Verifikation

19.4.2002

Page 2: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

2

Inhalt

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Kapitel 1: Systeme

Page 3: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 4: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

4

Kapitel 2

Temporale Logik

Page 5: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 6: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 7: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 8: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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}

Page 9: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 10: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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)

Page 11: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 12: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 13: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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 .....

Page 14: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 15: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 16: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 17: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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)

Page 18: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 19: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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.

Page 20: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 21: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 22: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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)

Page 23: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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:

Page 24: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 25: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 26: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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)

Page 27: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 28: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

28

CTL –EG und AF

s

s AF grün

Tautologienb: EG AF EG EG EG AF AF AF AF EG

s EG blau

Page 29: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

29

CTL –AX und EX

s

s EX grün

Tautologien: AX EX AXEX

s AX blau

Page 30: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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)

Page 31: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 32: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

32

Gegenbeispiele

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Page 33: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

33

Gegenbeispiele für A-Formeln

Gegenbeispiel für... = Zeugenpfad für...

AG EF

AF EG

(AX ) (EX )

A( U )EG oderE( U ( ))

Page 34: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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 (

Page 35: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 36: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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|)

Page 37: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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

Page 38: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

38

Übung 2

Welche der folgenden Formeln sind Tautologien?

F F ( U ) G ( U ) G F

U U X U ( U ) ( ) U

Page 39: 1 Computergestützte Verifikation 19.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

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.