Woche 03: Anwendung: Formale Verifikation

• Wenn wir eine gemeinsame Ressource nutzen wollen machen wir das oft mit einem System von höflichkeit
• Sowas kann man allerdings nur sehr schlecht formalisieren
• Das ist problematisch, weil dann können wir uns praktisch garnicht sicher sein, ob das was wir machen / das was wir betrachten, tatsächlich das tut was es tun soll
• Wenn wir uns das mal fundamental anschauen, sehen wir, dass eine Ressource automatisch abhängig ist, wenn wir sie teilen
• Genauer gesagt ist ein System Abhängig, indem sich mehrere Prozesse untereinander beeinflussen können
• Das können sachen sein die ein gemeinsames Ziel verfolgen oder auch dinge sein die was komplett unterschiedliches machen
• klassisch können wir das in einem System beobachten indem es Mutual exclusion gibt
  • sprich asynchrone Programme oder ähnliches

Dijkstras Protokoll

• Um damit vernünftig durchzustarten hat unser beliebter Dijkstra schonmal ein Protokoll gemacht
• in diesem Protokoll stellt er einen weg dar, mit dem man sowas vernünftig handlen kann
• Zunächst unterteilen wir unser Programm in einen Kritischen und einen Unkritischen bereich
• Hier ist der unterschied, dass der Kritische bereich die Ressource darstellt, die geteilt ist
  • Also hier können wir probleme bekommen, denn die ressource kann logischerweise nur von einem Thread / einem Prozess gleichzeitig genutzt werden
• Wir schnappen uns also ein "Signal" bzw. einen Indikator, mit dem wir aussagen können, ob eine Ressource derzeit available oder nicht ist
• Wenn also eine ressource auf den kritischen bereich zugreifen will, schauen wir zuerst nach, ob der bereich betretbar ist
• Wenn das geht, setzen wir die ressource auf "unavailable" und gehen dann rein
• Nachdem wir mit dem kram fertig sind, können wir das dann einfach wieder zurückstellen
• So können wir sichergehen, dass nicht zwei ressourcen gleichzeitig versuchen auf die selbe Ressource zuzugreifen
• Und ausserhalb von unserem kritischen bereich, können wir alles einfach so machen wie wir wollen

Einführung ins Model Checking

• Beim model-Checking verwenden wir (wie so häufig) einen Algorithmus um zuzuschauen, dass alles so passiert wie wirs haben wollen

1. Wir modellieren unser Programm in einem Transitionssystem, damit wir den fluss von Daten / Informationen schön und sinnvoll darstellen können
2. Spezifizieren der einzelnen Eigenschaften durch formeln
   • Wir schreiben also eine Formel, für jede auftretende eingenschaft, damit wir uns absolut sicher sein können, dass wir tatsächlich das ausdrücken was wir auch sagen wollen
3. Dann testen wir, ob das Transitionssystem auch unseren Formeln "Standhält"
4. Wenn das nicht der fall sein sollte, konstruieren wir ein Gegenbeispiel

• betrachten können wir das ganze durch typische Logiken
  • $LTL$ Linear temporal logic
  • $CTL$ Computational tree logic
• Das modelchecking und seine respektiven logiken verwenden wir in Programmen, Protokollen und vielem mehr

Wie kommen wir denn jetzt dahin

• Naja, wenn wir uns jetzt den Ablauf oben anschauen, sehen wir, dass wir ja irgendwie unsere Strukturen bauen müssen
• Wir bauen uns also unser Transitionssystem: eine Kripke-Struktur mit verschiedenen Startwelten
• Die startwelten haben einen Pfeil (wie bei den Automaten in Info 3)
• In der "normalen" Literatur haben die Kanten meisstens beschriftungen, das machen wir hier einfach nicht
• Aber wie machen wir denn jetzt aus unserem Theoretischen Entwurf eine Kripestruktur?
  • Wir schauen uns alle möglichen "states" an
  • Diese können wir dann modellieren und mit Transitionen miteinander verbinden
  • Sprich: es kann nur ein Valider State in einen anderen validen State wechseln
  • Damit können wir das "relativ" leicht darstellen und ein wunderschönes Diagramm erstellen

Eigenschaften Spezifizieren

• ja wir haben also jetzt unsere "tolle" Kripestruktur
• Wir überlegen uns jetzt erstmal "sinnvolle" Eigenschaften
• 1. Fangen wir mit Korrektheit an, was sind dinge, die immer gelten müssen?
• 2. "Fairness" wie können wir sicherstellen, dass alle teile unseres Systems gleichmäßig gut die geteilte ressource nutzen könnnen?

Abwicklung

• Aus jeder Welt unserer Kripestruktur können wir eine Abwicklung konstruiheren
• Diese ist analog mit unseren Transitionssystemen
• eine Abwicklung ist am ende nichts weiter, als der "Weg" ausgehend von einer Kripestruktur

CTL

• Wenn wir uns CTL anschauen, sehen wir, dass es sehr sinnvolle Operatoren gibt
• 
• 
• 
• 
• 
• 
• 
• 
• 

Syntax und Semantik

• Wenn wir Formeln wie $\phi$ oder $\psi$ haben können wir auch
  • $\neg \phi ,\phi \wedge \psi$ und $\phi \vee \psi$
  • $EX\phi ,EF\phi ,EG\phi$ und $E(\phi U\psi )$
  • $AX\phi ,AF\phi ,AG\phi$ und $A(\phi U\psi )$ haben
• Kurz gesagt, können wir die beliebig aneinanderhängen und stacken
• Die vorhergehenden Ausdrücke "begrenzen" sozusagen die folgenden
• Denn am ende bezieht sich das alles auf einen Weg

Auswertung

• Zur auswertung haben wir ja meisstens noch ein Transitionssystem zur hand
• Hiermit können wir dann unsere Formeln auswerten, und schauen was passiert und aufschreiben wofür was genau gilt

Konstruktion

Verifikation

• Zu "guter" letzt wollen wir den kram ja auch noch irgendwie verifizieren, also schauen, dass das wirklich sinn macht, was wir da gebastelt haben
• So nutzen wir den kram den wir uns ausgesucht haben dann auch wirklich
• Wir werfen noch einen Blick auf das tolle diagramm von vorher
• 

Beispiel: