Verifikation digitaler Systeme - Braindump
| Semester | Prüfer |
|---|---|
| Sommersemester 2023 | Oliver Keszöcze |
Einleitende Fragen
Warum ist Verifikation wichtig?
Je früher Fehler gefunden werden, desto billiger.
Ein Beispiel dafür?
Ich nenne den Divisionsfehler bei Intel Pentium Prozessoren.
Die Vorlesung ist grob in zwei Teilbereiche gegliedert. Welche?
Formale Verifikation und Simulationsbasierte Ansätze.
Welche Vor- und Nachteile gibt es jeweils
- Formale Verifikation garantiert Fehlerfreiheit
- aber nur, wenn Abstraktionen richtig
- Simulation kann Fehler schnell finden
- Simulation garantiert (fast) nie Fehlerfreiheit
Formale Verifikation
Formale Verifikation teilt sich ebenso in zwei Teilbereiche. Welche?
Äquivalenzprüfung und Eigenschaftsprüfung (hier brauche ich einiges an Hilfe des Dozenten)
Was ist Äquivalenzprüfung?
Vergleich, ob sich zwei Systeme gleich verhalten.
TEDs sind ein Mittel zur Äquivalenzprüfung. Wie funktionieren sie?
Basieren auf der Taylorentwicklung von arithmetischen Funktionen um einen Basispunkt.
Ich erkläre die grundlegende Struktur usw.
Warum sollte man TEDs verwenden?
Hier schwimme ich ein wenig, überlege laut, dass TEDs eindeutige Normalformen haben und damit die Äquivalenzprüfung zur Gleichheit reduziert.
Wie wird die Normalform eines TEDs berechnet?
Irgendwas mit Kantengewichten die paarweise prim sind, stellt den Prüfer nicht gerade zufrieden.
Wie funktioniert Automatenäquivalenz?
Ich erkläre die normale Definition von Automatenäquivalenz, reduziere auf Zustandsäquivalenz der Startzustände und zu Produktautomaten.
Wie ist ein Produktautomat definiert?
- Zustandsmenge als kartesisches Produkt der Zustandsmengen der einzelnen Automaten
- Eingabealphabet wird übernommen
- Ausgabealphabet \(\mathbb{B}\)
- Ausgabefunktion
true, wenn Automaten gleiche Ausgabe erzeugen, sonstfalse
Wie viele Zustände hat der Produktautomat?
Für Automaten \(N,M\) mit \(n,m\) Zuständen \(n \cdot m\)
Sind alle davon sinnvoll?
Nicht alle müssen vom Startzustand erreichbar sein.
Wie kann man die Äquivalenzprüfung im Produktautomat berechnen?
Forward traversal oder Backward traversal, ich erkläre kurz Forward traversal.
Wie nennt man den grundlegenden Algorithmus beider Verfahren?
Breitensuche.
Wie noch?
BDDs.
Was sind BDDs
Repräsentation boolescher Funktionen.
Sind BDDs eindeutig?
ja?
Verhadere mich ein bisschen indem ich den Zerlegungstypen als Merkmal definiere, was aber bei BDDs noch keine Rolle spielt.
Welche Zerlegungsarten gibt es?
- Shannon
- {positive, negative} Davio
Zeichnen Sie den BDD für die boolesche Funktion \(f(a,b,c) = a \land b \lor c\)
siehe damaliges Whiteboard.
Warum ist die Variablereihenfolge wichtig?
Variablenreihenfolge hat Einfluss auf die Größe des BDDs.
Das Finden der optimalen Reihenfolge ist aber in NP.
Was ist Eigenschaftsprüfung?
Prüfen, ob das System sich gemäß definierter Eigenschaften verhält.
Was geht hier, aber nicht in Äquivalenzprüfung?
Wie können Eigenschaften beschrieben werden?
Mit Temporaler Aussagenlogik
Temporale Aussagenlogik
Was ist eine Temporale Struktur
Menge von Zeitpunkten mit linkstotaler Übergangsrelation.
LTL vs CTL
LTL modelliert Zeit linear, CTL mit Verzweigungen.
Was repräsentiert eine Verzweigung in einer temporalen Struktur?
Eine Entscheidung wurde getroffen.
Nennen Sie ein Beispiel, bei dem eine lineare temporale Struktur sinnvoll ist
Ampelschaltung (ohne Fußgängerknopf!)
Wie kann die Eigenschaft, dass wenn bei einer Fußgängerampel gedrückt wird, auch irgendwann grün wird, ausgedrückt werden?
\(\mathrm{AG}(\mathit{knopf} \implies \mathrm{AF} \mathit{gruen})\)
Erklären Sie die Formel
Ich erkläre die Pfad- und Zustandsquantoren.
Welche Basisoperatoren?
Ich nenne \(\mathrm{EF}, \mathrm{EG}, \mathrm{EU}\), richtig wäre \(\mathrm{EX}, \mathrm{EG}, \mathrm{EU}\)
Wie berechnet man eine CTL-Formel
Durch Fixpunktiteration des größten/kleinsten Fixpunkts.
Fazit
Entspannte Prüfung mit humanem Fragenkorpus.
Die Vorlesung umfasst sehr viele Themen, geprüft wird aber nur, was auch in den Übungen vorkam und einige generellen Konzepte.
Am Ende schwankt der Prüfer zwischen 1,3 und 1,7, entscheidet sich für 1,3 (danke).