 |
| | | | | Beschreibung | | Durch eine (formale) Verifikation im Software- und Hardwareengineering wird die Übereinstimmung der Eigenschaften der erstellten Artefakte (z.B. Dokumente, Modelle, Implementierungen) einer (Entwicklungs-)Phase gegenüber einer anderen (i.d.R. direkt anschließenden) sichergestellt.
In diesem Kontext werden dabei exemplarisch die Spezifikations- und Modellierungs(Design-)phase betrachtet und daher soll die Verifikation in diesem Fall die Korrektheit des Modells und damit die Erfüllung der Eigenschaften einer Spezifikation gegenüber einem Modellbildung nachweisen. Der Unterschied zu einer "einfachen" Simulation (z.B. einem Debuggingdurchlauf "von Hand"), in der oftmals aufgrund des damit verbundenen hohen zeitlichen Aufwands nur ein Teil aller möglichen aber häufig notwendigen Simulationsläufe durchgeführt werden kann, liegt in der Vollständigkeit und Konsistenz eines solchen Nachweises.
Um eine (formale) Verifikation durchzuführen existieren die zwei grundsätzlichen Ansätze Theorem Proving und Model Checking, welche u.a. in ihrem (möglichen)Automatisierungsgrad, notwendigen Vorkenntnissen und verifizierbaren Modellen differieren. So kann beispielsweise das Model Checking durch entsprechende Entwicklungsprogramme (nahezu) ohne weitere Vorkenntnisse vollständig durch einen Rechner durchgeführt werden, wohingegen beim Theorem Proving zwar mittlerweile rechnergestützt vorgegangen werden kann, aber immer noch ein speziell ausgebildeter Verifikationsexperte vonnöten ist.
Damit eine formale Verifikation durchgeführt werden kann müssen Spezifikation und Modell in einer formalen Repräsentation vorliegen. Zur Spezifikation werden dabei u.a. Symbolic Timing Diagrams (die dann in eine Form von Formale Logiken umgewandelt werden) , zur Modellbildung bspw. (welche dann in Endlicher Automaten übersetzt werden) benutzt.
Die formale Repräsentation ist von grundlegender Bedeutung, weil sie die Definition einer formalen Semantik ermöglicht, welche notwendig ist für jede Form der formalen Verifikation, egal ob sie automatisch, (semi-)automatisch oder manuell durchgeführt wird. Eine solche formale Semantik ist entscheidend für die Verifikation, weil dadurch Missverständnisse bei der Interpretation von Spezifikation und Modell ausgeschlossen werden können.
| |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | |  | Übergeordnet | | | | | | | | | | | Verifikation (formal) | | | | |  | Untergeordnet | | | | | | | | | | | | | | | | | | Erfahrungen | | | | | | | | | | | Ansprechpartner | | | | | | | | | | | Literaturhinweise | | | | | | | | | | | | | | | | Löst die Probleme | | | | | | | | | | | | | | | | | | | | | | Weitere Themen | | | | | | | | | | | | | | Glossar | | | | | | | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
