18612940
Description
Flashcards by Stael Tchinda, updated more than 1 year ago
|
Created by Stael Tchinda
over 5 years ago
|
|
| Question | Answer |
| Blatt 1 Ready ? | Go ! |
| Was zeichnet ein für die Verifikation ideales Modell aus? Nennen und erklären Sie zwei Ursachen, die zu suboptimalen Modellen führen! | Weder zu abstrakt noch zu konkret. - Ist das Modell zu abstrakt, erfüllt es eventuell die Spezifikation nicht, obwohl dies auf das System, das modelliert werden sollte, zutrifft (wichtige Teile wurden wegabstrahiert). - Ist das Modell zu konkret, kann die Verifikation an unnöötiger Komplexität scheitern (unwichtige Teile wurden nicht wegabstrahiert) . |
| Was ist im Allgemeinen das Ziel der formalen Verifikation hinsichtlich der Pfade eines Systems? Wie steht dies im Bezug zum Testen? | Verifikation versucht Aussagen über alle Pfade im System zu machen. Testen dagegen kann in der Regel nur Aussagen über einige Pfade im System machen |
| Nennen Sie 4 Modellierungssprachen! | -Modellierung: • Automatenbasierte Ansätze • Prozess-Algebren • Petri-Netze • C-Code |
| Nennen Sie 2 Spezifikationssprachen! | - Spezifikation: • Temporallogik • Automaten |
| Erkären sie die beiden Wortbestandteile des Begriffs "Formale Verifikation" ! | Formal mathematisch: versucht die Aussagen präzise und rigoros zu machen Verifikation versucht Aussagen über alle Pfade im System zu machen |
| Wie schwer ist formale Verifikation von Software? Können Sie dem Software-Verifikationsproblem eine Komplexitätsklasse zuweisen? Nennen Sie diese bzw. geben Sie eine Begründung, falls dies nicht möglich sein sollte! | - i.A. unentscheidbar - Aber: entscheidbar für eingeschränkte Systeme, z.B. viele abstrakte Modelle, Halteproblem |
| Welche Klassen von Eigenschaften gibt es, die man verifizieren kann? | - Sicherheitseigenschaften (safety) - Lebendigkeitseigenschaften (liveness) |
| Erklären Sie, was Sicherheitseigenschaften sind ? (mit Beispielen und wie man sie beweisen kann) | "Etwas Schlechtes wird nicht passieren." (bei keiner möglichen Ausfüuhrung des Programms) - Beispiele: • Programm stürzt nicht ab. • Ausgabe ist immer im erlaubten Wertebereich. • Programm läuft nie in einen Deadlock - Gegenbeispiel: Konkreter endlicher Pfad durch das Programm vom Anfang zur Spezifikationsverletzung (= Testfall) - Beweis: Vollständiges Absuchen aller erreichbaren Zustände; Induktionsbeweis durch Invariante, die die Eigenschaft impliziert |
| Erklären Sie, was Lebendigkeitseigenschaften sind ? (mit Beispielen und wie man sie beweisen kann) | "Etwas Gutes wird (irgendwann) passieren." (bei jeder möoglichen Ausführung des Programms) - Beispiele: • Programm terminiert. • Während der Laufzeit des Programms gibt es nach jeder Eingabe eine Ausgabe aus. - Gegenbeispiel (bei nicht-terminierendem Programm): Unendlicher langer Pfad ohne Spezifikationserfüllung (Lasso) - Beweis: Vollständiges Absuchen aller erreichbaren Zustände; Induktionsbeweis durch Invariante, die die Eigenschaft impliziert |
| Wie erkennen, ob eine Eigenschaft Sicherheits- oder Lebendigkeitseigenschaft ist ? | Überlegen Sie sich, ob die Eigenschaft ein endliches Gegenbeispiel hat! Ja => Sicherheitseigenschaft Nein => Lebendigkeitseigenschaft |
| Blatt 1 fertig Got it ? | Yeah ! |
| 1.3 Sprachen für Spezifikationen und Modelle Ready (for the rest) ? | Go ! |
| Was sind die (3) Aspekte, um Modellierungssprachen zu unterscheiden | 1. Variablen oder Ereignisse (Events) 2. synchrone oder asynchrone Kommunikation 3. echte oder künstliche Parallelität |
| 1.4 Ansätze zur Verifikation Ready (for the rest) ? | Go ! |
| Was sind diese Einsätze ? (2) | - Interaktive (Theorembeweiser) Verifikation - Algorithmische (Model-Checking-basierte) Verifikation: |
Want to create your own Flashcards for free with GoConqr? Learn more.