■設計例
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が返るのを待って、最初に戻る。
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上の、レポート提出システムからアップロードし、提出しなさい。
|