Transcript
Temporale Logik und Modelchecking
Seminar Logik für Informatiker
Olaf Böttcher
2/14
Einführung
Quelle: E.Kindler: Vorlesung Modelchecking
3/14
Verifikation Die Verfikationsmethode M ╞ Φ Was ist M ? Was ist Φ ? Was ist ╞ ?
4/14
Was ist M ?
a,b
a,b
b,c
a,b b,c
c
c
c
State Transition Graph
Infinite Computation Tree
c
5/14
Kripkestrukturen Eine Kripkestruktur besteht aus z einer Zustandsmenge, z mit ausgezeichneten Anfangszuständen, z einer (totalen) Übergangsrelation z einer Beschriftung der Zustände mit einer Menge von atomaren Aussagen.
6/14
Was ist Φ ?
• Beschreibt das gewünschte Verhalten des •
Systems in einer Spezifikationssprache Temporale Logik:
• Zukünftige Zustände von Variablen • Zeit: • Diskret oder stetig • Verzweigend oder linear
7/14
CTL Semantik Es existiert ein Pfad, auf dem immer φ gilt. EG φ
8/14
CTL Semantik Auf allen Pfaden gibt es einen Zustand in dem φ gilt. AF φ
9/14
CTL Semantik Es gibt einen erreichbaren Zustand in dem ψ gilt, und bis dahin φ gilt. E[φ U ψ ]
10/14
CTL Syntax/Semantik z
Quantor:
• Operator:
A – Es gilt für alle Pfade E – Es existiert ein Pfad F – „some future state“ G – „generally“ X – „next State“ U – „until“ R – „release“
11/14
Was ist ╞ ? M,s ╞ Φ Modelchecking Wir ermitteln induktiv über den Aufbau der CTL Formel die Menge der Zustände, in denen die Formel gilt: z atomare Aussagen z temporale Operatoren z boolesche Operatoren z
12/14
Beispiel: Mutual Exclusion s0
n1,n2
s1
s2
t1,n2
c1,n2
n1,t2 s5 s3
s4
c1,t2
t1,t2
t1,t2 s8
n1,c2 t1,c2 s7
s6
13/14
Äquivalenzen z z
z
CTL Modelchecking Jede CTL Formel kann durch die Terme ¬,∨, EX, EU und EG dargestellt werden Bsp.: ⌐AF φ ≡ EG ⌐φ ⌐EF φ ≡ AG ⌐φ
14/14
Zusammenfassung z
z z
Modelchecking ermöglicht, die Modellierung eines Systems daraufhin zu überprüfen, ob sie bestimmte Eigenschaften erfüllt. Automatisierte Verifikation Fehleranalyse optimiert
