CafeOBJ入門(4) : 証明譜による検証法(<特集>エージェント) Introducing CafeOBJ (4) : Verification with Proof Scores

この論文にアクセスする

この論文をさがす

著者

抄録

証明譜を用いた簡約のみに基づく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.

収録刊行物

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

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

    日本ソフトウェア科学会

参考文献:  3件中 1-3件 を表示

各種コード

  • NII論文ID(NAID)
    110006990888
  • NII書誌ID(NCID)
    AN10075819
  • 本文言語コード
    JPN
  • 資料種別
    Journal Article
  • ISSN
    02896540
  • NDL 記事登録ID
    9701113
  • NDL 雑誌分類
    ZM13(科学技術--科学技術一般--データ処理・計算機)
  • NDL 請求記号
    Z14-1033
  • データ提供元
    CJP書誌  NDL  NII-ELS  IR 
ページトップへ