model checking i - ctl - se.uni- · pdf filemodel checking i - ctl 3 model checking...

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


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


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



• durch Ausführung des Systems entsteht ein Berechnungsbaum, der alle möglichen unendlichen Abläufe des Systems darstellt

• Abläufe werden Pfade genannt



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


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


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


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²


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 φ]


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


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²


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 φ


BeispieleBeispiele

M , s0² p∧q

⇒trueM , s0² EX q∧r

M , s2² AG r⇒true

⇒true


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


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.


Ä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


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)


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


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/

model checking i - ctl - se.uni- · pdf filemodel checking i - ctl 3 model checking...

Documents