Skip to main content

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

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Metadaten
Titel
Verification of synchronous sequential machines based on symbolic execution
verfasst von
Olivier Coudert
Christian Berthet
Jean Christophe Madre
Copyright-Jahr
1990
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-52148-8_30

Neuer Inhalt