Eigenschaftsprüfung

Model Checking mit temporaler Logik

Sprache, Modell, Methode

Die formale Verifikation digitaler Systeme erfordert:• ein mathematisches Modell des Systems, was die zu

verifizierenden Eigenschaften genau genug erfasst• eine zu dem Modell passende Sprache, in der die für uns wichtigen Eigenschaften des Modells formuliert werden können• eine Methode, die überprüft, ob eine in dieser Sprache formulierte Eigenschaft für das Modell gültig ist.

Möglicher Ansatz

Modell:Beschreibung des mikroelektronischen Systems auf unterschiedlichen Abstraktionsebenen (Mehrebenenmodellierung)

Sprache: Prädikatenlogik

Methode: allgemeine Verfahren des automatischen Beweisens

Denkbarer allgemeiner Ansatz:

Problem: je genauer das Modell und je ausdrucksfähiger die Sprache desto komplexer die Beweismethode!

Industrielle Praxis

Welche Eigenschaften eines digitalen mikroelektronischen Systemssollen überhaupt betrachtet werden?

Problemeingrenzung:

Wir beschränken uns darauf, zu untersuchen, welche Signalwerte bzw. welche Booleschen Zusammenhänge für die Signalwerte unter Berücksichtigung bestimmter zeitlicher Umstände gelten

⇒ Aussagenlogik erweitert um modallogische und temporale Operatoren

Beispiel

Eine Nebenstraße kreuzt eine vielbefahrene Hauptstraße. Der Verkehr soll durch eine Ampelsteuerung mit einer Kontaktschleife für die Nebenstraße gesteuert werden.

Die Hauptstraßenampel zeigt mindestens für eine Zeitperiode T (lange Periode) grün an. Ist die Zeit T verstrichen und befindet sich dann ein Fahrzeug auf der Kontaktschleife, schaltet die Hauptstraßenampel erst auf gelb und dann auf rot. Die Gelbphase dauert eine Periode t (kurze Periode). Die Nebenstraßenampel wechselt entsprechend von rot auf grün. (Zur Vereinfachung gibt es keine Rotgelbphase.) Sobald alle Autos durchgefahren sind, spätestens aber nach der Zeit T, geht die Nebenstraßenampel auf gelb und nach der Periode t wieder auf rot. Jetzt geht die Hauptstraßenampel auf grün.

Ampelsteuerung mit Kontaktschleife

Beispiel – Implementierung Implementierung durch folgende Blöcke und Signale:

Sensor:setzt das Signal car auf 1, falls ein Fahrzeug auf der Kontaktschleife steht

Beachte: das Erscheinen eines Fahrzeuges wird durch ein Zufallssignal z modelliert

Zeitgeber:wird zurückgesetzt, falls start = 1. Nach dem Rücksetzen ist zunächst timeout = 0 und Timeout = 0. Zum Zeitpunkt t nach dem Rücksetzten wird timeout auf 1 gesetzt. Zum Zeitpunkt T wird Timeout auf 1 gesetzt. Beide Signale bleiben 1 bis wieder

rückgesetzt wird.

Beachte: zur Vereinfachung der Implementierung werden die Perioden t und T durch ein Zufallssignal r implementiert, (falls r = 1 gilt, ist die Periode zu Ende)

Beispiel – Implementierung

Implementierung durch folgende Blöcke und Signale:

Nebenstraßensteuerung:

durchläuft einen Ampelzyklus gesteuert durch den Zeitgeber, falls Hauptstraßensteuerung enable_n = 1 setzt und car = 1 erfüllt ist.

Hauptstraßensteuerung:

durchläuft einen Ampelzyklus gesteuert durch den Zeitgeber, falls Nebenstraßensteuerung enable_h = 1 setzt.

Beispiel - Blockschaltbild

Nebenstraßen-steuerung

Hauptstraßen-steuerungZeitgeber

Sensorcar

Timeouttimeout

start_n

start_h start

enable_h

enable_n

Blockschaltbild der Ampelsteuerung

Beispiel – Zustandsdiagramme

START t

T

Nein Ja

start oder !r !start und !r / timeout

!start und r / timeout

