Applications of Property-Based Synthesis in Formal Verification

Die vorliegende Dissertation stellt eine neue Form des eigenschaftsbasierten Entwurfs vor. Neben den schon bekannten Techniken zur Erzeugung von Monitoren und funktionierender Hardware wird eine Methodik zur Erzeugung sogenannter Cando-Objekte vorgestellt. Der Begriff 'Cando-Objekt' bezeichnet die allgemeinste Form eines Schaltkreises, der einem Eigenschaftssatz genügt. Alle Eigenschaften eines Cando-Objekts müssen daher auch für alle Entwürfe gelten, für die die Eigenschaften gelten, aus denen das Cando-Objekt erzeugt wurde. Cando-Objekte können verwendet werden, um Systemeigenschaften anhand von Moduleigenschaften zu beweisen, um Moduleigenschaften sicher aus Systemeigenschaften abzuleiten und um Eigenschaftssätze zu vergleichen. Neben diesen primären Anwendungen erlaubt es der Generierungsprozess, Informationen zur Konsistenz und Vollständigkeit von Eigenschaftssätzen zu gewinnen.

Die vollständige Präsentation der zur Generierung der Cando-Objekte verwendeten Algorithmen und ihrer praktischen Anwendungen wird durch detaillierte experimentelle Resultate ergänzt. Die beschriebenen Experimente demonstrieren, wie eine Software, die die vorgestellten Algorithmen implementiert, mit industriellen Eigenschaftssätzen umgehen kann.