Verifikation digitaler Systeme - Exam

Aufgabe 1)

Du hast ein digitales System, das häufig in Verkehrsleitsystemen verwendet wird. Das System hat bestimmte Zustände und Übergänge, die durch Eingaben gesteuert werden. Deine Aufgabe ist es, dieses System mittels formaler Methoden zu spezifizieren und zu überprüfen.

• Du sollst mathematische Modelle wie Automaten und Zustandsräume verwenden, um das System zu modellieren.
• Du wirst eine Spezifikationssprache wie Z verwenden, um die Eigenschaften und das Verhalten des Systems zu beschreiben.
• Überprüfe die Spezifikationen auf Konsistenz und Vollständigkeit.

a)

Definiere einen endlichen Automaten für das Verkehrsleitsystem, wobei die Zustände und Übergänge des Systems beschrieben werden. Skizziere den Zustandsraum des Systems und beschreibe die Übergänge zwischen den Zuständen.

Lösung:

Um einen endlichen Automaten für das Verkehrsleitsystem zu definieren, müssen wir die Zustände und Übergänge des Systems klar spezifizieren. Ein endlicher Automat besteht aus folgenden Komponenten:

• Eine endliche Menge von Zuständen (\textbf{Q})
• Ein Alphabet von Eingabesymbolen (\textbf{Σ})
• Eine Übergangsfunktion (\textbf{δ}), die Zustandsübergänge basierend auf den Eingabesymbolen definiert
• Einen Startzustand (\textbf{q₀})
• Eine Menge von Endzuständen (\textbf{F})

Zustände und Übergänge

Angenommen, unser Verkehrsleitsystem hat die folgenden Zustände und Übergänge:

• Zustände (\textbf{Q}): Q = {R, G, Y}
  • R: Rotlicht
  • G: Grünlicht
  • Y: Gelblicht
• Eingabesymbole (\textbf{Σ}): Σ = {timer}
• Übergangsfunktion (\textbf{δ}):
  • δ(R, timer) = G
  • δ(G, timer) = Y
  • δ(Y, timer) = R
• Startzustand (\textbf{q₀}): q₀ = R
• Endzustände (\textbf{F}): F = {}

Skizzierung des Zustandsraums

Der Zustandsraum unseres Verkehrsleitsystems kann wie folgt skizziert werden:

               +---(timer)-->  G               |               |               R <---(timer)---+ Y               |               |               +---(timer)-->  Y

Übergänge beschreiben

• Vom Zustand R (Rotlicht) wechselt das System mit der Eingabe timer zu Zustand G (Grünlicht).
• Vom Zustand G (Grünlicht) wechselt das System mit der Eingabe timer zu Zustand Y (Gelblicht).
• Vom Zustand Y (Gelblicht) wechselt das System mit der Eingabe timer zu Zustand R (Rotlicht).

Damit haben wir den endlichen Automaten für das Verkehrsleitsystem definiert sowie den Zustandsraum skizziert und die Übergänge beschrieben.

b)

Verwende die Spezifikationssprache Z, um die wichtigsten Attribute, Zustände und Übergänge des Verkehrsleitsystems formal zu spezifizieren. Achte darauf, Invarianten und Prädikate einzufügen, um das System korrekt zu beschreiben.

Lösung:

Um die wichtigsten Attribute, Zustände und Übergänge des Verkehrsleitsystems formal mit der Spezifikationssprache Z zu spezifizieren, definieren wir zunächst die grundlegenden Komponenten des Systems. In Z werden diese als Schemata dargestellt.

Definition der Grundkomponenten

Alphabet und Zustände

TRAFFIC_LIGHT_SYSTEM alphabet == { timer }[STATUS] == { red, green, yellow }

Schema für das Verkehrsleitsystem

Das Hauptschema wird die Attribute, den aktuellen Zustand und die Invarianten des Systems beschreiben.

TrafficLightSystem[ currState : STATUS]

Initialzustand

Init[ TrafficLightSystem ] currState = red

Definition der Übergänge

Nun definieren wir die Übergänge des Verkehrsleitsystems. Jeder Übergang wird als separates Schema spezifiziert.

