CafeOBJ入門(4) : 証明譜による検証法  [in Japanese] Introducing CafeOBJ (4) : Verification with Proof Scores  [in Japanese]

Search this Article

Author(s)

Abstract

証明譜を用いた簡約のみに基づくCafeOBJの検証法を解説する.待ち行列を用いる相互排除プロトコルQlockの相互排除性の検証を例として,証明譜を用いた検証法の原理や仕組みを説明するとともに,証明譜の記述の技法も解説する.CafeOBJ's verification method with proof scores which only uses reductions is presented. The example of QLOCK (mutual exclusion protocol with a waiting queue) is used to present theory and principle of the verification method, and techniques for writing the proof scores are also explained.

Journal

  • コンピュータソフトウェア

    コンピュータソフトウェア 25(4), 68-84, 2008-10-28

    日本ソフトウェア科学会

References:  3

Codes

  • NII Article ID (NAID)
    110006990888
  • NII NACSIS-CAT ID (NCID)
    AN10075819
  • Text Lang
    JPN
  • Article Type
    REV
  • ISSN
    02896540
  • NDL Article ID
    9701113
  • NDL Source Classification
    ZM13(科学技術--科学技術一般--データ処理・計算機)
  • NDL Call No.
    Z14-1033
  • Data Source
    CJP  NDL  NII-ELS 
Page Top