The Stable Revivals Model in CSP-Prover
The Stable Revivals Model in CSP-Prover
复制标题
DOI：
10.1016/j.entcs.2009.08.021
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
D. Gift Samuel;M. Roggenbach;Yoshinao Isobe
中科院分区：
文献类型：
--
作者：
D. Gift Samuel;M. Roggenbach;Yoshinao Isobe
稳定复活模型R为进程代数Csp提供了一个新的语义框架。模型R最近被添加到已建立的CSP模型的领域。在Csp上下文中，它增强了对系统特性（如响应性和稳定性）的分析。这些属性在基于组件的系统设计中是必不可少的。在本文中，我们报告了Csp-Prover中模型R的不同变体的实现。Csp-Prover是一个基于Isabelle/HOL的交互式Csp精化证明工具，它在底层Csp模型中是通用的。在实践方面，我们对模型R的编码为响应性和粘性的推理提供了半自动的证明支持。在理论方面，我们的实现也产生了一个机器验证模型R的健全性，以及其预期的属性。
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.