ChangeToGreen[ ΔTrafficLightSystem currState = red 
<= green>
]

ChangeToYellow[ ΔTrafficLightSystem currState = green 
<= yellow>
]

ChangeToRed[ ΔTrafficLightSystem currState = yellow 
<= red>
]

Invarianten und Prädikate

Um das System korrekt zu beschreiben, fügen wir Invarianten und Prädikate hinzu.

Invariant: Das System muss immer in einem der drei Zustände sein

TrafficLightSystem[ currState : STATUS 
currState ∈ { red, green, yellow }
]

Zusammenführung der Spezifikation

Unsere vollständige formale Spezifikation des Verkehrsleitsystems in Z sieht nun wie folgt aus:

TRAFFIC_LIGHT_SYSTEM alphabet == { timer }[STATUS] == { red, green, yellow }

TrafficLightSystem[ currState : STATUS
currState ∈ { red, green, yellow }
]

Init[ TrafficLightSystem ] currState = red

ChangeToGreen[ ΔTrafficLightSystem currState = red 
<= green>
]

ChangeToYellow
ChangeToYellow[ ΔTrafficLightSystem currState = green 
<= yellow>
]
ChangeToRed[ ΔTrafficLightSystem currState = yellow 
<= red>
]
Damit haben wir das Verkehrsleitsystem mit der Spezifikationssprache Z formal spezifiziert, inklusive der Attribute, Zustände, Übergänge und Invarianten.
c)
 
Formuliere eine Konsistenzprüfung für die Zustandsübergänge in deiner Spezifikation. Zeige mathematisch, dass die Übergänge konsistent sind, indem du die Erhaltung der Invariante überprüfst.
 
 Lösung: 
