|
Newsletter Ausgabe Januar 10 |
|
Dienstleister für die Wissenschaft |
|
Schickel, Martin Applications of Property-Based Synthesis in Formal Verification 978-3-86624-464-1 39.00 EUR |
|
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. |