!start / timeout, Timeout

start / timeout, Timeout

start / timeout

!start und r

!z z / car

z

!z / car

Zeitgeber

Sensor

Beispiel –Zustandsdiagramme

grün gelb

rot

grün gelb

rot

!car oder !Timeout

car und Timeout / start_h

!timeout

timeout / enable_n

!enable_h

enable_h / start_h

car und !Timeout !timeout

!car oder Timeout / start_n

timeout / enable_h

!enable_n

enable_n / start_n

Hauptstraßensteuerung Nebenstraßensteuerung

Beispiel - Verifikation

Welche Eigenschaften sollen (formal) verifiziert werden?

z.B.:

1) Die Hauptstraße und die Nebenstraße haben nicht gleichzeitig grün.2) Wenn auf der Nebenstraße ein Auto kommt, dann bekommt es irgendwann grün.3) Die Hauptstraße hat irgendwann sicher grün, egal was auf der Nebenstraße passiert.

usw.

Modale OperatorenFeststellung der Gültigkeit von Aussagen unter Berücksichtigung zeitlicher Umstände (Modalitäten)

Erweiterung der Aussagenlogik um modale Operatoren E und A zur Beschreibung von Möglichkeit und Notwendigkeit (modallogische Aussagenlogik)

• Ist p eine Formel, dann ist auch Ep eine Formel (lies: "es ist möglich, dass p gilt")

• Ist p eine Formel, dann ist auch Ap eine Formel (lies: "es ist notwendig, dass p gilt")

z.B.: p: "es regnet", Ep: "es ist möglich, dass es regnet" (je nach Ort, Zeit)

CTLNähere Beschreibung der Umstände durch zeitliche Angaben

⇒ Modellierung der Zeit in CTL (computation tree logic)

1) Diskrete Zeit: Jeder Zeitpunkt hat genau einen unmittelbar nachfolgenden und unmittelbar vorausgegangenen Zeitpunkt

2) Linearität: für beliebige Zeitpunkte t1 und t2 gilt stets genau eine der drei folgenden Beziehungen:

t1 < t2, t1 > t2, t1 = t2

3) Baumartig verzweigender Zeitstruktur (branching time temporal logic)

Computation Tree

grün gelb

rot

Abrollen eines Zustandsdiagramms in einen (unendlichen) Baum

Darstellung eines Zustandsdiagramms als computation tree

grün

rot

rot

grün grün rotgelb

rot gelb

Temporale Operatoren

Erweiterung der modallogischen Aussagenlogik um temporale Operatoren: F, G, X, U

• Ist p eine Formel, dann ist auch Fp eine Formel. (lies: "zu mindestens einemzukünftigen Zeitpunkt wird p gültig sein")

• Ist p eine Formel, dann ist auch Gp eine Formel. (lies: "zu jedem zukünftigen Zeitpunkt wird p gültig sein")

• Ist p eine Formel, dann ist auch Xp eine Formel. (lies: "zum nächstenZeitpunkt wird p gültig sein")

• Sind p und q eine Formel, dann ist auch p U q eine Formel. (lies: "zu einem zukünftigen Zeitpunkt wird q gültig sein, bis zu diesem Zeitpunkt wird p gültig sein")

Kripke-Modell Die Semantik von CTL beruht auf dem Kripke-Modell:

Definition:

Ein Kripke-Modell ist ein Quintupel K = (S, S0, R, A, l). Dabei ist:S: eine endliche Menge von Zuständen

S0: eine Menge von Anfangszuständen mit S0 ⊆ S

R: eine Übergangsrelation, R ⊆ S × S, die die möglichenZustandsübergänge des Modells beschreibt

A: eine Menge von atomaren Formeln, A = {p, q, ...}, die jeweils den Wert true oder false annehmen können

l: eine Funktion, l: A → 2S, die für jede atomare Formel aus A die Menge aller Zustände aus S angibt, für welche die atomare Formel gültig (true) ist

Das Kripke-Modell kann leicht aus der Zustandsgraphbeschreibung eines digitalen Schaltwerkes gewonnen werden.

CTL-Syntax

Definition: (CTL-Syntax)

