Name
Abstract | ||
|---|---|---|
The stable revivals model R provides a new semantic framework for the process algebra Csp. The model R has recently been added to the realm of established Csp models. Within the Csp context, it enhances the analysis of systems with regards to properties such as responsiveness and stuckness. These properties are essential in component based system design. In this paper we report on the implementation of different variants of the model R within Csp-Prover. Based on Isabelle/HOL, Csp-Prover is an interactive proof tool for Csp refinement, which is generic in the underlying Csp model. On the practical side, our encoding of the model R provides semi-automatic proof support for reasoning on responsiveness and stuckness. On the theoretical side, our implementation also yields a machine verification of the model R's soundness as well as of its expected properties. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1016/j.entcs.2009.08.021 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
csp,csp context,established csp model,interactive proof tool,process algebra csp,isabelle/hol,stable revivals,stable revivals model r,practical side,model r,underlying csp model,stable revivals model.,stable revivals model,csp refinement,semi-automatic proof support,process algebra | HOL,Discrete mathematics,Semantic framework,Computer science,Systems design,Theoretical computer science,Soundness,Process calculus,Gas meter prover,Encoding (memory) | Journal |
Volume | Issue | ISSN |
250 | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
2 | 0.36 | 11 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| D. Gift Samuel | 1 | 2 | 0.36 |
| Markus Roggenbach | 2 | 294 | 32.63 |
| Yoshinao Isobe | 3 | 58 | 7.84 |