Formale Methoden Des Software Engineering Sose 13

Front 1

Definition Sprachen

Back 1

Syntax = Symbole und deren Verknüpfung
Benennung (mathematischer) Objekte der realen Welt
Semantik = Funktion mit Syntax als Eingabe und math. Objekt als Ausgabe

Front 2

Definition eines Programmes: Vorgehen

Back 2

Mathematische Objekte der realen Welt definieren
- Wertebereich, operationen
Verwaltung des Programmzustands schaffen
- Lookup Assign
Semantik funktion aufstellen (Verknüpfung Syntax und reale Welt)
- Ausdrücke Expressions / Statements

Front 3

First Order Logic

Back 3

Signatur G
V: Variablen
F: Funktionssymbole (Konstanten = Funktionen mit Stelligkeit 0)
R: Releationssymbole
Terme: Variablen, Konstanten,Funktionen
Formeln: Releationen, Tautologien,UND/ODER rtc
Verküpfungen von Formeln

Front 4

First Order Logic: Struktur S

Back 4

G: Signatur
Definitionsbereich
Menge von Funktionen inkl. Konstanten über
Menge von Relationen über
f: F Eine Funktion die jedem Symbol der Signatur eine entspechende Funktion oder Relation gleicher Stelligkeit über zuweist
Belegung a: V
Semantik eine Terms ist Wert aus dem Definitionsbereich
Semantik einer Formel ist TRUE oder FALSE

Front 5

Definition First Order Logic

Back 5

FOL definiert durch
Zeichen (Signatur der Logik)
Syntaktische Regeln (BNF für Terme und Formeln)
Verknüpfung der mathematischen Objekte (Struktur der Logik)
Auswertungsumgebung (Belegungsfunktion a)
Semantik (Interpretation Ta und Ma)

Front 6

Ausdrucksstärke einer Logik

Back 6

Logik kann bestimmte Eigentschaften ausdrücken, wenn
Die Logik erlaubt Formel aufzuschreiben , die die Eigenschaft beschreibt und
Diese Formel einer Klasse von Strukturen genau dann wahr ist, wenn die Eigenschaft auf den Elementen der Domäne erfüllt

Front 7

Propositionale Logik

Back 7

Teilmenge der FOL
- Keine Quantifizierung
- Keine Funktionssysmbole oder Relationssymbole
Nur propositionale Variablen AP, die die Werte True oder False annehmen können
Keine Terme

Front 8

Beweissysteme - Axiome

Back 8

Besteht aus Schema in dem Schemavariablen auftreten können

Front 9

Beweissysteme - Beweisregeln

Back 9

Besteht aus einer Reihe von Schemata (Prämissen) un der Konsequenz (horizontaler Strich)

Front 10

Beweissysteme - Vorgehen

Back 10

Ersetzen der Schemavariablen durch Teil-Formeln in einem Schema -> Instanz des Schema
Man erhält Menge von FOL Formeln (Prämissen) und eine Formel (Konsequenz)

Front 11

Beweissysteme - Vorwärtsschließen

Back 11

Endliche Folge von nummerierten Formeln
Jede Zeile hat folgende Eingenschaften:
Zeile ist Hypothese aus ....
ist Instanz eines Axioms
folgt aus vorangehenden Beweiszeilen und Anwendung einer Beweisregel

Front 12

Beweissysteme - Rückwärtsschließen

Back 12

Beweisregeln werden Rückwärtsbetrachtet
Konsequenz wird in Teile zerlegt, die Einzeln bewiesen werden

Front 13

Beweissysteme - Korrektheit und Vollständigkeit

Back 13

Korrekt: nur wahre Eigenschaften können abgeleitet werden.
Vollständig: alle wahren Eigenschaften können abgeleitet werden.

Front 14

Transitionssysteme

Back 14

Transitionen (erzeugen Zustände)
formal Tupel S,T,Theta
S ist Struktur mit Signatur G (G enthält Variablen des Programms und Hilfsvariablen)
T: endliche Menge von Transitionen
p: Schaltbedingung (unquantifizierte FOL-Formel)
vi in V: Menge ovn zu verändernden Variablen
ei: Menge von neuen Werten als FOL Formel über G (werden den Variablen bei Übergang zugewiesen)
"p wird unter Struktur S in Zustand s wahr"
Theta: Startzustand

Front 15

Zustandsraum

Back 15

S: Menge von Zuständen
t: Menge von Transitionen
I teilmenge S: Initiale Zustände
Lauf: Folge von Zusatänden s0 in I, (si,si+1)
für gelabelte Zustandsräume Li: Ti-> = Labelingfunktion

Front 16

Parallele Komposition

Back 16

Beispiel vfür Kombination von Zustandsräumen
Gi <S¡,∑i,"",Ii> mit 11,2 Zustandsräiumen mit Benannten Transitionen
Dann: T1||T2 = komibinierter Zustandsraum
(Karthesisches Produkt)

Front 17

Fairness

Back 17

