| Year | 2014 |
|---|---|
| Type | Conference |
| Status | Submitted |
| Authors | Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi |
Links
Abstract
The proof scores method is an interactive verification method
in algebraic specification that combines manual proof planning and re-
duction (automatic inference by rewriting). The proof score approach
to software verification coordinates eficiently human intuition and ma-
chine automation. We are interested in applying these ideas to transi-
tion systems, more concretely, in developing the so-called OTS/CafeOBJ
method, a modelling, specification, and verification method of observa-
tional 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.