 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Model Checking (Motivation) |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Die heutzutage in industriell relevanten Systemen eingesetzte Software und Hardware hat eine Komplexität, die mit traditionellen Methoden wie Simulation und Testen einzelner Szenarien nicht mehr zu bewältigen ist. Betrachtet man zum Beispiel eine einfache Zentralverriegelung, wie sie in einem modernen Auto eingebaut wird, so würde man für die Untersuchung der gesamten Zentralverriegelung Jahre benötigen, vorausgesetzt man könnte jede einzelne Konfiguration dieser Zentralverriegelung innerhalb einer Nanosekunde simulieren und testen.
In traditionellen Ansätzen wird daher eine große Anzahl von Konfigurationen gar nicht erst bei der Simulation und beim Testen berücksichtigt, was möglicherweise fatale Konsequenzen haben kann. Beispielsweise explodierte die Trägerrakete Ariane 5 37 Sekunden nach der Zündung der Triebwerke, weil ein falsch konvertierter Messwert die Steuerungsrechner zum Abschalten zwang. Da die Sicherstellung der Korrektheit von Hard- und Software insbesondere im Bereich sicherheitskritischer Systeme das zentral zu lösende Problem darstellt, werden in Prozessmodellen (z.B. V-Modell) bereits seit geraumer Zeit formale Nachweise der Korrektheit gefordert. Grundlage dafür ist die Erstellung eines Systemmodells sowie die Formulierung der Anforderungen auf Basis formaler Notationen mit eindeutiger Semantik. Durch mathematische Verfahren kann nachgewiesen werden, dass das Modell die spezifizierten Anforderungen erfüllt. Im Gegensatz zu herkömmlichen Testverfahren sind formale Korrektheitsnachweise vollständig. Beim Testen kann nur eine begrenzte Auswahl möglicher Systemläufe betrachtet werden. Wird dabei kein Fehler gefunden, kann trotzdem einer existieren. Ein formaler Korrektheitsnachweis betrachtet hingegen alle Systemläufe. Derartige Nachweise mussten bislang ebenso wie auch die Transformation bzw. Formalisierung des Systemmodells und der Spezifikation manuell durch einen Verifikationsexperten angefertigt werden. Dies bringt zwar den Vorteil der Vollständigkeit, ist aber ebenfalls zeit- und kostenintensiv sowie fehleranfällig. Zur Vermeidung dieser Nachteile müssen Automatismen entwickelt werden, die bei der Konstruktion der Beweise unterstützen bzw. diese vollständig rechnergestützt auf Basis der im Entwicklungsprozess entstehenden Zwischenergebnisse anfertigen können. Ein aussichtsreicher Ansatz zur Lösung dieser Problematik ist das sogenannte „Model Checking“. Es handelt sich dabei um ein automatisiertes Verfahren zur Verifikation von endlichen zustandsbasierten nebenläufigen Systemen. Die Anfertigung des mathematischen Nachweises geschieht vollständig durch einen Rechner. Weiter zum nächsten Gliederungspunkt: Model Checking | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Model Checking (Motivation) | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