Um die Konsistenzprüfung für die Zustandsübergänge im Verkehrsleitsystem durchzuführen, müssen wir sicherstellen, dass alle definierten Übergänge die Invariante des Systems beibehalten. Die Invariante in unserer Spezifikation ist, dass der Zustand immer einer der definierten Zustände {red, green, yellow} sein muss.
Invariante:
TrafficLightSystem[ currState: STATUS currState ∈ {red, green, yellow}]
Die Invariante muss vor und nach jedem Übergang erfüllt sein.
Überprüfung der Zustandsübergänge
Überprüfung des Übergangs ChangeToGreen:
ChangeToGreen[ ΔTrafficLightSystem currState = red currState' = green]
Startzustand: \(currState = \text{red}\)Nach dem Übergang: \(currState' = \text{green}\)Da \(currState' \in \{\text{red}, \text{green}, \text{yellow}\}\) bleibt die Invariante erhalten.
Überprüfung des Übergangs ChangeToYellow:
ChangeToYellow[ ΔTrafficLightSystem currState = green currState' = yellow]
Startzustand: \(currState = \text{green}\)Nach dem Übergang: \(currState' = \text{yellow}\)Da \(currState' \in \{\text{red}, \text{green}, \text{yellow}\}\) bleibt die Invariante erhalten.
Überprüfung des Übergangs ChangeToRed:
ChangeToRed[ ΔTrafficLightSystem currState = yellow currState' = red]
Startzustand: \(currState = \text{yellow}\)Nach dem Übergang: \(currState' = \text{red}\)Da \(currState' \in \{\text{red}, \text{green}, \text{yellow}\}\) bleibt die Invariante erhalten.
Mathematische Konsistenzprüfung
Die Konsistenz der Zustandsübergänge kann mathematisch nachgewiesen werden, indem gezeigt wird, dass die Invariante in jeder möglichen Übergangssituation beibehalten wird. Formal formuliert:
∀ s: STATUS • ChangeToGreen(s) ∧ (s ∈ STATUS) ⟹ s' ∈ STATUS∀ s: STATUS • ChangeToYellow(s) ∧ (s ∈ STATUS) ⟹ s' ∈ STATUS∀ s: STATUS • ChangeToRed(s) ∧ (s ∈ STATUS) ⟹ s' ∈ STATUS
ChangeToGreen: Wenn \(currState = \text{red}\) ist, dann ist \(currState' = \text{green}\). Angenommen ein gültiger Startzustand \(currState ∈ \{ \text{red}, \text{green}, \text{yellow} \}\), dann \(currState' \in \{ \text{red}, \text{green}, \text{yellow} \}.\)
ChangeToYellow: Wenn \(currState = \text{green}\) ist, dann ist \(currState' = \text{yellow}\). Angenommen ein gültiger Startzustand \(currState ∈ \{ \text{red}, \text{green}, \text{yellow} \}\), dann \(currState' \in \{ \text{red}, \text{green}, \text{yellow} \}.\)
ChangeToRed: Wenn \(currState = \text{yellow}\) ist, dann ist \(currState' = \text{red}\). Angenommen ein gültiger Startzustand \(currState ∈ \{ \text{red}, \text{green}, \text{yellow} \}\), dann \(currState' \in \{ \text{red}, \text{green}, \text{yellow} \}.\)
Da alle möglichen Übergänge die Invariante erfüllen, bleibt das System konsistent.
d)
 
Führe eine Vollständigkeitsprüfung der Spezifikation durch. Erkläre, wie du sicherstellst, dass alle möglichen Zustände und Übergänge des Systems erfasst wurden und keine unberücksichtigten Fälle vorhanden sind.
 
 Lösung: 
Um eine Vollständigkeitsprüfung der Spezifikation des Verkehrsleitsystems durchzuführen, müssen wir sicherstellen, dass alle möglichen Zustände und Übergänge des Systems erfasst wurden und keine unberücksichtigten Fälle vorhanden sind. Hierzu gehen wir schrittweise vor:
1. Überprüfung der möglichen Zustände
Gemäß der Spezifikation existieren die folgenden Zustände:
Red (R)
Green (G)
Yellow (Y)
Diese Zustände decken alle möglichen Signallichter eines typischen Verkehrsleitsystems ab.
2. Überprüfung der möglichen Übergänge
Damit ein Verkehrsleitsystem vollständig erfasst ist, müssen alle möglichen Übergänge zwischen den Zuständen definiert sein:
ChangeToGreen: \(R \rightarrow G\)
ChangeToYellow: \(G \rightarrow Y\)
ChangeToRed: \(Y \rightarrow R\)
Jeder Zustand muss durch eine Eingabe (den Timer) zu einem anderen Zustand übergehen können. Diese Übergänge sind in der Spezifikation enthalten:
ChangeToGreen[ ΔTrafficLightSystem currState = red currState' = green]
ChangeToYellow[ ΔTrafficLightSystem currState = green currState' = yellow]
ChangeToRed[ ΔTrafficLightSystem currState = yellow currState' = red]
3. Überprüfung der Vollständigkeit durch Invarianz
Die Invariante garantiert, dass das System stets in einem gültigen Zustand bleibt:
TrafficLightSystem[ currState : STATUS currState ∈ {red, green, yellow}]
Da alle Übergänge und Zustände die Invariante erfüllen, wird sichergestellt, dass das System keine unberücksichtigten Zustände oder Übergänge enthält.
4. Vollständigkeit durch Endlichkeit und Zyklizität
Das System ist endlich und zyklisch, da:
Es gibt eine endliche Anzahl von Zuständen (red, green, yellow).
Die Übergänge bilden einen Zyklus: \(R \rightarrow G, G \rightarrow Y, Y \rightarrow R\).
Kein Übergang führt zu einem unbestimmten Zustand, und jeder Zustand hat einen definierten Nachfolger.
Fazit:
Die Spezifikation ist vollständig, da:
Alle möglichen Zustände des Systems spezifiziert sind.
Alle möglichen Übergänge zwischen den Zuständen beschrieben sind.
Die Invariante sicherstellt, dass das System immer in einem gültigen Zustand bleibt.
Das System endlich und zyklisch ist, ohne unberücksichtigte Fälle.
Durch diese Vorgehensweise wird sichergestellt, dass alle Zustände und Übergänge des Verkehrsleitsystems vollständig erfasst und spezifiziert sind.
Aufgabe 2)
 Im Rahmen des „Model Checkings“ werden Algorithmen genutzt, um Zustände eines Systems systematisch zu durchlaufen und zu überprüfen, ob bestimmte spezifizierte Eigenschaften erfüllt sind. Dabei wird oft mit Problemen der Zustandsexplosion konfrontiert, da die Größe des Zustandsraumes exponentiell mit der Anzahl der Variablen wächst. Es gibt verschiedene technische Ansätze, um diesem Problem zu begegnen: Breadth-First Search (BFS), Depth-First Search (DFS) sowie symbolisches Model Checking mithilfe von Binary Decision Diagrams (BDDs). Außerdem wird temporale Logik (LTL, CTL) verwendet, um die zu überprüfenden Eigenschaften zu spezifizieren. 
a)
 Erkläre den Unterschied zwischen Breadth-First Search (BFS) und Depth-First Search (DFS) in Bezug auf die Zustandsraumerkundung bei Model-Checking-Algorithmen. Diskutiere außerdem, unter welchen Bedingungen einer dieser Algorithmen vorteilhafter sein könnte. 
 Lösung: 
Unterschied zwischen Breadth-First Search (BFS) und Depth-First Search (DFS):
 
 
Breadth-First Search (BFS): BFS durchläuft den Zustandsraum Schicht für Schicht. Das bedeutet, dass es zuerst alle Nachbarn eines Ausgangszustands untersucht, bevor es zu den Nachbarn dieser Nachbarn übergeht. Dies geschieht, bis alle Zustände besucht sind oder bis ein Zustand gefunden wird, welcher die zu überprüfende Eigenschaft erfüllt.
 
Vorteile von BFS: - Garantiert den kürzesten Pfad zu einem Zustand, der eine Eigenschaft erfüllt. - Gut geeignet, wenn herausgefunden werden soll, ob ein Zustand erreichbar ist.
 Nachteile von BFS: - Erfordert mehr Speicher, da alle Zustände einer Ebene gleichzeitig im Speicher gehalten werden müssen.
 
 
 
Depth-First Search (DFS): DFS verfolgt jeden Pfad im Zustandsraum bis zu seinem Ende, bevor es zum nächsten Pfad übergeht. Es geht so tief wie möglich, bevor es zurückspringt und alternative Pfade untersucht.
 
Vorteile von DFS: - Benötigt weniger Speicher, da nur die aktuellen Pfade und ihre Zustände gespeichert werden müssen. - Kann effizienter sein, wenn nur ein kleiner Teil des Zustandsraumes relevant ist.
 Nachteile von DFS: - Es gibt keine Garantie, den kürzesten Pfad zu einem Zustand zu finden, der eine Eigenschaft erfüllt. - Kann in endlosen Pfaden oder großen Suchbäumen stecken bleiben, ohne eine Lösung zu finden.
 
 
 
 
Unter welchen Bedingungen ist einer dieser Algorithmen vorteilhafter:
 
 
Breadth-First Search (BFS): BFS ist vorteilhafter, wenn: - Eine kurze Lösung oder der kürzeste Pfad zu einem Zielzustand priorisiert wird. - Der Zustandsraum relativ tief ist, aber die Lösungszustände auf einer flacheren Ebene liegen.
 
Depth-First Search (DFS): DFS ist vorteilhafter, wenn: - Es wenige Speicherressourcen gibt und der Zustandsraum sehr groß ist. - Der Zustandsraum eher tief als breit ist und Lösungen in tieferen Ebenen erwartet werden. - Die Suche in großen und verhältnismäßig wenigen Pfaden nötig ist, um eine mögliche Lösung zu finden (weniger Verzweigungen).
 
b)
 Angenommen, ein System besitzt 10 binäre Variablen. Berechne die gesamte Anzahl der möglichen Zustände des Systems. Erkläre anschließend, wie symbolisches Model Checking und die Nutzung von BDDs helfen können, die Herausforderungen der Zustandsexplosion zu bewältigen. 
 Lösung: 
Berechnung der Anzahl der möglichen Zustände:
 
 
Ein System mit 10 binären Variablen hat jede Variable, die zwei Zustände annehmen kann (0 oder 1).
 
Da jede der 10 Variablen 2 Zustände annehmen kann, ergibt sich die Gesamtzahl der möglichen Zustände durch die folgende Berechnung:
 
 
2^{10} = 1024
 
 
Das System hat also 1024 mögliche Zustände. Dies verdeutlicht, wie schnell die Anzahl der Zustände mit der Anzahl der Variablen exponentiell wächst.
 
 
Bewältigung der Herausforderungen der Zustandsexplosion mit symbolischem Model Checking und der Nutzung von BDDs:
 
 
Symbolisches Model Checking: 
 
Symbolisches Model Checking verwendet mathematische Formeln und logische Ausdrücke zur Darstellung und Analyse von Zustandsmengen, anstatt jede möglichen Zustand einzeln explizit durchzuarbeiten.
 
Diese Methode ermöglicht eine effizientere und skalierbarere Überprüfung großer Zustandsräume, da Zustandsgruppen zusammengefasst und als Ganzes behandelt werden können. Dies reduziert die Anzahl der benötigten Zustände und damit auch den Speicherverbrauch und die erforderliche Rechenleistung.
 
 
 
Binary Decision Diagrams (BDDs): 
 
BDDs sind eine Datenstruktur zur kompakten und kanonischen Darstellung boolescher Funktionen. Sie minimieren Redundanzen, indem sie äquivalente Teilstrukturen gemeinsam nutzen.
 
BDDs erlauben umfangreiche Zustandsräume effizient zu handhaben, da sie grundlegende logische Operationen schnell und platzsparend durchführen. Dadurch wird der Speicherbedarf drastisch reduziert im Vergleich zur expliziten Aufzählung aller möglichen Zustände.
 
BDDs sind besonders nützlich, um große Mengen von Zuständen zu komprimieren und die Zusammenhänge zwischen Variablen zu optimieren.
 
 
 
 
Beispiel:
 
 
Angenommen, wir wollen überprüfen, ob eine bestimmte Bedingung in einem Subset der 1024 möglichen Zustände erfüllt wird. Durch die Nutzung von BDDs können diese Zustände effizient gruppiert und redundante Zustände entfernt werden, wodurch der Überprüfungsprozess erheblich beschleunigt und vereinfacht wird.
 
 
Zusammenfassend lässt sich sagen, dass sowohl symbolisches Model Checking als auch BDDs entscheidende Werkzeuge sind, um die Herausforderungen der Zustandsexplosion zu bewältigen. Sie bieten speichereffiziente und skalierbare Methoden zur Analyse großer Zustandsräume und erlauben eine effektive und praktikable Überprüfung selbst sehr großer Systeme.
c)
 Beschreibe, was unter temporaler Logik (LTL, CTL) verstanden wird und wie sie im Model Checking eingesetzt wird. Gehe dabei auf die Unterschiede zwischen LTL und CTL ein und gib ein Beispiel für eine formale Spezifikation einer temporalen Logikeigenschaft. 
 Lösung: 
Temporale Logik (LTL, CTL) im Model Checking:
 
Temporale Logik wird im Model Checking verwendet, um Aussagen über die zeitlichen Abfolgen von Zuständen in einem System zu machen. Sie ermöglicht es, Eigenschaften eines Systems zu spezifizieren und diese im zeitlichen Verlauf zu überprüfen.
 
 
Lineare Temporale Logik (LTL): 
 
LTL betrachtet lineare Sequenzen von Zuständen, wobei Zustände in einer linearen Abfolge gesehen werden.
 
Es gibt spezielle temporale Operatoren in LTL, die helfen, zeitliche Eigenschaften zu beschreiben: 
 
\(X\) (Next): \(X\ p\) bedeutet, dass \(p\) im nächsten Zustand wahr ist.
 
\(G\) (Globally): \(G\ p\) bedeutet, dass \(p\) in allen zukünftigen Zuständen wahr ist.
 
\(F\) (Finally): \(F\ p\) bedeutet, dass \(p\) irgendwann in der Zukunft wahr sein wird.
 
\(U\) (Until): \(p\ U\ q\) bedeutet, dass \(p\) so lange wahr ist, bis \(q\) wahr wird.
 
 
 
 
 
Computation Tree Logic (CTL): 
 
CTL umfasst sowohl lineare als auch verzweigende Zeitpfade und ermöglicht es, Aussagen über verschiedene mögliche Zukunftspfade eines Systems zu treffen.
 
CTL kombiniert Pfadquantoren mit temporalen Operatoren: 
 
\(A\) (for All paths): \(A\ p\) bedeutet, dass \(p\) in allen Zukunftspfaden wahr ist.
 
\(E\) (there Exists a path): \(E\ p\) bedeutet, dass \(p\) in mindestens einem Zukunftspfad wahr ist.
 
Beispiele für CTL-Operatoren sind \(AX\ p\) (in allen Pfaden ist \(p\) im nächsten Zustand wahr) und \(EF\ p\) (es gibt mindestens einen Pfad, in dem \(p\) irgendwann in der Zukunft wahr wird).
 
 
 
 
 
 
Unterschiede zwischen LTL und CTL:
 
 
LTL betrachtet nur lineare Sequenzen (Pfade) von Zuständen.
 
CTL betrachtet verzweigende Pfade und ermöglicht es, Aussagen über alle möglichen Zukunftspfade zu treffen.
 
 
Beispiel für eine formale Spezifikation einer temporalen Logikeigenschaft:
 
 
LTL Beispiel: 
 
\(G (request → F acknowledgment)\): Diese Spezifikation bedeutet, dass nach jeder \textit{request} immer irgendwann eine \textit{acknowledgment} folgt, d.h. jede Anfrage wird schließlich bestätigt.
 
 
 
CTL Beispiel: 
 
\(AG (request → EF acknowledgment)\): Diese Spezifikation bedeutet, dass in allen möglichen Zukunftspfaden (AG) aus jedem Zustand, in dem eine \textit{request} gemacht wird, es mindestens einen Pfad (EF) gibt, an dessen Ende eine \textit{acknowledgment} folgt. Das heißt, aus jedem Zustand, in dem eine Anfrage gestellt wird, gibt es garantiert einen möglichen Pfad, in dem die Anfrage bestätigt wird.
 
 
 
 
Temporale Logik wie LTL und CTL ist ein mächtiges Werkzeug im Model Checking, das eine präzise und formale Überprüfung von Eigenschaften komplexer Systeme ermöglicht.
Aufgabe 3)
 Gegeben ist ein endlicher Zustandsraum für ein System S, bestehend aus den Zuständen S = {s0, s1, s2}, sowie den Übergängen zwischen diesen Zuständen definiert durch eine Transition-Relation T. Die Transition-Relation T wird durch folgende Übergänge beschrieben: 
