2001 | OriginalPaper | Buchkapitel
From model checking to a temporal proof
verfasst von : Doron Peled, Lenore Zuck
Erschienen in: Model Checking Software
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
Model checking is used to automatically verify temporal properties of finite state systems. It is usually considered to be ‘successful’, when an error, in the form of a counterexample to the checked property, is found. We present the dual approach, where, in the pres- ence of no counterexample, we automatically generate a proof that the checked property is satisfied by the given system. Such a proof can be used to obtain intuition about the verified system. This approach can be added as a simple extension to existing model checking tools.