From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories
复制标题
从隐藏到可见：将行为理论转变为重写理论的统一框架
DOI：
10.1016/j.tcs.2018.01.006
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
K. Ogata
中科院分区：
文献类型：
--
作者：
Min Zhang;K. Ogata
Algebraic formalization and verification are effective and practical ways of modeling and verifying software systems by both model checking and theorem proving techniques. In algebraic approaches, a system can be modeled either in ahiddenway as a behavioral theory or in avisibleway as a rewrite theory. Several approaches have been proposed to transform behavioral theories into rewrite theories for integrating model checking and theorem proving in verification. In this paper, we propose a framework for transforming behavioral theories into rewrite theories, which unifies four existing related transformation approaches. In this framework, each existing transformation approach can be viewed as a process of transforming behavioral theories first into a special class of behavioral theories and finally into rewrite theories. From this perspective, these transformation approaches differ from each other only in the transformation from ordinary behavioral theories into the classified ones, and their transformations from the classified ones into rewrite theories are essentially the same. We prove that the transformation framework preserves linear-time properties. The preservation of linear-time properties guarantees that a counterexample found by model checking a linear-time property with a generated rewrite theory is also a counterexample in the original behavioral theory, as required by integrated verification.
登录
查看更多内容
从行为规范到重写规范的规范转换
DOI：
--
发表时间：
2008
期刊：
IEICE Transactions 91-D(5)
影响因子：
--
作者：
Masaki Nakamura;Weiqiang Kong;Kazuhiro Ogata;Kokichi Futatsugi
通讯作者：
Kokichi Futatsugi
用于系统验证的定理证明和模型检查的轻量级集成
DOI：
--
发表时间：
2005
期刊：
Proc.of The 12th Asia-Pacific Software Engineering Conference (APSEC 2005)
影响因子：
--
作者：
Weiqiang Kong;Kazuhiro Ogata;Takahiro Seino;Kokichi Futatsugi
通讯作者：
Kokichi Futatsugi
OTS/CafeOBJ 方法中的证明分数
DOI：
--
发表时间：
2003
期刊：
Lecture Notes in Computer Science,(FMOODS 2003), 2884
影响因子：
--
作者：
Kazuhiro Ogata;Kokichi Futatsugi
通讯作者：
Kokichi Futatsugi
从 OTS/CafeOBJ 到 OTS/Maude 的完整规范转换
DOI：
--
发表时间：
2006
期刊：
影响因子：
--
作者：
Masaki Nakamura;Weiqiang Kong;Kazuhiro Ogata;Kokichi Futatsugi
通讯作者：
Kokichi Futatsugi
SET 形式化验证的方程方法
DOI：
--
发表时间：
2004
期刊：
Proceedings of the 4th International Conference on Quality Software (4th QSIC),(IEEE Computer Society Press)
影响因子：
--
作者：
Kazuhiro Ogata;Kokichi Futatsugi
通讯作者：
Kokichi Futatsugi