プロトコル検証の例(ABP) | ||||||
■プロトコル検証の例(ABP) 1. Alternating Bit Protocol (ABP) 3. ABPのobservationalな仕様(SERVICE) 2015年4月22日 12:02
|
Full LOTOSによるAlternating Bit Protocol (ABP)を記述する。それについて、外部から見た可観測な値の挙動(SERVICE)との、observational な等価性について検証を行う。 この章で学習する内容は以下の4つである。最後に演習問題4を与える。 1. Alternating Bit Protocol (ABP) ●Alternating Bit Protocol (ABP)1.1 概要交番ビットプロトコル(Alternating Bit Protocol (ABP))とは、転送誤りを起こすような通信路を挟んで、片方向のメッセージ転送を行う際、送信側はメッセージに、そのメッセージの番号を交番ビットとして付与し、受信側はメッセージに付与された交番ビットと、受信側が期待した番号との比較を行うことで、受信成功(ack)あるいは受信誤り(nack)を送信側へ伝え、送信側からの再送処理を行うものである。 送信側(TRANS)から受信側(RECV)へのメッセージ送信時には、以下のケースがある。 (TR1) 送信されたメッセージは、正常に受信側へ届く。 受信側(RECV)から送信側(TRANS)へのack/nack通知時には、以下のケースがある。 (RT1) 通知した ack は、正常に送信側へ届く。 1.2 通信路誤りあり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仕様は、以下のようになる。
spec ABP の構成としては、図7.1のブロック図に示すように、
・送信側(TRANS)と受信側(RECV)プロセスが非同期並列化構成(interleaving)
・メディア1(Medium1)とメディア2(Medium2)プロセスが非同期並列化構成
・上記2つの並列化構成プロセスブロック間を、ゲートを用いて並列化構成(full-synchlonized)
といった並列化を行っている。
なお、"通信路"としての Medium1, Medium2 との間のゲートは、gate hiding してある。
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 で定義する。
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; ....
といったシーケンスで得られることとなる。
#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 を得る。
図7.2 トレースグラフ ABP.bcg
途中の不可観測なアクション(smes, serrorなど)を隠すために、bcg_minアプリケーションにより、observational reductionを行い、グラフの縮小を行う。
------------------------------------------------------------
$ bcg_min -observational ABP.bcg ABP_omin.bcg
------------------------------------------------------------
実行後、縮小済みトレースグラフファイル ABP_omin.bcg を得る。
図7.3 縮小済みトレースグラフ ABP_omin.bcg
メッセージタイプ MSG の種類の分岐が、初期状態からアクション PUT !0,!1,!2,!3,!4を為している。n∈MSGとしたとき、PUT
!n の後、必ず、GET !n が行われる様相がよく観察できる。
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仕様は、以下のようになる。
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が自然数全体をなすような抽象データ型であったとしても、常に満たされる性質なのである(重要)。
[1] ABP.lotos について、caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察せよ。(bcg_infoアプリケーションを用いてデッドロック状態の有無を確認せよ)
[2] ABP.bcgを obs. reduction した ABP_omin.bcgを、bcg_minアプリケーションを用いて生成せよ。また、そのトレースグラフを観察せよ。
[3] (ABP == SERVICE) → TRUE を bcg_cmpアプリケーションを用いて確かめよ。
<課題>
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.