Proof scores method is an interactive verification method in algebraic specifications that combines manual proof planning and reduction (automatic inference by rewriting). Proof score approach to software verification coordinates efficiently human intuition and machine automation. In this paper we are interested in applying these ideas to transition systems, more concretely, in developing the so-called OTS/CafeOBJ method, a modeling, specification, and verification method of Observational Transition Systems (OTS). We propose a methodology for applying the previously developed formal proof rules for the proof score method into a precise and efficient way. A main goal of this methodology is to increase the possibility of automating the proof score development. As a novelty, we use, besides of equations, rewriting rules for reduction but with the same denotational semantics as that of equations, namely the equality. From the operational semantics point of view, the reduction system consisting of rewriting rules is regarded as a second reduction system on top of the equational one. A main advantage of this is the preservation of the termination and easier handling of the non-confluent specifications obtained during the proving process. The methodology is exhibited on the example of the alternating-bit-protocol, where the unreliability of channels is faithfully specified. |