On Automation of OTS/CafeOBJ Method
On Automation of OTS/CafeOBJ Method
复制标题
OTS/CafeOBJ方法的自动化研究
DOI：
10.1007/978-3-642-54624-2_29
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Kokichi Futatsugi
中科院分区：
文献类型：
--
作者：
Daniel Gaina;Dorel Lucanu;Kazuhiro Ogata;Kokichi Futatsugi
The proof scores method is an interactive verification method in algebraic specification that combines manual proof planning and reduction (automatic inference by rewriting). The proof score approach to software verification coordinates efficiently human intuition and machine automation. We are interested in applying these ideas to transition systems, more concretely, in developing the so-called OTS/CafeOBJ method, a modelling, specification, and verification method of observational transition systems. In this paper we propose a methodology that aims at developing automatically proof scores according to the rules of an entailment system. The proposed deduction rules include a set of generic rules, which can be found in other proof systems as well, together with a set of rules specific to our working context. The methodology is exhibited on the example of the alternating bit protocol, where the unreliability of channels is faithfully specified.
