文章基本信息
- 标题：CafeOBJ入門(6) 通信プロトコルの検証
- 本地全文：下载
- 作者：緒方 和博 ; 二木 厚吉 ; 中村 正樹 等
- 期刊名称：コンピュータ ソフトウェア
- 印刷版ISSN：0289-6540
- 出版年度：2009
- 卷号：26
- 期号：2
- 页码：2_93-2_106
- DOI：10.11309/jssst.26.2_93
- 出版社：Japan Society for Software Science and Technology
- 摘要：
代数仕様言語CafeOBJによる通信プロトコルの検証の例を示す．SCP通信プロトコルは，ABP通信プロトコルの簡略版で，送受信者間の通信路として信頼できないセルを用いる．受信者がN個のパケットを受け取ったとき，それらは送信者が送った最初のN個のパケットで，順番を保存している，という性質を通信信頼性という．SCP通信プロトコルが通信信頼性を満たすことの証明譜による検証を解説する．
