プロトコル検証の例(ABP)

■プロトコル検証の例(ABP)

1. Alternating Bit Protocol (ABP)

2. 通信路誤りありABPのFull LOTOS仕様

3. ABPのobservationalな仕様(SERVICE)

4. 等価性の検証例

練習問題7-1

参考資料・リンク集

2015年4月22日 12:02

 

Full LOTOSによるAlternating Bit Protocol (ABP)を記述する。それについて、外部から見た可観測な値の挙動(SERVICE)との、observational な等価性について検証を行う。

この章で学習する内容は以下の4つである。最後に演習問題4を与える。

1. Alternating Bit Protocol (ABP)
2. 通信路誤りありABPのFull LOTOS仕様
3. ABPのobservationalな仕様(SERVICE)
4. 等価性の検証例

練習問題7-1

●Alternating Bit Protocol (ABP)

1.1 概要
1.2 通信路誤りありABP


1.1 概要

交番ビットプロトコル(Alternating Bit Protocol (ABP))とは、転送誤りを起こすような通信路を挟んで、片方向のメッセージ転送を行う際、送信側はメッセージに、そのメッセージの番号を交番ビットとして付与し、受信側はメッセージに付与された交番ビットと、受信側が期待した番号との比較を行うことで、受信成功(ack)あるいは受信誤り(nack)を送信側へ伝え、送信側からの再送処理を行うものである。

送信側(TRANS)から受信側(RECV)へのメッセージ送信時には、以下のケースがある。

(TR1) 送信されたメッセージは、正常に受信側へ届く。
(TR2) 送信されたメッセージは、通信路Medium1上で誤り、受信側へ届く。
(TR3) 送信されたメッセージは、通信路Medium1上で消失し、受信側へ届かない。

受信側(RECV)から送信側(TRANS)へのack/nack通知時には、以下のケースがある。

(RT1) 通知した ack は、正常に送信側へ届く。
(RT2) 通知した ack は、通信路Medium2上で誤り、送信側へ届く。
(RT3) 通知した ack は、通信路Medium2上で消失し、送信側へ届かない。


1.2 通信路誤りありABP

通信路誤りがある場合(i.e. 通信路がlossyなMediumの場合)について、その上のABPについて考える。

この場合には、
・送信側:ackの状況に応じた再送処理
・受信側:交番ビットによる番号の識別とack/nackの通知
の処理が、各プロセスに必要となる。

【条件】
・PUT/GETされるメッセージの抽象データ型はMSGとする(NATURAL NUMBER)。
・PUT/GETされるメッセージに交番ビット:BIT {0,1} を付与したものを送信メッセージとする。
・ACK通知の抽象データ型は、BIT {0,1} の2値とする。
・Medium1, Medium2 を lossyな通信路とする。
・各通信路から、受信側・送信側へ、転送誤りを通知するアクション {rerror, serror} を用意する。


【通信路誤りありABPのプロセス構成図】

 
spec: ABP

      +---------+ smsg!M!B +---------+ rmsg!M!B +---------+
      |         |--------->| Medium1 |--------->|         |
      |         |          |         |--------->|         |
PUT-->|  TRANS  |          +---------+  rerror  |  RECV   |--->GET
:MSG  | [TSEND] |  sack!B  +---------+          |         |    :MSG
      |   (B)   |<---------| Medium2 |  rack!B  |   (B)   |
      |         |<---------|         |<---------|         |
      +---------+  serror  +---------+          +---------+

図7.1 Alternating Bit Protocol (ABP) の構成(通信路誤り通知あり)

●通信路誤りありABPのFull LOTOS仕様

ABPの動作を記述した Full LOTOS仕様は、以下のようになる。

spec ABP の構成としては、図7.1のブロック図に示すように、

・送信側(TRANS)と受信側(RECV)プロセスが非同期並列化構成(interleaving)
・メディア1(Medium1)とメディア2(Medium2)プロセスが非同期並列化構成
・上記2つの並列化構成プロセスブロック間を、ゲートを用いて並列化構成(full-synchlonized)

といった並列化を行っている。

なお、"通信路"としての Medium1, Medium2 との間のゲートは、gate hiding してある。

【ABP.lotos】

 
specification ABP [PUT, GET] :noexit

 library ABP endlib

 behaviour

   hide smes, rmes, rerror, rack, sack, serror in
   (
      (
        TRANS [PUT, smes, sack, serror] (0 of BIT)
        |||
        RECV  [GET, rmes, rack, rerror] (0 of BIT)
      )
      |[smes, rmes, rerror, rack, sack, serror]|
      (
        Medium1 [smes, rmes, rerror]
        |||
        Medium2 [rack, sack, serror]
      )
   )

   where

