Anzeige
Erschienen in:
2001 | OriginalPaper | Buchkapitel
From Falsification to Verification
verfasst von : Doron Peled, Amir Pnueli, Lenore Zuck
Erschienen in: FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science
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 enhances the linear temporal logic model checking process with the ability to automatically generate a deductive proof that the system meets its temporal specification. Thus, we emphasize the point of view that model checkingcan also be used to justify why the system actually works. We show that, by exploitingthe information in the graph that is generated during a failed search for counterexamples, we can generate a fully deductive proof that the system meets its specification.