設計例

■設計例

1. 簡単なプロトコル(Simple Protocol)

2. Alternating Bit Protocol (ABP)

3. 通信路誤り無しの場合

4. 通信路誤りありの場合

練習問題5-1

参考資料・リンク集

2015年4月22日 11:52

 

Basic LOTOS を用いて簡単なプロトコルと、Alternating Bit Protocol (ABP)を記述する。それらについて、外部から見た可観測な値の挙動(SERVICE)との、observational な等価性について検証を行う。なお、ABPについては、その通信路がlossyでない場合と、lossyな場合の両方について記述をおこなってみる。

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

1. 簡単なプロトコル(Simple Protocol)
2. Alternating Bit Protocol (ABP)
3. 通信路誤り無しの場合
4. 通信路誤りありの場合

練習問題5-1

●簡単なプロトコル(Simple Protocol)

1.3節にて取り上げた、簡単なプロトコル(Simple Protocol)について、これを Basic LOTOS 仕様で記述してみよう。片方向のメッセージ転送を行う簡単なプロトコル(SPROT)のモデル化について、以下に再掲する。

1.1 SPROTの仕様
1.2 SPROTのBasic LOTOSによる設計
1.3 SPROTのobservationalな仕様(SERVICE)
1.4 SERVICEのBasic LOTOSによる設計


1.1 SPROTの仕様

SPROTプロトコルは、2つの送受信プロセス:PSEND, PRECV から構成される。

PSENDは、入力PUTをメッセージ転送チャンネル msg を使って PRECVへ送る。
PRECVは、チャンネル msg から送られてきたメッセージを出力GETとし、ackを返す。
PSENDは、ackを受信したら、次のメッセージ転送手順を開始する。

spec: SPROT
      +---------+   msg    +---------+
| |--------->| |
PUT-->| PSEND | | PRECV |-->GET
| |<---------| |
+---------+ ack +---------+

図4.1 Simple Protocol の構成

メッセージ転送チャンネル msg,ack は、必ず正常に動作していると仮定する。

※PSEND, PRECVの定義と並列化

PSENDは、入力PUTをmsgを使って送信し、ackが返るのを待って、最初に戻る。

PSEND = *[PUT;msg;ack]

PRECVは、msgの受信を待ち、送られてきたら出力GETとし、ackを返し、最初に戻る。

PRECV = *[msg;GET;ack]

図4.1に示すように、2つのプロセスは msg, ack で同期を取りながら、並列動作を行っている。PSEND, PRECV を合成した SPROT を書くと以下のようになる。

SPROT =  PSEND || PRECV
= *[PUT;msg;ack]
|[msg,ack]|
*[msg;GET;ack]

1.2 SPROTのBasic LOTOSによる設計

SPROTの動作を記述した Basic LOTOS仕様は、以下のようになる。
なお、"通信路"としての msg, ack の両アクションは、gate hiding してある。

もし、トレースグラフにおいて、アクション msg, ack を観察したければ、LOTOSファイル中の hide msg,ack in の行をコメントアウトし、specification のアクション列の引数として、msg, ack を追加すればよい。

【SPROT_spec.lotos】


specification SPROT_spec [PUT,GET] :noexit

  behaviour

    hide msg,ack in
    (
      PSEND [PUT,msg,ack]
      |[msg,ack]|
      PRECV [msg,GET,ack]
    )

where

   process PSEND [PUT,msg,ack] :noexit :=
     PUT; msg; ack;
       PSEND[PUT,msg,ack]
   endproc

   process PRECV [msg,GET,ack]:noexit:=
     msg; GET; ack;
       PRECV[msg,GET,ack]
   endproc

endspec
			

 


1.3 SPROTのobservationalな仕様(SERVICE)

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

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

 


1.4 SERVICEのBasic LOTOSによる設計

SPROTの外部からみた挙動(SERVICE)を記述した Basic LOTOS仕様は、以下のようになる。

【SPROT_service.lotos】

 
specification SPROT_service [PUT,GET] :noexit

  behaviour

    SERVICE [PUT,GET]

where

   process SERVICE [PUT,GET] :noexit :=
     PUT; GET;
       SERVICE [PUT,GET]
   endproc

endspec
           

 

●Alternating Bit Protocol (ABP)

