Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Model Checking PSL Using HOL and SMV
verfasst von : Thomas Tuerk, Klaus Schneider, Mike Gordon
Erschienen in: Hardware and Software, Verification and Testing
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
In our previous work, we formally validated the correctness of a translation from a subset of Accellera’s Property Specification Language
(PSL)
to linear temporal logic
(LTL)
using the
HOL
theorem prover. We also built an interface from
HOL
to the
SMV
model checker based on a formal translation of
LTL
to
ω
-automata. In the present paper, we describe how this work has been extended and combined to produce a model checking infrastructure for a significant subset of
PSL
that works by translating model checking problems to equivalent checks for the existence of fair paths through a Kripke structure specified in higher order logic. This translation is done by theorem proving in
HOL
, so it is proven to be correct. The existence check is carried out using the interface from
HOL
to
SMV
. Moreover, we have applied our infrastructure to implement a tool for validating the soundness of a separate
PSL
model checker.