Verifikation eines Microkernels
Verifikation eines Microkernels
| Typ: |
Seminarthema |
| Betreuer: |
Thorsten Bormer |
|
|
Die formale Verifikation komplexer, großer Softwaresysteme stellt eine besondere Herausforderung dar.
Ein Beispiel eines solchen Vorhabens ist das Projekt "L4.verified". Ziel dieses Projekts ist der
Korrektheitsbeweis der Implementation eines L4-basierten Microkernels, "seL4". Eine Übersicht
über das Projekt und die darin erzielten Ergebnisse der Ende 2009 abgeschlossenen Verifikation wurden 2010
in den Communications of the ACM vorgestellt.
Der Inhalt des Vortrages sollte eine Übersicht der zugesicherten Korrektheitseigenschaften umfassen,
die im Projekt verwendete Verifikationsmethodik erläutern, sowie einen Vergleich des Vorhabens mit
ähnlichen Verifikationsprojekten ermöglichen.
