mse-v_fragen2.txt

Card Set Information

Author:
Anonymous
ID:
126726
Filename:
mse-v_fragen2.txt
Updated:
2012-01-09 05:38:16
Tags:

Folders:

Description:
verhalten
Show Answers:

Home > Flashcards > Print Preview

The flashcards below were created by user Anonymous on FreezingBlue Flashcards. What would you like to do?


  1. Validierung vs. Verifikation
    • Validierung: Vertrauen durch Simulation -> Experimente; kein Nachweis über Korrektheit
    • Verifikation: (formale) Beweis, dass Implementierung die Spezifikation erfüllt
  2. Überblick formale Verifikation
    • Spezifikation gewöhnlich nur informell, vage, unscharf, uneindeutig
    • Formale Verifikation nur mit formaler Spezifikation
    • Modellbasiert oder beweistheoretische Techniken
    • Equivalence Checking oder Model Checking (Property Checking)
    • Kann nicht fehlerfreiheit beweisen
  3. Formale Spezifikation
    • Vollständige Beschreibung von Eigenschaften/Verhalten in mathem. fundierter Sprache
    • Möglichst abstrakte Beschreibung, keine unnötigen Details
    • Kann fehlerhaft/unvollständig sein
  4. Equivalence Checking
    • Nachweis, dass zwei Beschreibungen indentisch Verhalten (formale Spezifikation, Implementierung)
    • Innerhalb einer Abstraktionseben
  5. Property Checking
    • Nachweis, dass Implementierung Menge von spezif. Eigenschaften erfüllt (properties)
    • Verifikation von Entwurfsschritten zw. versch. Abstraktionsebenen
  6. Schaltfunktionen
    • gehört zu den Booleschen Funktionen
    • beschreiben Verhalten digitaler Hardware (kombinatorische und sequentiell)
    • Repräsentationen: Boolesche Gleichungen, Wertetabellen, Aussagenlogik, BDDs
  7. Schaltfunktionen in Wertetabellen
    • Vorteil: besitzt Normalformeigenschaft, führt immer zu identischen Tabellen
    • Nachteil: 2^2^n Schaltfunktionen mit n Vars, Tabelle wächst exponentiell
  8. Schaltfunktionen in Aussagenlogik
    • x ->y := (¬x+y) Implikation
    • x<->y := (xy + ¬x¬y) Äquivalenz
  9. BDDs
    • Binary Decision Diagrams
    • Graphische Repräsentation der Shannon-Zerlegung mit Knoten = Entscheidungsvar
    • Erfordern keine zweistufige Normalformdarstellung (Min-/Maxtermnormalform)
    • Knoten eliminieren: wenn beiden Pfeile auf das gleiche zeigen; wenn Subgraphen isomorph sind.
  10. Überblick ROBDDs
    • Reduced Ordered BDDs
    • definiert rekursiv eine Schaltfunktion
    • Algorithmus: für alle Ebenen/Variablen; für alle Knoten; Zweige vergleichen/zusammenfassen; identische Subgraphen suchen/zusammenfassen
    • Variablenordnung beeinflusst stark die Größe
    • In der Praxis bewährt
  11. Eigenschaften ROBDDs
    • Gültigkeit: ROBDD für gültige Fkt. -> nur ein T-Knoten
    • Erfüllbarkeit: ROBDD für nicht erfüllbare Fkt. -> nur ein F-Knoten
    • Finden erfüllbarer Einsetzung: Durchlauf Wurzel bis T-Knoten
    • Größe: Kann exponentiell mit n wachsen
  12. Equivalence Checking für komb. Schaltungen
    • Repräsentation durch Schaltfunktionen zB f2(x1,x2,x3)=f1+x1*x2
    • Implizit: Zwei Schaltungen auf gleicher Ebene -> ROBDD -> Isomorph?
    • Explizit: Formulierung Beweisziel (XOR-Verknüpfung zweier Schaltungen) -> ROBDD/T-Knoten -> Tautologie?
  13. Equivalence Checking für seq. Schaltungen
    • Algorithmus der Äquivalenz der Startzustände nachweist!
    • Auf Basis der Zustandsäquivalenz der Produktautomaten
  14. Produktautomat
    • Zustände des Prod.Automaten werden durch Zustandspaar beider Automaten gebildet (Kreuzprodukt)
    • Gleiches Eingabealphabet, Ausgang Binär
    • Beliebige Eingangssequenz -> Ausgang wahr bei funktionaler Äquivalenz
  15. Endliche Automaten
    • Transductor, übersetzt Eingangsfolge in Ausgangsfolge
    • Akzeptor, Eingangsfolge genügt Akzeptanzbedingungen
  16. Mealy-Automat
    • M=(Q,SIGMA,DELTA,delta,lambda,q^0)
    • Q: Zustände
    • SIGMA: Eingangsalphabet
    • DELTA: Ausgangsalphabet
    • delta: Zustandsüberg.fkt. QxSIGMA->Q
    • lambda: Ausgangsfkt. QxSIGMA->DELTA
    • q^0: Startzustand
    • Moore-Automat: nicht von Eingangszustand abhängig
    • lambda: Q->DELTA
  17. Quotientenautomat
    Wenn sich Redundanzen (äquivalente Zustände) durch einen Zustand ersetzen lassen.
  18. Büchi-Automat
    • für unendlich lange Eingabefolgen
    • Sequenz ist akzeptiert, wenn er in einem F-State bleibt
  19. Charakteristische Funktionen
    Effiziente Variante zur relationalen Darstellung (y<->x1*x2) von Schaltfkt.
  20. Vorgehensweisen Equivalence Checking FSMs
    • Explicit State Space Traversal: Tiefensuche ohne Produktautomat
    • Symbolic State Space Traversal: Breitensuche auf Produktautomat, Zustände als Menge, Mengen durch charakt. Fkt.
  21. Equivalence-Checking-Algorithmus
    • 1. Startzustand -> Menge in einem Schritt erreichbarer Zustände
    • 2. Prüfen, ob einer der Zustandsübergänge F liefert -> Nicht Äquivalent!
    • 3. Menge in einem Schritt erreichbarer Zustände
    • 4. Wenn keine neuen Zustände -> Äquivalent!
    • 5. weiter mit 2.

What would you like to do?

Home > Flashcards > Print Preview