(* ----------------------------------------------------------------- *)

   process TRANS [PUT, mes, ack, error] (B:BIT) : noexit :=

     PUT ?M:MSG;         (* acquiring a new message *)
        TSEND [PUT, mes, ack, error](B, M) 

   where

     process TSEND [PUT, mes, ack, error] (B:BIT, M:MSG) : noexit :=

       mes !M !B;           (* sending message M with bit B *)
          (
          ack !B;           (* control bit correct, alternating bit *)
             TRANS [PUT, mes, ack, error] (not (B))
          []
          ack !(not (B));   (* incorrect control bit, retry to send *)
             TSEND [PUT, mes, ack, error] (B, M)
          []
          error;            (* ack distorted, retry to send *)
             TSEND [PUT, mes, ack, error] (B, M)
          []
          i;                (* timeout *)
             TSEND [PUT, mes, ack, error] (B, M)
          )

     endproc

   endproc

(* ----------------------------------------------------------------- *)

   process RECV [GET, mes, ack, error] (B:BIT) : noexit :=

      mes ?M:MSG !B;          (* correct control bit *)
         GET !M;              (* output the message  *)
            ack !B;           (* sending correct ack *)
               RECV [GET, mes, ack, error] (not (B))
      []
      mes ?M:MSG !(not (B));  (* incorrect control bit *)
         ack !(not (B));      (* sending incorrect ack (nack) *)
            RECV [GET, mes, ack, error] (B)
      []
      error;                  (* message distorted *)
         ack !(not (B));      (* sending incorrect ack (nack) *)
            RECV [GET, mes, ack, error] (B)
      []
      i;                      (* timeout *)
         ack !(not (B));      (* sending incorrect ack (nack) *)
            RECV [GET, mes, ack, error] (B)

   endproc

(* ----------------------------------------------------------------- *)

   process Medium1 [input, output, error] : noexit :=

      input ?M:MSG ?B:BIT;    (* receive the message *)
         (
         output !M !B;        (* transmission correctly *)
            Medium1 [input, output, error]
         []
         error;               (* message distorted *)
            Medium1 [input, output, error]
         []
         i;                   (* lost message *)
            Medium1 [input, output, error]
         )

   endproc

(* ----------------------------------------------------------------- *)

   process Medium2 [input, output, error] : noexit :=

      input ?B:BIT;           (* receive the ack/nack message *)
         (
         output !B;           (* transmission correctly *)
            Medium2 [input, output, error]
         []
         error;               (* ack message distorted *)
            Medium2 [input, output, error]
         []
         i;                   (* lost ack message *)
            Medium2 [input, output, error]
         )

   endproc

(* ----------------------------------------------------------------- *)

endspec

送信メッセージの抽象データ型:MSGと、交番ビットの抽象データ型:BITについては、別ファイル ABP.lib で定義する。MSG型の取り得る値の範囲については、別ファイル ABP.t で定義する。

【ABP.lib】

library 
   BOOLEAN, NATURAL
endlib 

type BIT is
   sorts BIT 
   opns 0 (*! constructor *),
        1 (*! constructor *) : -> BIT
        not : BIT -> BIT
   eqns
      forall X, Y:BIT
      ofsort BIT
         not (0) = 1;
         not (1) = 0;
endtype

type MESSAGES is NATURAL renamedby
   sortnames MSG for NAT
endtype

このままでは、自然数値NATURALは、その範囲を限定しない場合、Abstract Data Typeとしての数値、0..255までの256種類の値をとる。このままではメッセージの種類が多すぎるので、ここでは、5つの種類 = {0,1,2,3,4} に限定してみる(4種類ではない)。

Abstract Data Type : NAT の範囲を制限するため、前処理を行う caesar.adtアプリケーションへの指示を与えるための ABP.t ヘッダファイルを作成・編集する。

この指示により、PUT/GETされるメッセージは、例えば、

PUT !0; GET !0; PUT !1; GET !1; .... ;PUT !4; GET !4; ....

といったシーケンスで得られることとなる。

【ABP.t ※2006/6/13改訂[caesar.adt 5.2]

 
#define CAESAR_ADT_EXPERT_T 5.2

/* This file restricts the message numbers to the integer range 0..4 */

#define ADT_ENUM_NEXT_NAT(CAESAR_ADT_0) ((CAESAR_ADT_0)++ < 4)

上記で作成した Full LOTOS版 SPROTのモデル ABP.lotos から LTS生成を行うためには、同一ディレクトリに、ABP.lib と ABP.t を置き、

(1)caesar.adtによって前処理
(2)caesarによってLTS生成

を順次実行する。

------------------------------------------------------------

$ caesar.adt ABP.lotos

$ cassar ABP.lotos

------------------------------------------------------------

実行後、トレースグラフファイル ABP.bcg を得る。

※トレースグラフ ABP.bcg はここから参照

PDFファイルはここをクリック!

図7.2 トレースグラフ ABP.bcg

途中の不可観測なアクション(smes, serrorなど)を隠すために、bcg_minアプリケーションにより、observational reductionを行い、グラフの縮小を行う。

------------------------------------------------------------

$ bcg_min -observational ABP.bcg ABP_omin.bcg

------------------------------------------------------------

実行後、縮小済みトレースグラフファイル ABP_omin.bcg を得る。

※トレースグラフ ABP_omin.bcg はここから参照

PDFファイルはここをクリック!

図7.3 縮小済みトレースグラフ ABP_omin.bcg


メッセージタイプ MSG の種類の分岐が、初期状態からアクション PUT !0,!1,!2,!3,!4を為している。n∈MSGとしたとき、PUT !n の後、必ず、GET !n が行われる様相がよく観察できる。

