CSP-prover
CSP-Prover is an interactive theorem prover dedicated to refinement proofs within the process algebra CSP. It aims specifically at proofs on infinite state systems, which may also involve infinite non-determinism. For this reason, CSP-Prover currently focuses on the stable failures model F as the underlying denotational semantics of CSP. Semantically, CSP-Prover offers both classical approaches to denotational semantics: the theory of complete partial orders (cpo) as well as the theory of complete metric spaces (cms). In this context the respective Fixed Point Theorems are used for two purposes: (1) to prove the existence of fixed points, and (2) to prove CSP refinement between two fixed points. CSP-Prover implements both these theories for infinite product spaces and thus is capable to deal with infinite systems of process equations. Technically, CSP-Prover is based on the generic theorem prover Isabelle, using the logic HOL-Complex. Within this logic, the syntax as well as the semantics of CSP is encoded, i.e., CSP-Prover provides a deep encoding of CSP. The tool’s architecture follows a generic approach which makes it easy to re-use large parts of the encoding for other CSP models. For instance, merely as a by-product, CSP-Prover includes also the CSP traces model T. More importantly, CSP-Prover can easily be extended to the failure-divergence model N and the various infinite traces models of CSP. ..
Keywords for this software
References in zbMATH (referenced in 16 articles , 2 standard articles )
Showing results 1 to 16 of 16.
Sorted by year (- Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim: Automated verification of reactive and concurrent programs by calculation (2021)
- Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)
- Murray, Toby: On the limits of refinement-testing for model-checking CSP (2013)
- Chen, Zhenbang; Liu, Zhiming; Wang, Ji: Failure-divergence semantics and refinement of long running transactions (2012)
- Kleine, Moritz; Sanders, J. W.: Simulating truly concurrent CSP (2011)
- Gruner, S.; Steyn, T. J.: Deadlock-freeness of hexagonal systolic arrays (2010)
- Falcão, Flávia; Iyoda, Juliano; Sampaio, Augusto: Multiple synchrony in MSC (2009)
- Kahsai, Temesghen; Roggenbach, Markus: Property preserving refinement for Csp-Casl (2009)
- Miller, Alice (ed.); Calder, Muffy (ed.): Proceedings of the 8th international workshop on automated verification of critical systems (AVoCS 2008), Glasgow, UK, September 30 -- October 1, 2008 (2009)
- O’Reilly, Liam; Roggenbach, Markus; Isobe, Yoshinao: CSP-CASL-Prover: a generic tool for process and data refinement (2009)
- Samuel, D. Gift; Roggenbach, Markus; Isobe, Yoshinao: The stable revivals model in CSP-Prover (2009)
- Isobe, Yoshinao; Roggenbach, Markus: Proof principles of CSP -- CSP-prover in practice (2008)
- Reeves, Steve; Streader, David: Generic tools via general refinement (2008)
- Isobe, Yoshinao; Roggenbach, Markus: A complete axiomatic semantics for the CSP stable-failures model (2006)
- Roggenbach, Markus: CSP-CASL -- a new integration of process algebra and algebraic specification (2006)
- Isobe, Yoshinao; Roggenbach, Markus: A generic theorem prover of CSP refinement (2005)