1990 | ReviewPaper | Buchkapitel
Verification of synchronous sequential machines based on symbolic execution
verfasst von : Olivier Coudert, Christian Berthet, Jean Christophe Madre
Erschienen in: Automatic Verification Methods for Finite State Systems
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper presents an original method to compare two synchronous sequential machines. The method consists in a breadth first traversal of the product machine during which symbolic expressions of its observable behaviour are computed. The method uses formal manipulations on boolean functions to avoid the state enumeration and diagram construction. For this purpose, new algorithms on boolean functions represented by Typed Decision Graphs has been defined.