Introducing CafeOBJ (6) : Verification of a Communication Protocol

  • OGATA Kazuhiro
    Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • FUTATSUGI Kokichi
    Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • NAKAMURA Masaki
    School of Electrical and Computer Engineering, Kanazawa University

Bibliographic Information

Other Title
  • CafeOBJ入門(6) 通信プロトコルの検証
  • チュートリアル CafeOBJ ニュウモン 6 ツウシン プロトコル ノ ケンショウ

Search this article

Abstract

An example of verification of communication protocols with CafeOBJ algebraic specification language is shown. The SCP communication protocol is a simplified version of the ABP communication protocol, which uses unreliable cells as communication channels between senders and receivers. The reliable communication property is as follows: when a receiver receives N packets, they are the first N packets that a sender has sent and the order in which the N packets has been sent is preserved. Described is the verification with proof score that the SCP communication protocol satisfies the reliable communication property.

Journal

  • Computer Software

    Computer Software 26 (2), 93-106, 2009

    Japan Society for Software Science and Technology

Citations (1)*help

See more

References(5)*help

See more

Related Projects

See more

Details

Report a problem

Back to top