Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
A Generic Theorem Prover of CSP Refinement
verfasst von : Yoshinao Isobe, Markus Roggenbach
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
We describe a new tool called
Csp
-Prover which is an interactive theorem prover dedicated to refinement proofs within the process algebra
Csp
. It aims specifically at proofs for infinite state systems, which may also involve infinite non-determinism. Semantically,
Csp
-Prover supports both the theory of complete metric spaces as well as the theory of complete partial orders. Both these theories are implemented for infinite product spaces. Technically,
Csp
-Prover is based on the theorem prover Isabelle. It provides a deep encoding of
Csp
. The tool’s architecture follows a generic approach which makes it easy to adapt it for various
Csp
models besides those studied here: the stable failures model
$\mathcal{F}$
and the traces model
$\mathcal{T}$
.