交番ビットプロトコル(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上で消失し、送信側へ届かない。

      +---------+  msg*    +---------+  msg**   +---------+
      |         |--------->| Medium1 |--------->|         |
PUT-->|  TRANS  |          +---------+          |  RECV   |--->GET
      |         |  ack**   +---------+  ack*    |         |
      |         |<---------| Medium2 |<---------|         |
      +---------+          +---------+          +---------+

図4.2 Alternating-Bit Protocol (ABP) の各プロセスの接続図

●通信路誤り無しの場合

まず最初に、通信路誤りが無い場合(i.e. 通信路に相当するlossyなMediumがない場合)について、その上のABPについて考える。


3.1 通信路誤り無しABPのBasic LOTOS仕様

【条件】
・PUT/GETされるメッセージに交番ビット 0/1 を付与した、送信メッセージの種類は
 {msg0, msg1} の2種類とする。
・ACK通知の種類は、{ack0, ack1} の2種類とする。
・lossyな通信路はないので、再送処理は行う必要がない。


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

spec: ABP_reliable

      +---------+   msg0/1 +---------+
      |         |--------->|         |
PUT-->|  TRANS  |          |  RECV   |-->GET
      |         |<---------|         |      
      +---------+   ack0/1 +---------+

図4.3 Alternating Bit Protocol (ABP) の構成(通信路誤り無し)

ABP_reliable の動作を記述した Basic LOTOS仕様は、以下のようになる。
なお、"通信路"としての msg0/1, ack0/1 のアクションは、gate hiding してある。

【ABP_reliable.lotos】

 
specification ABP_reliable [PUT,GET] : noexit

  behaviour

    hide msg0,msg1,ack0,ack1 in
    (
      TRANS [PUT,msg0,msg1,ack0,ack1]
      |[msg0,msg1,ack0,ack1]|
      RECV  [GET,msg0,msg1,ack0,ack1]
    )

  where

    process TRANS [PUT,msg0,msg1,ack0,ack1]: noexit:=

      PUT;      (* get next message to be sent *)
        msg0;   (* send current message + control bit 0 *)
          ack0; (* wait to get ack0 *)
            TRANS [PUT,msg1,msg0,ack1,ack0]  (* alternating bit *)

    endproc

    process RECV [GET,msg0,msg1,ack0,ack1]: noexit:=

      msg0;     (* wait to receive message + control bit 0 *)
        GET;    (* output the message *)
          ack0; (* send ack0 *)
            RECV [GET,msg1,msg0,ack1,ack0]   (* alternating bit *)

    endproc

endspec

 


3.2 ABPのobservationalな仕様(SERVICE)

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

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

この外部からみた挙動(SERVICE)を記述した Basic LOTOS仕様は、以下のようになる。(先の SPROT_service の仕様と同一)

【ABP_service.lotos】

 
specification ABP_service [PUT,GET] :noexit

  behaviour

    SERVICE [PUT,GET]

where

   process SERVICE [PUT,GET] :noexit :=
     PUT; GET;
       SERVICE [PUT,GET]
   endproc

endspec

 

●通信路誤りありの場合

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

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

【条件】
・PUT/GETされるメッセージに交番ビット 0/1 を付与した、送信メッセージの種類は
 {msg0, msg1} の2種類とする。
・ACK通知の種類は、{ack0, ack1} の2種類とする。
・Medium1, Medium2 を lossyな通信路とする。
・各通信路から、受信側・送信側へ、転送誤りを通知するアクション {rerror, serror} を追加する。


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

 
spec: ABP_unreliable

      +---------+ smsg0/1  +---------+ rmsg0/1  +---------+
      |         |--------->| Medium1 |--------->|         |
      |         |          |         |--------->|         |
PUT-->|  TRANS  |          +---------+ rerror   |  RECV   |--->GET
      | [TSEND] | sack0/1  +---------+          |         |
      |         |<---------| Medium2 | rack0/1  |         |
      |         |<---------|         |<---------|         |
      +---------+ serror   +---------+          +---------+

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

ABP_unreliable の動作を記述した Basic LOTOS仕様は、以下のようになる。
なお、"通信路"としての Medium1, Medium2 との間のアクションは、gate hiding してある。

【ABP_unreliable.lotos】

 
specification ABP_unreliable [PUT,GET] :noexit

 behaviour

   hide smes0, smes1, rmes0, rmes1, rerror, 
        rack0, rack1, sack0, sack1, serror in
   (
      (
        TRANS [PUT, smes0, smes1, sack0, sack1, serror]
        |||
        RECV  [GET, rmes0, rmes1, rack0, rack1, rerror]
      )
      |[smes0, smes1, rmes0, rmes1, rerror, 
        rack0, rack1, sack0, sack1, serror]|
      (
        Medium [smes0, smes1, rmes0, rmes1, rerror]
        |||
        Medium [rack0, rack1, sack0, sack1, serror]
      )
   )

   where

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

   process TRANS [PUT, mes0, mes1, ack0, ack1, error] : noexit :=

     PUT;         (* acquiring a new message *)
       TSEND [PUT, mes0, mes1, ack0, ack1, error]

   where

     process TSEND [PUT, mes0, mes1, ack0, ack1, error] : noexit :=

       mes0;             (* sending a 0-message *)
         (
          ack0;          (* control bit correct, alternating bit *)
            TRANS [PUT, mes1, mes0, ack1, ack0, error]
          []
          ack1;          (* incorrect control bit, retry to send *)
            TSEND [PUT, mes0, mes1, ack0, ack1, error]
          []
          error;         (* ack distorted, retry to send *)
            TSEND [PUT, mes0, mes1, ack0, ack1, error]
         )

     endproc

   endproc

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

   process RECV [GET, mes0, mes1, ack0, ack1, error] : noexit :=

     mes0;               (* correct control bit *)
       GET;              (* output the message  *)
         ack0;           (* sending correct ack *)
           RECV [GET, mes1, mes0, ack1, ack0, error]
     []
     mes1;               (* incorrect control bit *)
       ack1;             (* sending incorrect ack (nack) *)
         RECV [GET, mes0, mes1, ack0, ack1, error]
     []
     error;              (* message distorted *)
       ack1;             (* sending incorrect ack (nack) *)
         RECV [GET, mes0, mes1, ack0, ack1, error]

   endproc

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

   process Medium [in0, in1, out0, out1, error] : noexit :=

     in0;            (* send 0-message *)
       (
        out0;        (* transmission correct *)
          Medium [in0, in1, out0, out1, error]
        []
        error;       (* message distorted *)
          Medium [in0, in1, out0, out1, error]
       )
     []
     Medium [in1, in0, out1, out0, error] (* alternating channel *)

   endproc

endspec

 

 

●練習問題5-1

[1] SPROT_spec, SPROT_service について、caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察せよ。

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

[3] ABP_reliable について、caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察せよ。

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

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

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

[7] ABP_unreliableにおいて、誤りのある通信路とは、実のところ、Medium の「メッセージ転送誤り」だけをモデル化しており、メッセージ消失に伴うタイムアウト処理は考慮されていない。Mediumは、常に out0/1 あるいは error をアクションとして有する。本来は、in0/1 アクションの後、out0/1もerrorも生起しないケース(メッセージ消失)をモデル化すべきである。このケースを盛り込んだプロセスMedium を作成せよ。次に、TSEND/RECVプロセスについては、各Mediumから常にactionが来ないケースがあるので、これは internal action を用いて、メッセージ消失時のタイムアウト処理を仕様に盛り込むべきである。以上の「メッセージ消失」をモデル化した Medium/TSEND/RECVの各プロセスを作成し、ABP_serviceとのobs. equivalencyを確認せよ。

★レポート課題2

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

提出するファイルは以下の通り(tar+gzipでアーカイブした後、提出)。
・LOTOSファイル:ABP4_spec.lotos
・プロセスグラフ生成に必要な他のファイル(*.lib, *.tなど)
・LTSプロセスグラフファイル:ABP4_spec.bcg
・obs. reducedしたプロセスグラフファイル:ABP4_spec_omin.bcg


<演習手順>

(1)ABP_unreliableのTSEND と RECV で、Mediumのメッセージ消失に伴うタイムアウト処理を考慮した実装(練習問題5-1[7])を行いなさい。

(2)次に、交番ビットを、現在の2値 {0,1} から、4値 {00,01,10,11} へ拡張しなさい。bit alternatingの順序は、00-->01-->10-->11-->00....とする。

(3)上記(1)(2)を仕様とした、lossyな通信路 Medium を有するような ABP4_spec.lotos を作成しなさい。

(4)ABP4_spec について、caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察しなさい。(デッドロック状態の有無を確認)

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

(6)obs. reducedしたプロセスグラフファイル:ABP4_spec_omin.bcg を bcg_min を用いて生成しなさい。また、そのトレースグラフを観察しなさい。


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

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

(2)以下のいずれかの形式でarchiveし、一本のファイルにまとめなさい。
アーカイブのファイル名は ABP4_spec.zip あるいは ABP4_spec.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.