CSP-CASL-Prover: A Generic Tool for Process and Data Refinement |
| |
Authors: | Liam O'Reilly Markus Roggenbach Yoshinao Isobe |
| |
Affiliation: | aSwansea University, United Kingdom;bAIST, Tsukuba, Japan |
| |
Abstract: | The specification language Csp-Casl allows one to model processes as well as data of distributed systems within one framework. In our paper, we describe how a combination of the existing tools Hets and Csp-Prover can solve the challenges that Csp-Casl raises on integrated theorem proving for processes and data. For building this new tool, the automated generation of theorems and their proofs in Isabelle/HOL plays a fundamental role. A case study of industrial strength demonstrates that our approach scales up to complex problems. |
| |
Keywords: | Process Algebra Algebraic Specification Theorem Proving Functional Programming |
本文献已被 ScienceDirect 等数据库收录! |