FSV Kapitel 1

Description

Flashcards on FSV Kapitel 1, created by Stael Tchinda on 01/07/2019.
Stael Tchinda
Flashcards by Stael Tchinda, updated more than 1 year ago
Stael Tchinda
Created by Stael Tchinda almost 5 years ago
5
0

Resource summary

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:
Show full summary Hide full summary

Similar

British Empire
chloeeatsalot
AS Unit 1 Physics Flashcard Deck
Callum McClintock
CHEMISTRY C1 4
x_clairey_x
IB Economics SL: Microeconomics
Han Zhang
Themes of Jane Eyre
blackfeather1128
anatomy of the moving body: Skeletal system
Rupa Kleyn
atoms and elements
Danoa400
Roles of Education
Isobel Wagner
PuKW - STEP 1 (mögliche Prüfungsfragen/Prüfungsvorbereitung)
Steven Lee
5 Big Ideas
cassie_dodd
GCSE - AQA: C1.1 The Fundamental Ideas in Chemistry
Olly Okeniyi