Jede atomare Formel ist eine CTL-Formel. Sind p und q CTL-Formel dann sind auch

¬p, p ∧ q, p ∨ q, EXp, E(pUq), EGp, EFp, AXp, A(pUq), AGp, Afp CTL-Formeln.

Beachte:

Die fettgedruckten CTL-Formeln sind ausreichend, alle anderen können daraus hergeleitet werden. Nach den modalen Operatoren (A, E) muss stets ein temporaler Operator (F, G, U, X) folgen. Jedem temporalen Operator muss ein modaler Operator vorangehen.

Notation: K, s f heißt, dass im Zustand s des Kripke-Modells K die Formel f gültig ist (der Einfachheit halber wird K im Folgenden meist weggelassen).

Seien f und g beliebige CTL-Formeln. Die Semantik von CTL bzgl. eines Kripke-Modells K = (S, S0, R, A, l) ist wie folgt:

s p ⇔ s ∈ l(p), für p ∈ As ¬f ⇔ f ist im Zustand s nicht gültig (false)s f ∧ g ⇔ s f und s gs f ∨ g ⇔ s f oder s g s0 AXf ⇔ für alle Pfade (s0, s1, s2, ...) ist s1 fs0 EXf ⇔ es existiert ein Pfad (s0, s1, s2, ...), so dass s1 fs0 A(f U g) ⇔ für alle Pfade (s0, s1, s2, ..., si,... ) existiert ein i mit i ≥ 0, so

daß si g und es gilt sj f für alle 0 ≤ j < is0 E(f U g) ⇔ es existiert ein Pfad (s0, s1, s2, ..., si,... ), für den ein i mit i ≥ 0

existiert, so daß si g und es gilt sj f für alle 0 ≤ j < is0 AGf ⇔ für alle Pfade (s0, s1, s2, ...) ist s0 f, s1 f, s2 f, ...s0 EGf ⇔ es existiert ein Pfad (s0, s1, s2, ...), so dass s0 f, s1 f, s2 f, ...s0 AFf ⇔ für alle Pfade (s0, s1, s2, ..., si,... ) existiert ein i mit i ≥ 0, so dass si fs0 EFf ⇔ es existiert ein Pfad (s0, s1, s2, ..., si,... ) für den ein i mit i ≥ 0 existiert,

so dass si f

CTL-Semantik

Beobachtungen

Anmerkung 1:

Bei CTL gehört die Zukunft mit zur Gegenwart.

Anmerkung 2:

Im Folgenden identifizieren wir eine CTL-Formel f mit einer Teilmenge S' der Zustandsmenge S eines Kripke-Modells. Dann bezeichnet f ∧ g die Schnittmenge der Zustandsmenge, in der f gilt und der Zustandsmenge, in der q gilt. Entsprechend bezeichnet f ∨g die Vereinigungsmenge von f mit g und es bezeichnet ¬f die Komplementmenge von f. True bezeichnet die Menge aller Zustände und false die leere Menge.

CTL Model CheckingAllgemeine Vorgehensweise zur Verifikation einer Eigenschaft in einem Kripke-Modell K:

• formuliere die zu verifizierende Eigenschaft als CTL-Formel f

• werte die Formel aus, d.h. berechne alle Zustände des Kripke-Modells, für die die Formel gültig ist

• die Eigenschaft ist verifiziert, genau dann wenn S0 ⊆ f

Wichtig: bei der Verifikation einer mikroelektronischen Schaltung dürfen in den CTL-Formeln keine Variablen auftreten, die lediglich von den Schaltungseingängen abhängen. Alle Variablen einer CTL-Formel

müssen als Funktion der Zustandsvariablen beschreibbar sein.

Beispiel – Ampelsteuerung

Formulierung zu verifizierender Eigenschaften in CTL:

1) Die Hauptstraße und die Nebenstraße haben nicht gleichzeitig grün.

Sei haupt_grün ein nur von Zustandssignalen abhängiges Signal, welches 1 ist, falls die Hautstraßensteuerung im Zustand grün ist. Entsprechend sei neben_grün ein nur von Zustandssignalen abhängiges Signal der Nebenstraßensteuerung:

AG(¬(haupt_grün ∧ neben_grün))

Beispiel – Ampelsteuerung

2) Wenn auf der Nebenstraße ein Auto kommt und die Hauptstraßenampel war mindestens für eine Periode T grün, dann wird die Nebenstraßenampel irgendwann grün.

AG((car ∧ Timeout) → AF neben_grün)

3) Die Hauptstraße hat irgendwann sicher grün, egal was auf der Nebenstraße passiert.

AG(AF haupt_grün)

Ergebnis

zu 1) Verifikation erfolgreich

zu 2) Verifikation scheitert !

zu 3) Verifikation scheitert !

Problem: Zeitgeber schaltet nur weiter, falls Zufallsvariable r den Wert 1 liefert. Dies ist aber nicht garantiert.

FAIR CTLErweiterung von CTL auf Fair CTL

Definition: Sei f eine Formel in CTL und π = (s0, s1, s2... ) ein Pfad, entlang dessen die Formel f in unendlich vielen Zuständen gültig ist. Dann heißt π fairer Pfad bezüglich f. ("Büchi-Fairness") Ein fairer Zustand ist ein Zustand, der auf einem fairen Pfad liegt.

Syntax von Fair CTL: Zusätzlich zu der zu verifizierenden CTL-Formel wird eine Menge von CTL-Formeln angegeben, die als fairness constraintsbezeichnet werden. Sonst wie CTL.

Semantik von Fair CTL: Die modalen Operatoren E und A (Pfadquantifizierer) berücksichtigen nur die Pfade, die bzgl. der angegebenen fairness constraints faire Pfade sind. Sonst wie CTL.

(Im Folgenden sprechen wir der Einfachheit halber von CTL, auch wenn Fair CTL gemeint ist.)

Beispiel

Seien zSTART und zt Zustandsvariable, die den Wert 1 annehmen, wenn sich der Zeitgeber in den mit START bzw. t bezeichneten Zuständen befindet.

Fairness constraints zur Verifikation der Ampelsteuerung:

¬zSTART¬zt

Damit wird ausgeschlossen, dass der Zeitgeber irgendwann einen der Zustände t oder START nie wieder verlässt.

CTL-Formeln

Beispiele für häufig benutzte CTL-Formeln

1. Nichts schlimmes kann jemals passieren. (¬p sei was schlimmes (z.B. verbotener Zustand))

AGp

2. Unendlich oft tritt p ein.AGAFp

3. Irgendwann tritt sicher p ein.AFp

4. Irgendwann beschränkt sich das System auf Zustände, wo p immer gilt.AFAGp

CTL Formeln

5. Egal, welche Zustände irgendwann erreicht werden, immer wenn p gilt, dann wird zu einem späteren Zeitpunkt q gelten. "freedom of starvation"

AG(p → AFq)

6. Egal, welche Zustände irgendwann erreicht werden, p wird zu einemspäteren Zeitpunkt immer möglich sein. "Liveness"

AGEFp

7. Berechne alle Zustände, die das System jemals annehmen kann.AG true

8. Es ist möglich, dass irgendwann p gilt.EFp

Fixpunktcharakterisierungvon CTL-Operatoren

Notationen:

Ein Funktional (Abbildung zwischen Mengen von Abbildungen) τ wird im Folgenden mit λy.f bezeichnet, wobei f eine Formel darstellt und yeine in f enthaltene Variable. Wird das Funktional auf eine Formel pangewandt, dann wird in f die Variable y durch die Formel p ersetzt.

Im Folgenden wenden wir Funktionale stets auf CTL-Formeln an.

Beispiel: Anwendung von Funktionalen auf aussagenlogische Formeln

gegeben: τ = λy.(x ∨ y), p = false

berechne τ(p): τ(p) = τ(false) = x ∨ false = x

Fixpunktcharakterisierung

Definition: Eine Formel p heißt Fixpunkt eines Funktionals τ, genau dann wenn gilt: τ(p) = p.

Beispiel: gegeben: τ = λy.(x ∨ y), p = x ∨ z

τ(p) = τ(x ∨ p) = x ∨ ( x ∨ z) = x ∨ z = p

