On automation of OTS/CafeOBJ method

Daniel Gǎinǎ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)578-602
Number of pages25
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8373
DOIs
Publication statusPublished - Jan 1 2014
Externally publishedYes

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this