Japan Society for Software Science and Technology = 日本ソフトウェア科学会
抄録
An example of verification of communication protocols with CafeOB J 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.
権利
(c) Japan Society for Software Science and Technology 2009
CafeOBJ 入門 (6) : 通信プロトコルの検証
TE-PR-NAKAMURA-M-93.pdf
(175.65KB)
