MoSeS: Modellierung, Spezifikation und Semantik

[+] Klausur-Programme:

Hoare-Spezifikation $\{P\}\,c\,\{Q\}$

WHILE-Sprache

Vorbedingung $\{P\}$: Initialer Zustand

Programmcode $c$: Befehlsfolge

Schleifeninvariante $\{I\}$: Gilt vor/nach jeder Iteration

Nachbedingung $\{Q\}$: Zielzustand

✓ Partiell Korrekt

⚡ Angewendete Hoare-Regeln:

1. Zuweisungsaxiom: $\{Q[E/x]\}\;x := E\;\{Q\}$

2. Sequenzregel: $\{P\}\,c_1\,\{R\} \wedge \{R\}\,c_2\,\{Q\} \implies \{P\}\,c_1; c_2\,\{Q\}$

3. While-Regel: $\{I \wedge b\}\,c\,\{I\} \implies \{I\}\,\text{while } b \text{ do } c\,\{I \wedge \neg b\}$

4. Konsequenzregel: $(P \implies P') \wedge \{P'\}\,c\,\{Q'\} \wedge (Q' \implies Q) \implies \{P\}\,c\,\{Q\}$

Auswertung von $\langle c, \sigma \rangle \Downarrow \sigma'$ nach formalen Inferenzregeln

Initialer Zustand $\sigma_0$:

x = 3 y = 2 z = 0

Ausgewähltes Programm:

z := x + y; x := z * 2

Aktueller Inferenzschritt:

Klicken Sie auf „Schritt weiter“, um die formale Inferenzregel anzuwenden.

Formale Ableitung (Proof Tree):

Zustandsraum-Exploration und Modellprüfung formaler Sicherheitseigenschaften

Kripke-Struktur $\mathcal{M} = (S, S_0, R, L)$ 4 Zustände

Formel-Prüfung (Model Checker) Gültig in M

Wähle temporallogische Spezifikation $\Phi$:

✓ $\mathcal{M}, s_0 \models \Phi$ (Erfüllt)

In allen vom Startzustand erreichbaren Pfaden gilt die Safety-Eigenschaft.

Widerlegungsbeweise in KNF (Konjunktive Normalform) und Klauselmengen

Klauselmenge $S$ (KNF):

Format: {A, !B} für $A \vee \neg B$. Ein Literal pro Zeile.

Resolutions-Ableitungsschritte:

Originalgetreue TU Darmstadt Übungs- und Klausurfragen mit ausführlichen Musterlösungen

0 / 5 Punkte

Frage 1 von 5 MoSeS • Formale Methoden