Lehr- und Forschungseinheit
Institut
Universität
Lehr- und Forschungseinheit für Theoretische Informatik,
Institut für Informatik der Ludwig-Maximilians-Universität
München
Bounded Model Checking (BMC) ist eine symbolische Verifikationsmethode, die hauptsächlich zum Auffinden von Fehlern in Hardwarebausteinen mittels Spezifikation in Linearzeitlogiken eingesetzt wird.
Anstatt exhaustiv alle möglichen Läufe eines Systems nach Fehlern zu untersuchen, betrachtet man nur Läufe beschränkter Länge. Der Erfolg von BMC, was durchaus industriell eingesetzt wird, begründet sich darauf, dass Fehler oft früh im System auftreten, und dass deshalb nicht das gesamte System betrachtet werden muss.
Bisher wurde BMC hauptsächlich für die temporale Logik LTL eingesetzt. LTL ist jedoch bzgl. seiner Ausdruckstärke recht schwach. Es kann noch nicht einmal alle regulären Sprachen beschreiben. Im Rahmen des Projekts μ-Sabre an der LFE TCS wird in einem ersten Schritt BMC für alle regulären Sprachen entwickelt. Dazu wird hauptsächlich der Linearzeit μ-Kalkül, eine generische Erweiterung von LTL, verwendet.
Es gibt jedoch Korrektheitseigenschaften (insbesondere von Übertragungs-Protokollen), die noch nicht einmal regulär sind. Bsp.: Es werden niemals mehr send- als receive-Aktionen gemacht.
Ziel dieses Diplomarbeit ist es, die angefangene Erweiterung von BMC noch über reguläre Eigenschaften hinaus voranzutreiben. Dazu bietet sich Linear Time Fixpoint Logic with Chop (LFLC) an, wiederum eine Erweiterung des Linearzeit μ-Kalküls. In einem vorbereitenden Schritt kann BMC für reguläre Ausdrücke mit Durchschnitt, was jedoch ebenfalls nur reguläre Sprachen definiert, entwickelt werden.
Literatur/Material/Links:
Dr. Martin Lange, D1.07, Oettingenstr. 67, Tel.: 089 21809313