B3: Anwendung Formale Verifikation

• watn das?
• Wir versuchen ein (komplexes) stück hardware und oder software zu "beweisen"
• Also nicht schauen, dass es da ist, sondern beweisen, dass es das tut, wozu wir es definiert haben
• Idealerweise macht man das eben nicht von hand, sondern eben mit einem Compuper
• Wir wollen letztendlich dann alles irgendwie formell definieren und eben auch verifizieren
• Wir schauen uns zunächst ein "tolles" szenario an
• Das können wir am besten mit diesem bild veranschaulichen:
• 
• Wenn wir uns das anschauen, sehen wir, dass wir (hallup time) ein abhängiges System haben, indem sich mehrere Prozesse gegenseitig beeinflussen
  • Diese zwei prozesse können am ende alles sein, ob jetzt programme, Autos o.ä.
  • Die können auch nen gemeinsames Ziel verfolgen oder auch eben nicht
• Das beste beispiel dabei sind praktisch "Beispiele"
  • Denn jedes beispiel ist ein System dessen Prozesse ein "gemeinsames" Ziel erreichen (nämlich das zeigen, wozu wir ein beispiel machen)
  • Denn unterm strich greifen sie auf gemeinsame ressourcen zu
• Ein problem was wir dabei erkennen ist, dass vieles nur eine sache gleichzeitig machen kann
  • Dementsprechend kann dann immer nur ein Prozess drauf zugreifen
  • Das nennen wir dann "Mutual Exclusion" auch bekannt als der legendäre Mutex
• Wir schauen uns jetzt ein Szenario an:
  • Von zwei Prozessen kann maximal ein Prozess auf eine Gemeinsame Ressource zugreifen
  • Es gibt einen Kritischen und einen Unkritischen bereich.
  • Der geteilte bereich, ist dann eben der "kritische" bereich, weil dieser "weitergegeben" werden muss
  • Wir wollen also garantieren, dass nicht beide Prozesse gleichzeitig in eben diesem Kritischen bereich sind
• Das lösen wir am besten eben mit Semaphoren-
  • Wat dat?
    • Ein Semaphor "bewacht" eine gemeinsame Ressource, und entscheidet bzw. Signalisiert, ob diese gerade nutzbar ist
    • Ein Prozess kann sich eine Ressource vom Semaphor "reservieren" lassen, und solange diese Ressource reserviert ist, kann kein anderer Prozess auf eben diese Ressource zugreifen
    • Der Semaphor behält hier den überblick
  • Die, und all ihre operationen, sollen Atomar ausführen
  • Sprich: Das muss für alle immer gleich aussehen, und alles muss in einer festen reihenfolge passieren.
  • In der realen welt stelt das Betriebssysten eben das sicher
    • Wie geht das? Man lernt das in Betriebssysteme an
• Wir schauen uns eben das in "Dijkstras Protokoll" an.
  • Initial ist unser Prozess (den wir uns anschauen) im Unkritischen bereich
  • Der Prozess entscheidet jetzt, dass er die geteilte ressource braucht
  • Jetzt schaut er, ob sie frei ist, und wartet wenn sie nicht frei ist
  • Wenn die ressource dann frei ist, signalisiert der Prozess dem Semaphor, dass er die Ressource nutzen will und dieser Reserviert diese dann für unseren prozess
  • Dann ist der Prozess im sog. Kritischen Bereich, und hat alleinigen zugriff auf die ressource
  • wenn der Prozess dann fertig mit der Ressource ist, gibt der semaphor die ressource wieder frei, und der Prozess ist wieder im unkritischen bereich
  • Genauer gesagt, kann es auch passieren, dass ein OS wärend die Prozesse laufen sie zwangsweise abwechseln lässt, aber das ist hier gerade nicht weiter relevant
• Wir können so auch sehen, dass Dijkstras Protokoll nicht fair ist, dementsprechend schauen wir uns noch zwei andere Protokolle an:
• 
• 

Einführung ins Model Checking

