Model Checker SPIN

Hauptseminar Modellüberprüfung

Kathrin Ott

15.02.2002

2

SPIN

• Softwarepaket zur formalen Überprüfung von

verteilten Systemen, meist Datenkontrollprotokolle

• Simple Promela INterpreter

• in den 80er Jahren von den Bell Labs entwickelt

• SPIN ist ein kostenlos erhältliches Programm

• jährliche Workshops zu Erweiterung von SPIN

3

SPIN

• Designspezifikationen werden in der

Verifikationssprache PROMELA formuliert

• PROcess MEta LAnguage

• Arbeitsweise:

1. High-Level Model

2. Syntaxfehler

3. Mehrere Durchläufe

4. Ergebnisanalyse zu Generierung neuer Testläufe

• unter Verwendung von Reduktionsalgorithmen werden die

Durchläufe optimiert

4

PROMELA

• C-ähnliche Syntax

• Programmiersprache bestehen aus (ein oder

mehreren) Prozessen, Nachrichtenkanälen und

Variablen

• fünf Arten von Zeichen: Bezeichner, Schlüsselwörter,

Konstanten, Operatoren und Separatoren

5

Temporale Logik

• unterscheidet sich von der normalen Logik durch

zeitliche Gebundenheit

• Aussagen über Verhalten mit einem Zustands-

übergangsgraphen

• endliches Zustandssystem kann als Tupel beschrieben

werden

6

Algorithmen

• M=<S,T,R,L>

• S - endliche Menge von Zuständen

• T S - eine Menge von Grundzuständen

• R SS - Übergangsrelation, die mögliche

Übergänge von Zustand zu Zustand beschreibt

• L ist eine Funktion

7

Temporale Logik

8

LTL

• Lineare Temporale Logik

• jeder Pfad im Zustandsübergangsgraph wird für sich

durch die Formel gewertet

• bis, seit, immer, eventuell, ...

• f ::= p |true |false |(f) |f binop f |unop f

unop ::= | | !

binop ::= U | && | ∥ | |

9

LTL

• z.B.: p bleibt wahr solange bis q wahr wird =

(p U q)

• zu jeder Zeit in der Ausführung wird p zumindest

noch einmal wahr werden

( p)

10

LTL und Automaten

• Erfüllt ein gegebenes System eine gegeben Formel?

• Ja, wenn alle seine Berechnungen die Formel

erfüllen, also seine Sprache eine Teilmenge der

Formelsprache ist

• unendliche Sprache repräsentieren und die Inklusion

testen.

• unendliche Automaten wie den Büchi Automat

11

Büchi Automat

• eine unendliche Folge von Zuständen lässt sich in

einem Büchi Automat darstellen

• eine Formel ist dann erfüllt, wenn ihre Sprache nicht

leer ist, d.h. es gibt einen akzeptierenden Lauf

(unendliche Folge von Zuständen), der unendlich oft

einen Endzustand des Automaten beinhaltet

• wenn es einen unendlichen Weg durch den

Automatengraph gibt, dann gibt es auch einen

erreichbaren Kreis, auf dem der Endzustand liegt

12

LTL -> Büchi Automat

• Büchi Automat der LTL-Formeln

(p U q) ( p)

13

LTL -> PROMELA

$ spin -f „ ( p)“

never {

T0:

if

:: (true) goto T0

:: (p) goto accept

fi;

accept:

if

:: (true) goto T0

fi;

}

14

LTL -> PROMELA

$ spin -f „ (p U q)“

never {

T0:

if

:: (p) goto T0

:: (q) goto accept

fi;

accept:

if

:: ((p) || (q)) goto T0

fi;

}

15

Algorithmen

• SPIN verwendet neben dem Büchi Automaten noch

weitere Algorithmen:

• Partial Order Reduktion

• Tiefensuche

• Bit State Hashing

zur Reduktion von Zeit und Speicher

16

Beispiel: ABP

• Alternating Bit Protocol

• Datentransferprotokoll

• Stop-And-Go-Protokoll

• Datenübertragung zu einem Zeitpunkt und in eine

Richtung

• alternating bit, weil der Sender abwechselnd

(alternatively) 0 und 1 anhängt

17

ABP

Sender EmpfängerUnzuverlässige Datenübertragung

mesg1

mesg1

mesg0

ack0

ack1

ack1

18

ABP in PROMELA Codemtype = { msg0, msg1, ack0, ack1 };

chan sender = [1] of { mtype };chan receiver = [1] of { mtype };

inline phase(msg, good_ack, bad_ack){ do :: sender?good_ack -> break :: sender?bad_ack :: timeout -> if :: receiver!msg; :: skip /* lose message */ fi; od}

inline recv(cur_msg, cur_ack, lst_msg, lst_ack){ do :: receiver?cur_msg -> sender!cur_ack; break /* accept */ :: receiver?lst_msg -> sender!lst_ack od;}

19

ABP in PROMELA Code

active proctype Sender()

{

do

:: phase(msg1, ack1, ack0);

phase(msg0, ack0, ack1)

od

}

active proctype Receiver()

{

do

:: recv(msg1, ack1, msg0, ack0);

recv(msg0, ack0, msg1, ack1)

od

}

Tests: [] (ack1 -> <> mesg1)

20

LTL Anforderungen an ABP

• immer wird nach ack1 eventuell msg1 gesendet

– [] (ack1 -> <> mesg1)

• immer wird nach mesg1 solange nicht ack1 empfangen

bis ack0 empfangen wird

– [] (mesg1 -> (! ack1 U ack0)) (error behavior)

• immer wird nach mesg1 solange nicht ack0 empfangen

bis ack1 empfangen wird

– [] (mesg1 -> (! ack0 U ack1)) (desired behavior)