文章基本信息

标题：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通信プロトコルが通信信頼性を満たすことの証明譜による検証を解説する．