Eintrag kommentierenErfahrung zum Thema berichtenEintrag bewerten
Dieser Eintrag wurde im Schnitt mit 0 von 5 Punkten bewertet
Verfahren
Model Checking
Methode/Technik:2885
Externe Quellen zum Thema NEU: Externe Quellen zum Thema suchen 
Beschreibung
Überblick - Wie funktioniert Model Checking?

Mit Hilfe der Verifikationstechnik Model Checking ist es möglich, die Modellierung eines Systems (das sogenannte Model, beispielsweise ein das System beschreibende Programm oder ein Zustandsautomat) daraufhin zu überprüfen (Checking), ob sie die Eigenschaften aus einer bestimmten Spezifikation (Beschreibung der Eigenschaften des Modells, beispielsweise durch logische Formeln) erfüllt.

Gegenüber anderen Verifikationstechniken weist Model Checking folgende Vorteile auf:

  • Model Checking ist eine vollständige Verifikationstechnik (eine Benutzer-Interaktion ist nicht notwendig). Der Vorteil gegenüber unvollständigen Verifikationsmethoden (z.B. Testen), ist die Tatsache, dass nach einem erfolgten Verifikationsdurchlauf immer alle Fehler zwischen Modell und Spezifikation aufgedeckt werden.
  • Die Anfertigung des Verifikationsnachweises läuft im Gegensatz anderen vollständigen Verifikationstechniken (z.B. Theorem Proving)) komplett automatisch ab.
  • Im Gegensatz zu anderen vollständigen Verifikationstechniken (z.B. Theorem Proving) muss der Anwender keine Kenntnisse über die Verifikationsmethode besitzen.
  • Im Fehlerfall werden unmittelbar die Eigenschaften der Spezifikation bzw. die Zustände des Systems und der dorthin führende Fehlerpfad aufgedeckt, die Ursache des ermittelten Fehlers sind. Dadurch wird die Fehleranalyse optimiert und es entsteht insgesamt ein effizienterer Entwicklungsprozess.
Das bislang nicht abschließend gelöste primäre Problem des Model Checking ist die sogenannte „Zustandsexplosion“. Darunter versteht man das exponentielle Wachstum der Anzahl der zu untersuchenden Systemzustände bei einer Verifikation. Es existieren jedoch bereits Lösungsansätze aus der Forschung, um das Problem der Zustandsexplosion wirkungsvoll anzugehen.

Zusammenfassend lässt sich sagen, dass sich die Methode des Model Checking mittlerweile auch in der Praxis überaus erfolgreich durchgesetzt hat. Es existieren bereits zahlreiche Werkzeuge (beispielsweise die vom OFFIS entwickelte Statemate Verifikationsumgebung für Statemate Magnum Model Checker), die kommerziell vermarktet und in industriellen Entwicklungsprozessen eingesetzt werden.

Das ursprüngliche Kernanwendungsgebiet für das Model Checking waren digitale Schaltkreise, aufgrund der im Vergleich zur Software oftmals geringeren Komplexität und des dort häufig eher als kritisch einzustufenden Einsatzgebietes. Die immer stärkere Integration von Software in eingebettete Systeme lenkt die Forschungsbestrebungen aber insbesondere auf die Verifikation von Software durch Model Checking.

Interessante Artikel zur Thematik

    Die Gewährleistung der korrekten Funktionsweise von Hard- und Software ist ein entscheidender Faktor bei der heutigen Systementwicklung. Dies trifft ganz besonders auf das Gebiet der sog. „sicherheitskritischen“ Systeme zu. Vor diesem Hintergrund stellt dieser Artikel die Grundlagen des sog. „Model Checkings“ vor, einer automatisch durchführbaren, vollständigen Verifikationsmethode. Ergänzt wird diese Einführung durch einige Beispiele von Erfahrungen (…)

Zurück zum Gliederungspunkt Model Checking (Motivation)
Weiter zum nächsten Gliederungspunkt Model Checking (Zustandsexplosion)

Externe Quellen zum Thema NEU: Externe Quellen zum Thema suchen 
 Eintrag kommentieren 
 Eintrag bewerten 
 Erfahrung zum Thema berichten 
Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben.
 
Zum Seitenanfang Top Drucken Impressum AGB
Home

VSEK ©2001-2017