氏名: 近藤哲史 (l0351632)
論文題目: プロセス代数による通信プロトコルの仕様記述及び検証の自動化手法の実
現
論文概要
本論文では通信プロトコルをプロセス代数によってモデル化し、その正
当性の検証を行う。通信プロトコルとして、半二重方式のAlternating Bit
Protocolを対象にする。CCSの検証ツールである、Concurrency Workbench
を用いて、バッファとの観測等価性を検証する。
また、プロセス代数として値受け渡しの変数を用いる動作式によってモデ
ル化しているが、Concurrency Workbenchでは値受け渡しの変数を用いるこ
とができない。よって、値受け渡しの変数を用いる動作式でモデル化され
た通信プロトコルの仕様記述を入力すると、変数を値に応じて展開し、
Concurrency Workbenchで用いる動作式に変換するプログラムを作成した。
目次に戻る