• Wir können letztendlich alles verifizieren
• Das machen wir aber alles mit einem bestimmten schema, das ist dann eben das hier:
• 
• Wir wollen uns jetzt Transitionssysteme anschauen, sprich wie man von einem Protokoll zur Logik kommt

Vom Protokoll zum Transitionssystem

• Naja, das transitionssystem ist eine Kripke-Strkruktur mit Startwelten
• Das erste was wir also machen müssen, ist uns zu überlegen wie man von unserm Protokoll zum Transitionssystem kommen
  • Das Protokoll ist eben unser sachverhalt, sprich ein Schaltkreis, Programm o.ä. Irgendwas, was definiert werden kann
• Wir schauen uns erstmal an was für zustände es gibt.
  • Nen zustand ist z.b. was für gegebenheiten gerade innerhalb des Progreamms herrschen
• Wenn wir alle zustände haben, bauen wir eben ein Transittionssystem
  • Wir überlegen uns also, wie man von einem Zustand in den nächsten wechseln kann
  • Das machen wir dann eben mit "tollen" Pfeilen
  • Das sieht dann am ende so aus: (irgendwie ein bisschen wie ein Pentagramm)
• 
• Jetzt können wir auf "einen blick" sehen, was wie erreichbar ist

Spezifikation von Eigenschaften

• Wir schauen uns jetzt eine Spezifikationssprache an
• Die sprache heisst CTL
• Die protokolle die wir uns anschauen müssen ja eine gewisse anzahl an "vorraussetzungen" erfüllen
• Eine davon ist auf jeden fall die Korrektheit, denn das ding muss ja auch funktionieren.
  • ${\varphi }_1=AG(\neg c_1\vee \neg c_2)$
  • Das liest man dann so:
    • $A$ = Für alle Berechnungpfade
    • $G$ = Global, also überall in unserer welt
• Eine zweite Eigenschaft ist Fairness
  • Das bedeutet, dass jeder Prozess gleich behandelt wird, also jeder zugreifen darf (wenn wir das beispiel von oben weiter nutzen)
  • $AG({\omega }_1\to AF{c}_1)$
    • Das liest man:
      • Für alle möglichen berechnungspfade muss gelten, dass wenn jemand wartet
      • irgendwann $c_1$ gelten muss
• Das alles sind +CTL* Formeln, das steht für "Computation Tree Logic"
• Die dinger können wir auch als "Berechnungsbaum" anschauen, und so werten wir das dann am ende aus
  • Das ist gleich, wie die abwicklung einer Startwelt, also wie wir durch diese welt (und ihre folgewelten) laufen können
• Die welten verhalten sich nach dem oben definierten schema, und dann können wir eben durch diese welt mithilfe des Berechnungsbaum laufen

Zutaten von CTL

• CTL hat gewisse Operatoren
  • $EX,EF,EG,EU$
  • $AX,AF,AG,AU$
• dabei stehen die buchstaben (logischerweise) für tolle dinge
  • $E$: "Es gibt einen Pfad..."
  • $A$: "Für alle Pfade..."
• Der Zeweite Teil beschreibt dann den quantifizierten Pfad:
  • $X\varphi$: In der nächsten Welt gilt $\varphi$
  • $F\varphi$: In einer zukünftigen Welt gilt $\varphi$
  • $G\varphi$: In allen zukünftigen Welten gilt $\varphi$
  • $\delta U\varphi$: $\delta$ gilt bis $\varphi$ gilt
• Insgesamt ist CTL eine Verallgemeinerung der Modallogik
  • $EX$ entspricht $◊$
  • $AX$ entspricht $\square$
• Es gibt in CLT immer einen "Roten Faden", also was immer gilt usw.
• 
• 
• 
• 
• 
• 
• 
• 

Syntax und Semantik von CTL

Auswertung von CTL-Formeln

Verifikation von Eigenschaften

• Wir erinnern uns nochmal an das schema:
• 
• 
• 
• Letztendlich ist die Große frage die wir uns stellen und die wir entscheiden wollen ist eben, ob die Aussage bzw. das vorliegende Protokoll Stimmt und unseren Vorraussetzungen entpsicht