(s0, s1)
(s1, s0)
(s1, s2)
 In diesem System ist s0 der Startzustand und es gibt zwei propositionale Variablen: p und q. Die Belegung der Variablen ist wie folgt: 
In s0 gilt p
In s1 gilt q
In s2 gelten p und q
 Du sollst mit Hilfe von LTL und CTL temporale Ausdrücke für verschiedene Eigenschaften formulieren und überprüfen. 
a)
 Formuliere einen LTL-Ausdruck, der beschreibt, dass die Variable q irgendwann in der Zukunft immer wahr sein wird. Überprüfe, ob diese Eigenschaft für das gegebene System S zutrifft. Tipp: Verwende den \texttt{G} und den \texttt{F} Operator. 
 Lösung: 
LTL-Ausdruck für die gegebene Eigenschaft
Um einen LTL-Ausdruck zu formulieren, der beschreibt, dass die Variable q irgendwann in der Zukunft immer wahr sein wird, verwenden wir den \texttt{G} (globally) und den \texttt{F} (finally) Operator. Diese Operatoren helfen uns, zeitliche Eigenschaften zu beschreiben.
Der gesuchte LTL-Ausdruck lautet:
  G(F(q))  
Das bedeutet, dass global (zu jeder Zeit) in der Zukunft irgendwann q immer wahr sein wird.
Überprüfung der Eigenschaft für das gegebene System S
Jetzt überprüfen wir, ob diese Eigenschaft für das System S zutrifft:
Startzustand s0: In s0 gilt p. Laut der Transition-Relation T kann das System zu s1 übergehen.
Zustand s1: In s1 gilt q. Von hier aus kann das System entweder zurück zu s0 oder zu s2 übergehen.
Zustand s2: In s2 gelten sowohl p als auch q.
Betrachten wir alle möglichen Pfade:
s0 → s1: q wird wahr in s1.
s0 → s1 → s2: q bleibt wahr in s2.
s0 → s1 → s0 → s1...: q wird immer wieder in s1 wahr.
Unabhängig vom Pfad erreichst Du immer einen Zustand, in dem q gilt, und danach bleibt q wahr. Somit erfüllt das System S die angegebene LTL-Eigenschaft G(F(q)).
b)
 Formuliere einen CTL-Ausdruck, der spezifiziert, dass es einen Pfad gibt, auf dem p bis zu einem Zustand gilt, in dem q gilt, gefolgt von einem Zustand, in dem q nicht mehr gilt. Überprüfe, ob diese Eigenschaft für das gegebene System S zutrifft. 
 Lösung: 
CTL-Ausdruck für die gegebene Eigenschaft
Um einen CTL-Ausdruck zu formulieren, der spezifiziert, dass es einen Pfad gibt, auf dem p bis zu einem Zustand gilt, in dem q gilt, gefolgt von einem Zustand, in dem q nicht mehr gilt, verwenden wir die Operatoren \texttt{E} (es gibt einen Pfad), \texttt{U} (bis) und \texttt{X} (nächster Zeitpunkt).
Der gesuchte CTL-Ausdruck lautet:
  E(p U (q & EX(¬q)))  
Das bedeutet:
Es gibt einen Pfad (E)
auf dem p bis (U) zu einem Zustand gilt, in dem q gilt
gefolgt von einem Zustand, in dem q nicht mehr gilt (EX(¬q)).
Überprüfung der Eigenschaft für das gegebene System S
Jetzt überprüfen wir, ob diese Eigenschaft für das System S zutrifft:
Startzustand s0: In s0 gilt p. Vom Zustand s0 gibt es einen Übergang zu s1.
Zustand s1: In s1 gilt q. Von s1 gibt es Übergänge zu s0 und s2.
Zustand s2: In s2 gelten zuguich p und q, es gibt keine weiteren Informationen zu Q.
Betrachten wir nun die möglichen Pfade:
s0 → s1: In s1 gilt q, und es gibt einen Übergang zurück zu s0.
Es gibt jedoch keinen Zustand im Pfad, der direkt dem Zustand s1 folgt, in dem q gilt, wo q auch nicht mehr gilt. Da s0 gilt nicht q.
Somit erfüllt das System S die angegebene CTL-Eigenschaft E(p U (q & EX(¬q))) nicht.
Aufgabe 4)
 