Definition: Ein Funktional τ heißt monoton, genau dann wenn gilt:

p ⊆ q ⇒ τ(p) ⊆ τ(q)

Beispiel: gegeben: τ = λy.(x ∨ y) und p, q mit p ⊆ q

Es gilt: p ⊆ q ⇒ (x ∨ p) ⊆ (x ∨ q)

Fixpunkteallgemein gilt:

Jedes monotone Funktional τ = λy.f hat einen kleinsten Fixpunkt µy.f, der durch die Schnittmenge aller Fixpunkte gegeben ist, und es hat einen größten Fixpunkt νy.f, der durch die Vereinigung aller Fixpunkte gegeben ist [Tars55].

Notation:

τi(p) bezeichnet die Formel (Menge), die nach dem i-ten Iterationschritt des Funktionals für die Anfangsformel p vorliegt. (i-fache funktionale Komposition von τ mit sich selbst)

∪iτi(p) bezeichnet die Vereinigung aller Formeln, die durch Iteration des Funktionals ausgehend von der Anfangsformel p entstehen.

∩iτi(p) bezeichnet den Schnitt aller Formeln, die durch Iteration des Funktionals ausgehend von der Anfangsformel p entstehen.

Beispiel

gegeben: - ein Kripke-Modell K mit einer Zustandsmenge S- eine Menge S0 mit S0 ∈ S

Problemstellung: berechne die Zustände R, die in K von S0 aus erreichtwerden können

reach(S0): Prozedur zur Berechnung von R für gegebenes S0

xreach(A): Prozedur zur Berechnung aller Zustände, die ausgehend von der Zustandsmenge A in einem Schritt erreicht werden können(unmittelbare Nachfolger von A)

reach(S0){

Rit := ∅;do{

R := Rit;Rit := S0 ∪ xreach(R);

} until (R == Rit)return R;

}Prozedur zur Berechnung von R

Beispielbetrachte reach() und xreach() als Operatoren einer Logik basierend auf einem Kripke-Modell K:

(Mit jeder Formel p assoziieren wir die Zustände des Kripke-Modells, in denen die Formel gültig ist)

REACH(p): ist wahr für alle Zustände in K, die von den Zuständen, in denen p wahr ist, erreichbar sind

XREACH(p): ist wahr für alle Zustände in K, die von den Zuständen, indenen p wahr ist, in einem Schritt erreichbar sind

Sei τ = λy.(p ∨ XREACH(y)) ein Funktional und µy.(p ∨ XREACH(y)) sein kleinster Fixpunkt. Offensichtlich gilt:

REACH(p)= µy.(p ∨ XREACH(y)) = ∪i(λy.(p ∨ XREACH(y)))i (false)

Beispielp

Beispiel zur Anwendung von λy.(p ∨ XREACH(y))

τ0 = false

p

τ1 = p ∨ XREACH(false) = p

py

τ2 = p ∨ XREACH(p)

pyy y

τ3 = p ∨ XREACH(p ∨ XREACH(p))τ4 = τ3

pyy yy

Durchführung der Fixpunktiteration:

"y" markiert die jeweilsberechnete Zustands-menge.

Vereinigungsstetig Definition: Ein Funktional τ heißt vereinigungsstetig, wenn für eine beliebige

unendliche Folge p0, p1, p2 ... mit p0 ⊆ p1 ⊆ p2 ... gilt: ∪iτ(pi) = τ(∪i pi).Entsprechend heißt ein Funktional τ schnittstetig, wenn für eine beliebige unendliche Folge p0, p1, p2 ... mit p0 ⊇ p1 ⊇ p2 ... gilt: ∩iτ(pi) = τ(∩i pi).

Lemma: Sei τ = λy.f ein monotones Funktional und f eine CTL-Formel. Dann ist τ auch vereinigungs- und schnittstetig.

Satz: Sei τ = λy.f ein monotones Funktional und f eine CTL-Formel. Dann gilt:

µy.f = ∪iτi(false)

νy.f = ∩iτi(true)

Berechnung von CTL-Formeln

Satz: Für ein beliebiges Kripke-Modell K gilt:

EFp = µy.(p ∨ EXy)

EGp = νy.(p ∧ EXy)

E(p U q) = µy.(q ∨ (p ∧ EXy))

Da die betrachteten Funktionale monoton sind, folgt:

EFp = ∪i(λy.(p ∨ EXy))i (false)

EGp = ∩i(λy.(p ∧ EXy))i (true)

E(p U q) = ∪i(λy.(q ∨ (p ∧ EXy))i (false)

Beispiel

p

Beispiel zur Anwendung von EFp = µy.(p ∨ EXy)

τ0 = false

p

τ1 = p ∨ EX(false) = p

p

y

τ2 = p ∨ EXp

p

yy

τ3 = p ∨ EX(p ∨ EXp)τ4 = τ3

pyy y

Durchführung der Fixpunktiteration:

Beispiel

pp py yyy

Beispiel zur Anwendung von EGp = νy.(p ∧ EXy)

τ0 = true

pp py yyy

τ1 = p ∧ EX(true) = p

pp pyyy

τ2 = p ∧ EXp

pp pyy

τ3 = p ∧ EX(p ∧ EXp)τ4 = τ3

pp py

Durchführung der Fixpunktiteration:

Fairness Constraints

Es bezeichne C = {ck} eine Menge von fairness constraints (CTL-Formeln) und EC f die Zustände für die Ef unter Berücksichtigung der fairness constraints C gültig ist.

(d.h.: Formel ECGp ist gültig, falls ein Pfad existiert, so daß entlang dieses Pfades jede Formel ck ∈ C unendlich oft gültig ist und in jedem Zustand pgilt.)

Es gilt: ECGp = ∩i(λy.(p ∧ EX ∧ E(y U y ∧ ck)))i (true)ck ∈ C

Eigenschaften

Da die fairen Zustände eines Kripke-Modells durch ECG true charakterisiert sind, gilt für die restlichen CTL-Operatoren:

ECXp = EX(p ∧ ECG true)

ECFp = EF(p ∧ ECG true)

EC(q U p) = E(q U (p ∧ ECG true))

AlgorithmusGegeben: ein Kripke-Modell K mit Zustandsmenge S und eine CTL-Formel fAufgabe: werte f aus, d.h. berechne alle Zustände Sf in K, in denen f gültig ist

Vorgehensweise:

Sei comp(f) eine Prozedur zur Lösung dieser Aufgabe. Dazu betrachten wir folgende Unterfunktionen:

-compEX(Sf) eine Prozedur zur Auswertung von EXf für bekanntes Sf-compEU(Sq, Sp, Y) eine Prozedur zur Auswertung von E(q U p) für bekannte Sq und Sp (mittels einer Fixpunktiteration über Y)-compEG(Sf) eine Prozedur zur Auswertung von EGf für bekanntes Sf(mittels einer Fixpunktiteration über Y)

Die CTL-Formel wird rekursiv von innen nach außen berechnet. Alle Operatoren werden auf Fixpunktiterationen basierend auf der Berechnung von EXy zurückgeführt.

comp(f){switch (syntaktische Form von f){

case: f ist atomare FormelSf := {si ∈ S | si f};

case: f ist von der Form ¬pSf := S \ comp(p);

case: f ist von der Form (p ∨ q)Sf := comp(p) ∪ comp(q);

case: f ist von der Form EXpSf := compEX(comp(p));

case: f ist von der Form E(p U q)Sf := compEU(comp(p), comp(q), false);

case: f ist von der Form EGpSf := compEG(comp(p), true);

}return Sf;

}

Routine zur Auswertung einer CTL-Formel

Unterprozeduren zur Auswertung einer CTL-Formel

compEX(Sp){

return (alle unmittelbaren Vorgänger der Elemente von Sp );}

compEU(Sp, Sq, Y){

Yit := Y;do {

Y := Yit;Yit := Sq ∪ (Sp ∩ compEX(Y));

} until (Yit == Y)return Y;

}

compEG(Sp, Y){

Yit := Y;do {

Y := Yit;Yit := Sp ∩ compEX(Y));

} until (Yit == Y)return Y;

}