model checking i - ctl - se.uni- · pdf filemodel checking i - ctl 3 model checking...
Post on 06-Feb-2018
213 Views
Preview:
TRANSCRIPT
Werkzeuggestützte Softwareprüfungen:Werkzeuggestützte Softwareprüfungen:
Model Checking I - CTLModel Checking I - CTL
Vortrag vonFlorian Heyer
2Model Checking I - CTL
GliederungGliederung
• Wiederholung• Einführung• CTL im Detail• Anwendungsbeispiele• Abschluss
3Model Checking I - CTL
Model Checking (Wiederholung)Model Checking (Wiederholung)
• Überprüfung einer Systembeschreibung auf Anforderungen• dies soll automatisiert ablaufen• hierzu kommt ein Model Checker zum Einsatz: eine Software,
die die Überprüfung des Systems durchführen kann• Eingaben für den Model Checker sind:
– eine Beschreibung des zu untersuchenden Systems als Zustandsübergangssystem
– eine Menge von geforderten Eigenschaften des System, die hier in temporaler Logik formuliert sein sollen
• der Model Checker liefert eines der folgenden Ergebnisse:– das System besitzt die geforderten Eigenschaften– das System verletzt die Anforderungen; in diesem Fall liefert der Model
Checker ein Beispiel eines Systemdurchlaufs, welcher eine geforderte Eigenschaft verletzt
4Model Checking I - CTL
EinführungEinführung
• Zustandsübergangssystem als Modell eines zu untersuchenden Systems– Zustände– Transitionen zwischen den
Zuständen– Zustandsaussagen
• Zustandsübergangssysteme können übersichtlich als Graphen dargestellt werden
5Model Checking I - CTL
EinführungEinführung
• durch Ausführung des Systems entsteht ein Berechnungsbaum, der alle möglichen unendlichen Abläufe des Systems darstellt
• Abläufe werden Pfade genannt
6Model Checking I - CTL
EinführungEinführung
• beim Model Checking müssen Anforderungen an das System formuliert werden
• hierfür werden temporale Logiken genutzt– diese sind eine Erweiterung der Aussagenlogik um temporale
Operatoren– ermöglichen zeitliche Einschränkungen der Gültigkeit von Aussagen
(z.B. „immer“ oder „manchmal“)– temporale Logik ist eine spezielle modale Logik (Verwendung von
Modaloperatoren zum Ausdruck von Modalitäten)
7Model Checking I - CTL
Temporale LogikenTemporale Logiken
• LTL - Linear-time Temporal Logic (~1960)– älteste temporale Logik– lineares Zeitmodell– Aussagen gelten immer für alle Pfade
• CTL - Computation Tree Logic (~1980)– Zeit als Baum– Verzweigung in unterschiedliche Versionen der Zukunft (Pfade)– Aussagen können auf bestimmte Pfade beschränkt werden
• CTL* (1986)– später entwickelt als Erweiterung der Ausdrucksmöglichkeiten von CTL
und LTL– Zeit als Baum– freie Verschachtelung der Temporaloperatoren
8Model Checking I - CTL
Temporale LogikenTemporale Logiken
• Ausdrucksumfang der temporalen Logiken– es gibt Ausdrücke, die sich
zwar in LTL, nicht jedoch in CTL ausdrücken lassen und umgekehrt
– CTL* ist Obermenge von LTL und CTL
9Model Checking I - CTL
Semantik von CTL-FormelnSemantik von CTL-Formeln
• CTL-Formeln beziehen sich auf einen Zustand s im Modell M• Für eine Formel φ überprüft der Model-Checker die
Erfüllbarkeitsrelation
• häufigste Anwendung des Model Checkers:– erfüllen alle Zustände des Modells eine bestimmte Anforderung (=CTL-
Formel)?– die Antwort ist entweder true oder false – bei false wird meist der Durchlauf ausgegeben, welcher die
Anforderung verletzt hat
M , s²
10Model Checking I - CTL
Aufbau von CTL-FormelnAufbau von CTL-Formeln
• CTL-Formeln bestehen aus den folgenden Elementen– Konstanten true und false– atomare Zustandsaussagen– boolesche Operatoren (not, and, or, Implikation)– zusammengesetzte Operatoren, bestehend aus Pfadquantoren und
Temporaloperatoren
• Backus-Naur-Form von CTL-Formeln φ:
φ ::= ⊥ | T | p | (¬φ) | (φ ∧ φ) | (φ ∨ φ) | (φ → φ) | <compositeOp><compositeOp> ::= A<temporalOp> | E<temporalOp><temporalOp> ::= X φ | F φ | G φ | [φ U φ]
11Model Checking I - CTL
Zusammengesetzte Operatoren (<compositeOp>)Zusammengesetzte Operatoren (<compositeOp>)
• bestehen aus Paaren von Pfadquantor und Temporaloperator• Pfadquantoren
– A - All: Aussage gilt für alle in s beginnenden Pfade– E - Exists: Aussage gilt für mindestens einen Pfad, der in s beginnt
• Temporaloperatoren (bezogen auf die Zukunft)– unär
• X – neXt: Aussage gilt im nächsten Zustand• F – Future: Aussage gilt in Zustand in der Zukunft• G – Global: Aussage gilt für kompletten Pfad
– binär• U – Until: Aussage1 gilt für alle Zustände bis Aussage2 gilt und Aussage2
wird gelten
• es ergeben sich somit 2*4=8 zusammengesetzte Operatoren namens: AX, AF, AG, AU, EX, EF, EG, EU
12Model Checking I - CTL
Definition der ErfüllbarkeitsrelationDefinition der Erfüllbarkeitsrelation
• die Erfüllbarkeitsrelation lässt sich fallweise definieren• Konstanten
––
• Atomare Aussagen–
• Boolesche Operatoren
–
–
–
–
M , s² p gdw. p L s
M , s²
M , s²∧ gdw. M , s² and M , s²M , s²∨ gdw. M , s² or M , s²
M , s 2
M , s² gdw. M , s 2
M , s² gdw. M , s 2 or M , s²
13Model Checking I - CTL
Definition der ErfüllbarkeitsrelationDefinition der Erfüllbarkeitsrelation
• Zusammengesetzte Operatoren– AX φ gdw. in jedem nächsten Zustand gilt φ– AF φ gdw. man erreicht immer einen Zustand, der φ erfüllt– AG φ gdw. in allen Pfaden gilt φ– A[φ U ψ] gdw. es gilt immer φ bis zum ersten Auftreten von ψ– EX φ gdw. in (mind.) einem nächsten Zustand gilt φ– EF φ gdw. in (mind.) einem der folgenden Zustände gilt φ– EG φ gdw. es gibt (mind.) einen Pfad, so dass φ entlang des ganzen
Pfades gilt– E[φ U ψ] gdw. es gibt einen Pfad für den gilt: bis zum ersten Auftreten
von ψ gilt φ
14Model Checking I - CTL
BeispieleBeispiele
M , s0² p∧q
⇒trueM , s0² EX q∧r
M , s2² AG r⇒true
⇒true
15Model Checking I - CTL
BeispieleBeispiele
• Ein aufwärts fahrender Lift in der 2. Etage wechselt nicht die Richtung, falls Passagiere in den 5. Stock wollen:
• AG(etage2 ∧ aufwärts ∧ taste5 → A[aufwärts U etage5])
16Model Checking I - CTL
AnwendungsbeispieleAnwendungsbeispiele
• NuSMV– NuSMV is a symbolic model checker– NuSMV is a reimplementation and extension of SMV, the first model
checker based on BDDs.
• UPPAAL– Uppaal is an integrated tool environment for modeling, validation and
verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).
– The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark.
17Model Checking I - CTL
Äquivalente CTL-FormelnÄquivalente CTL-Formeln
• Semantische Äquivalenz von CTL-Formeln– Definition: zwei Formeln sind dann äquivalent, wenn ein beliebiger
Zustand aus einem beliebigen Modell, der die eine Formel erfüllt, auch die andere Formel erfüllt.
– ermöglicht Ersetzung von Ausdrücken durch äquivalente Ausdrücke– es ergibt sich eine Menge von adäquaten temporalen Operatoren, mit
denen sich CTL komplett ausdrücken lässt: AF, EU, EX– die booleschen Operatoren und Konstanten lassen sich ebenfalls auf
eine adäquate Menge beschränken: ¬, ∧, ⊥
• Beispiel: De-Morgan-Gesetze
AFEGEF AGAX EX
18Model Checking I - CTL
Algorithmen für die VerifikationAlgorithmen für die Verifikation
• Markierungsalgorithmus (labelling algorithm)– Eingabe: ein Modell M und eine CTL-Formel φ– Ausgabe: alle Zustände in M, die φ erfüllen– Effizienz O(f * V * (V + E)) mit
• f Anzahl der Operatoren in φ• V Anzahl der Zustände• E Anzahl der Zustandsübergänge
– somit linear zur Größe der Formel, quadratisch zur Größe des Zustandsübergangsgraphen
– Effizienz nach Optimierung: O(f * (V + E))
• Symbolisches Model Checking– erstmalig im Model Checker SMV verwendet (~1998)– verwendet OBDD (ordered binary decision diagrams)
19Model Checking I - CTL
Fazit Model-Checking mit CTLFazit Model-Checking mit CTL
• wird durch vielfältige Tools gut unterstützt• wird in der Praxis eingesetzt• ist aktuelles Lehr- und Forschungsthema• Aber:
– Abstraktion des realen Systems in ein formales Modell ist schwierig– CTL-Formeln höchst komplex– state explosion problem
• effiziente Datenstrukturen (OBDD)• Abstraktion• Partial order reduction: Reduktion der Zustandsmenge bei kommutativen
parallelen Transitionen• Dekomposition des betrachteten Systems
20Model Checking I - CTL
QuellenQuellen
• Michael Huth, Mark Ryan: „Logic in Computer Science - Modelling and Reasoning about Systems“, Cambridge University Press, 2004.
• Übersicht über Applikationen zum Thema Model Checking:http://www.pst.ifi.lmu.de/lehre/SS06/modelcheck/mc-list.html
• Homepage zur Applikation UPPAAL:http://www.uppaal.com/
• Homepage zu Applikation NuSMV:http://nusmv.irst.itc.it/
top related