Du bist beauftragt, ein digitales System mittels des Symbolic Model Checkers (SMV) zu verifizieren. Das zu überprüfende System ist eine Finite-State-Maschine (FSM), welche eine einfache Ampelschaltung repräsentiert. Die Ampelschaltung hat die folgenden Zustände:
GRUEN
GELB
ROT
Die Wechselzustände der Schaltung sind folgendermaßen definiert:
Von GRUEN zu GELB
Von GELB zu ROT
Von ROT wieder zu GRUEN
Deine Aufgabe ist es, mit Hilfe von SMV sicherzustellen, dass die Ampelschaltung korrekt funktioniert. Dabei sollen zwei wichtige Eigenschaften geprüft werden: (i) Sicherheit: Es darf niemals gleichzeitig GRUEN und ROT sein. (ii) Liveness: Der Zustand GELB darf nie ein Endzustand sein; es muss immer ein Übergang zu ROT oder GRUEN stattfinden.
 
a)
 
1. Implementiere in SMV die Modellierung der beschriebenen Ampelschaltung als FSM. Stelle sicher, dass die Zustandsübergänge korrekt definiert sind. Dein Modell sollte so aussehen, dass sichergestellt wird, dass die Schaltung von GRUEN zu GELB zu ROT und wieder zu GRUEN wechselt.
 MODULE main VAR state : {GRUEN, GELB, ROT}; ASSIGN init(state) := GRUEN; next(state) := case  state = GRUEN : GELB;  state = GELB : ROT;  state = ROT : GRUEN;  esac;  
 
 Lösung: 
Hier ist die SMV-Implementation für die Modellierung der beschriebenen Ampelschaltung als Finite-State-Maschine (FSM). Dieses Modell stellt sicher, dass die Ampelschaltung korrekt von GRUEN zu GELB zu ROT und wieder zu GRUEN wechselt:
MODULE main VAR    state : {GRUEN, GELB, ROT};ASSIGN    init(state) := GRUEN;    next(state) := case        state = GRUEN : GELB;        state = GELB : ROT;        state = ROT : GRUEN;        esac;
In diesem Modell wird:
VAR verwendet, um die möglichen Zustände der Ampelschaltung zu definieren: GRUEN, GELB und ROT.
ASSIGN, speziell init(state) := GRUEN;, verwendet, um den Anfangszustand der Ampel auf GRUEN zu setzen.
next(state) definiert die Zustandsübergänge: von GRUEN zu GELB, von GELB zu ROT und von ROT zurück zu GRUEN.
b)
 
2. Formuliere und überprüfe die Korrektheit der beiden angegebenen temporalen Logikeigenschaften mit CTL in deinem SMV-Modell. Dokumentiere die SMV-Befehle und erkläre, wie diese Eigenschaften verifiziert werden. 
Eigenschaft (i): Sicherheit: Erstelle eine CTL-Formel, die besagt, dass es niemals der Fall ist, dass sowohl der Zustand GRUEN als auch der Zustand ROT gleichzeitig aktiv sind.
Eigenschaft (ii): Liveness: Erstelle eine CTL-Formel, die sicherstellt, dass jedes Mal, wenn die Schaltung im Zustand GELB ist, dieser Zustand nicht dauerhaft bestehen bleibt, sondern zu ROT oder GRUEN übergeht.
SPEC AG !(state = GRUEN & state = ROT) SPEC AG (state = GELB -> AF (state = ROT | state = GRUEN))  
 
 Lösung: 
