2005 | OriginalPaper | Buchkapitel
BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking
verfasst von : Damien Bergamini, Nicolas Descoubes, Christophe Joubert, Radu Mateescu
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
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
The equivalence checking problem consists in verifying that a system (e.g., a
protocol
) matches its abstract specification (e.g., a
service
) by comparing their Labeled Transition Systems (
Lts
s) modulo a given equivalence relation. Two approaches are traditionally used to perform equivalence checking:
global
verification requires to construct the two
Lts
s before comparison, whereas
local
(or
on-the-fly
) verification allows to explore them incrementally during comparison. The latter approach is able to detect errors even in prohibitively large systems, and therefore reveals more effective in combating state explosion.