●ABPのobservationalな仕様(SERVICE)

ABPプロトコルを外から見る(つまり、内部のプロセスTRANS,RECV間で行われるaction smsg,sack等で何が行われているかは気にしない(hidden))ならば、TRANSへのPUTと、RECVのGETのactionの順序(SERVICE)は、常に以下のように行われることが期待されている。

SERVICE = PUT;GET;PUT;GET;… = *[PUT;GET]

PUT/GETされるメッセージの抽象データ型はMSGとする(NATURAL NUMBER)。このとき、外部からみた挙動(SERVICE)を記述した Full LOTOS仕様は、以下のようになる。

【SERVICE.lotos】

 
specification SERVICE [PUT, GET] :noexit

 library SERVICE endlib

 behaviour

   SERVICE_BODY [PUT, GET]

   where

(* ----------------------------------------------------------------- *)

   process SERVICE_BODY [PUT, GET] : noexit :=

      PUT ?M:MSG;               (* acquiring a new message *)
         GET !M;                (* output the message      *)
            SERVICE_BODY [PUT, GET]

   endproc

(* ----------------------------------------------------------------- *)

endspec

SERVICEについても、SPROT.lib, SPROT.t と同様のAbstract Data Type用の定義ファイルを設置する(SERVICE.lib, SERVICE.t)。そして、caesar.adt + caesarによって、SERVICE.bcg を得る。

●等価性の検証例

最後に、bcg_cmpを用いて、ABP と SERVICEのobs. equivalency検証を行う。

------------------------------------------------------------

$ bcg_cmp -observational ABP.bcg SERVICE.bcg
TRUE

------------------------------------------------------------

これにより、メッセージタイプ:MSGを用いたFull LOTOS版ABPにおいても、SERVICE仕様との間で

(ABP == SERVICE) → TRUE

であることが確かめられた。この性質は、先の送信メッセージ型:MSGのrestriction(!0から!4の5種類)に限定されるものではなく、MSGが自然数全体をなすような抽象データ型であったとしても、常に満たされる性質なのである(重要)。

●練習問題7-1

[1] ABP.lotos について、caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察せよ。(bcg_infoアプリケーションを用いてデッドロック状態の有無を確認せよ)

[2] ABP.bcgを obs. reduction した ABP_omin.bcgを、bcg_minアプリケーションを用いて生成せよ。また、そのトレースグラフを観察せよ。

[3] (ABP == SERVICE) → TRUE を bcg_cmpアプリケーションを用いて確かめよ。

★レポート課題2

<課題>
7.2節にて取り挙げた、交番ビットプロトコル(Alternating Bit Protocol (ABP))の"通信路誤りあり"のFull LOTOS版プロセスモデル(ABP.lotos)について、以下の<演習手順>に示す拡張を行ったモデル ABP4.lotos を Full LOTOSで記述し、CADP toolbox によってLTS生成を行いなさい。
また、生成したLTSのobs. reduced を行いなさい。

提出するファイルは以下の通り(tar+gzipでアーカイブした後、提出)。

・LOTOSファイル:ABP4.lotos
・プロセスグラフ生成に必要な他のファイル(*.lib, *.tなど)
・LTSプロセスグラフファイル:ABP4.bcg
・obs. reducedしたプロセスグラフファイル:ABP4_omin.bcg


<演習手順>

(1)交番ビットを、現在の2値 {0,1} から、4値 {00,01,10,11} へ拡張しなさい。bit alternatingの順序は、00-->01-->10-->11-->00....とする。拡張した抽象データ型のライブラリファイルはABP4.libとせよ。(ヒント:NATURALには、関数Succ()が定義されている)。

(2)(1)の仕様を盛り込んだ、ABP4.lotosを作成し、caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察しなさい。(メッセージは5種類。デッドロック状態の有無を確認せよ)

(3)ABP4.bcgをobs. reduction した ABP4_omin.bcgを、bcg_minアプリケーションを用いて生成せよ。また、そのトレースグラフを観察せよ。

(4)(ABP4 == SERVICE) → TRUE を bcg_cmpアプリケーションを用いて確かめなさい。


<レポート提出の手順>
(1)提出するファイルは以下の通り。

・LOTOSファイル:ABP4.lotos
・プロセスグラフ生成に必要な他のファイル(*.lib, *.tなど)
・LTSプロセスグラフファイル:ABP4.bcg
・obs. reducedしたプロセスグラフファイル:ABP4_omin.bcg

(2)以下のいずれかの形式でarchiveし、一本のファイルにまとめなさい。
アーカイブのファイル名は ABP4.zip あるいは ABP4.tar.gz とする。

※提出可能形式
(a) tar+gzip形式 (*.tar.gz) 例:UNIXコマンドの tar + gzip を用いる
(b) ZIP圧縮形式 (*.zip) 例:WinZipなど


(3)eALPSの、レポート提出システムからアップロードし、提出しなさい。 

wasaki@cs.shinshu-u.ac.jp
Copyright(c) Katsumi Wasaki. All rights reserved.