Um die temporalen Logikeigenschaften mittels Computational Tree Logic (CTL) in deinem SMV-Modell zu formulieren und zu überprüfen, gibt es zwei wichtige Eigenschaften: Sicherheit und Liveness.
Hier ist die Implementierung der CTL-Formeln und eine Erklärung zu deren Verifizierung:
Eigenschaft (i): Sicherheit: Es darf niemals der Fall sein, dass sowohl der Zustand GRUEN als auch der Zustand ROT gleichzeitig aktiv sind.
Eigenschaft (ii): Liveness: Es muss sichergestellt werden, dass jedes Mal, wenn die Schaltung im Zustand GELB ist, dieser Zustand nicht dauerhaft bestehen bleibt, sondern zu ROT oder GRUEN übergeht.
Die CTL-Formeln für die Verifizierung lauten wie folgt:
-- Eigenschaft (i): SicherheitSPEC AG !(state = GRUEN & state = ROT)  -- Eigenschaft (ii): LivenessSPEC AG (state = GELB -> AF (state = ROT | state = GRUEN))
Erklärungen:
Für Eigenschaft (i) - Sicherheit:
SPEC AG !(state = GRUEN & state = ROT) bedeutet, dass in allen möglichen Zustandssequenzen (AG) es niemals der Fall ist ( ! ), dass der Zustand gleichzeitig GRUEN und ROT ist.
Für Eigenschaft (ii) - Liveness:
SPEC AG (state = GELB -> AF (state = ROT | state = GRUEN)) bedeutet, dass in allen möglichen Zustandssequenzen (AG), wenn der Zustand GELB ist, dann muss sichergestellt werden, dass letztendlich (AF) der Zustand entweder ROT oder GRUEN ist.
Der Verifizierungsprozess mit SMV-Befehlen sieht wie folgt aus:
Speichere das aktualisierte SMV-Modell in einer Datei, zum Beispiel ampel.smv.
Starte den NuSMV-Symbolic Model Checker.
Führe die Verifizierung durch, indem Du den folgenden Befehl eingibst:
NuSMV ampel.smv
Der Symbolic Model Checker wird die Formeln überprüfen und bestätigen, ob die Eigenschaften erfüllt sind.