Schwache Prozess Fairness
Starke Prozess Fairness
Schwache Transitions Fairness
Starke Transitions Fairness

Front 18

Fairness - Schwache Prozess Fairness

Back 18

verbietet Schedules mit: es sind ab einem Zustand s immer Transitionen eines Prozesses Pi schaltfähig, es wird aber keine Transition von Pi nach s ausgeführt

Front 19

Fairness - Starke Prozess Fairness

Back 19

verbietet Schedules mit: es sind unendlich oft Transitionen eines Prozesses Pi schaltfähig, aber es werden nur endlich oft Transitionen von Pi ausgeführt

Front 20

Fairness - Schwache Transitions Fairness

Back 20

verbietet Schedules mit: Es ist ab einem Zustand s eine Bestimmte Transition immer schaltfähig, aber sie wird nie nach S ausgeführt

Front 21

Fairness Starke Transitions Fairness

Back 21

verbietet Schedules mit: Es ist nur eine Transition unendlich oft schaltfähig, aber sie wird nur endlich oft ausgeführt.

Front 22

LTL - Definition

Back 22

Struktur S einer statischen Logik
Unendliche Folge von Zuständen
Jeder Zustand hat eine Belegung
Jeder Zeitpunkt hat genau einen Nachfolger und bis X0 alle genau einen Vorgänger

Front 23

LTL Operatoren

Back 23

Nexttime ° Bedingung wird nächstes Mal erfüllt
eventually (Karo) wird irgendwann erfüllt
always (quadrat) wird immer erfüllt
release (V): x gilt solange bis y den Not-Aus drückt -> Keine Eventually garantie
Until (U): x gilt bis y aber nie gleichzeitig

Front 24

Büchiautomat

Back 24

A = ∑ S, Delta, I,L,F
∑ endliches Alphabet
S: endliche Menge von Zuständen
Delta: Transitions-Relation
I teilmenge S Initale Zustände
L:S-> Label der Zustände
F teilmenge S Menge der Akzeptioerenden Zustände

Front 25

Buchiautomat - Lauf

Back 25

Ein Lauf ovn A über ein unendliches Wort u ist unendlich langer Pfad im Graphen von A in dem die Knoten vo A entsprechen der Buchstaben in u markiert sind

Front 26

Modelchecking - Grundidee

Back 26

Software soll auf funktionale Korrektheitgeprüft werden.
Spezifikation A (Logik) und Realisierung B vorhanden
Ein Algorithmus soll entscheiden, ob die Realisierung die Spezifikation erfüllt.
A erfüllt B falls L(A) Teilmenge von L(B)
Jedes Wort, das von der Realisierung akzeptiert wird wird auch von der Spezifikation realisiert.

Front 27

Modelchecking - Transformation LTL Büchi

Back 27

Verienfachung der Formel
Zelegung der Formel in Teilformeln
Erzeugung zu jeder Teilformel

Front 28

Modelchecking - Transformation LTL Büchi - Vereinfachung

Back 28

Ersetzung eventually durch true until phi
Ersetung always durch false release phi
Implikationen auflösen
Negationen direkt vor die Variablen ziehen

Front 29

Modelchecking - Transformation LTL Büchi - Zelegung in Teilformeln

Back 29

LTL-Formeln zerlegen, nur noch propositionale Variablen (negtion normal form)
Jede Teilformel in NNF steht für Zustand, in dem diese Formel gilt.
Abgeleitete Teilformeln intereinander Verbinden, um zustandsfolgen zu erzeugen

Front 30

Modelchecking - Transformation LTL Büchi - Erzeugung von Zuständen zu jeder Teilformel

Back 30

Beschriftung ergibt sich aus negierten und nicht negierten propositionalen Variablen
Leere Menge ergibt true
Akzeptierende Zustände: verallgemeinerter Büchi-Automat
Betrachtung alle Teilformeln phi untel psi
Für jeder solcher Formeln Erstellung akzeptierender Knotenmege mit:
Knoten, deren Bschriftung Psi erfüllt
Knoten, die nichts mit dieser Teilformel zu tun haben.
Umformung verallgemeinerter Büchi-Automaten zu einfachen Büchi Automaten.

Front 31

Modelchecking - Algorithmus

Back 31

Konstruiere Automat A (System)
Kosntruiere Automat B Strich, Komplement der Spezifikation
Konstruiere den Schnittautomaten C
Suche in C starke Zusammenhangskomponente, welche von Initialzustand erreicht werden kann.
Enthält Komponente akzeptierenden Zustand?
Falls nein System A erfüllt Spezifikation B
Falls ja, System A erfüllt B nicht.

Front 32

Modelchecking - Algorithmus 2

Back 32

Konstruieren eines Gegenbeispiels
Wähle akzeptierenden Zustand aus einer Zusammenhangskomponente
Erstelle Pfad p von einen initialen Zustand q
Erstelle einen Zyklus z von q zurück zu sich selbst
Vereinige p mit z. jedes Wort, welches über die Vereinigung anwendbar ist.