 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Model Checking (Zustandsexplosion) |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Ein wesentliches Problem bei der Anwendung des Model Checking auf realistische Systeme ist die sogenannte Zustandsexplosion: Durch die parallele Ausführung von Programmen in Software oder den parallelen Betrieb einzelner Schaltkreise vgl. Nebenläufige Systeme) wächst die Anzahl der möglichen Zustände exponentiell an, so dass eine Untersuchung des Gesamtsystems mit Hilfe des Model Checking immer schwieriger und zeitaufwendiger wird. Systeme mit unendlichen Zustandsmengen sind einer automatischen Verifikation mit Hilfe des Model Checking zunächst nicht zugänglich.
Es existieren jedoch bereits zahlreiche Ansätze aus der Forschung, um das Problem der Zustandsexplosion anzugehen, so dass sich mittlerweile viele praktisch relevante Modelle erfolgreich verifizieren lassen:
Zurück zum Gliederungspunkt Model Checking (Motivation) | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Model Checking (Zustandsexplosion) | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
