Full LOTOS | ||||||||||||||||
■Full LOTOS 3. Full LOTOS版 "Simple Protocol" 2015年4月22日 11:59
|
プロセス代数のパートのみをサポートするのがBasic LOTOS である。ACT ONE と呼ばれる抽象データ型による定義(ADT : Abstract Data Type)も含むような仕様は Full LOTOS 、あるいは単に LOTOS仕様 と呼ばれる。ADTとCADP toolboxで用いられるADTライブラリについて取り上げる。次に、具体的なFull LOTOS仕様の記述について、PBLプロセスをFull LOTOSへ拡張した仕様を考え、実際にtoolboxでLTS生成を行ってみる。更に、Full LOTOSにより、簡単なプロトコルと、誤りなしAlternating Bit Protocol (ABP)を記述する。 この章で学習する内容は以下の4つである。最後に演習問題3を与える。 1. Abstract Data Type (ADT) ●Abstract Data Type (ADT)先述の通り、LOTOSは次の2つのパートから構成されている。 LOTOSにおけるこれら2つのパートは、お互いに独立しており、関連性が無い。 プロセス代数のパートのみをサポートするのがBasic LOTOS である。2つ目の定義も含むような仕様は Full LOTOS 、あるいは単に LOTOS仕様 と呼ばれる。 1.1 ACT ONE 抽象データ型(ADT)の仕様 1.1 ACT ONE 抽象データ型(ADT)の仕様ここで ACT ONE に関する詳細な解説を再掲するのは適切でない。 The
Formal Specification Language LOTOS: A Course for Users(local copy) chapter 4. Data Typing 1.2 caesar.adtアプリケーションによるADTのサポートcaesar.adt ユーザマニュアル Questions specific to CAESAR.ADT Predefined ADT library(CADP) 1.3 ADTライブラリ ・BOOLEAN ●Full LOTOSAbstract Data Typeに対する前処理は、 caesar.adtアプリケーションによって行われる。Full LOTOS仕様で定義・導入された種々のデータ型について、これを解析することによって、先述の caesar アプリケーションによるLTS生成を可能とするものである。 2.1 caesar.adtによる抽象データ型の解決 2.1 caesar.adtによる抽象データ型の解決caesarアプリケーションによって実際のLTS生成を行うためには、Abstract Data Typeによって記述された種々のデータ型(Boolean型、自然数型、ビット型など)について、具体的な抽象データとして見做すことで、例えば以下に説明する型付きguardの記述を、Basic LOTOSのnon-deterministic choiceへ変換する必要がある。 この解析と変換のために、caesar.adtアプリケーションを使用する。 caesar.adt ユーザマニュアル 2.1.1 抽象データ型解決の実際(PBL2)Boolean型のADTを用いた例として、先述のプッシュボタンのBasic-LOTOSによる記述例(PBL)の出力を、true/falseの2値出力に拡張することを考えてみる。 ボタンが1回押される(push)毎に、出力(output)メッセージとして true/falseを交互に発信するようにすればよい。
図6.1 PBL2 の構成 Boolean抽象データ型のライブラリファイルは BOOLEAN.lib である。 Full LOTOS仕様として、当該 specificationブロックの先頭で、このライブラリを使用することを宣言する。 "出力値"としてのメッセージ true/false は、BOOLEAN.lib の BOOL型sortsとして定義済みである。実際にoutputの出力値として用いる際には、!(true of BOOL) などとして、BOOL型sortsの "true" という値であることを明示するとよい。 outputゲートへの"出力"メッセージ、いいかえれば outputアクションが生起した場合に伴われるvalue expressionの記述は、型定義済みのsort
name を、!の後に続けて書けばよい。下記の例では、!true あるいは !(true of BOOL) を"出力する"、と見做すことができる。
2.1.2 caesar.adt + caesar を用いたLTS生成上記の PBL2.lotos を、caesar.adt ならびに caesar を連携して使用し、最終的なLTSを得る。 ---------------------------------- $ caesar.adt PBL2.lotos $ caesar -bcg PBL2.lotos ---------------------------------- 2.2 同期化とデータパッシングの考え方(guard expression)次に、上述の PBL_BODY の出力値(true/false)に応じて、実際の電灯のオン/オフを制御するようなプロセス LIGHT を接続することを考えてみる。 プロセス LIGHT の定義としては、入力メッセージとして true/falseというBOOL型の値に応じて、出力メッセージ on/off を発信するようにすればよい。
図6.2 PBL3 の構成 全体の仕様 PBL3 は、PBL_BODYとLIGHTを msgゲートで同期化したものとなっている。このmsgゲートの値に応じて、LIGHTプロセス側では on あるいは off のメッセージ出力を行えばよい。 "入力値"としてのメッセージ true/false は、BOOLEAN.lib の BOOL型sortsとして定義済みである。実際に msg の入力値を利用する際には、内部変数としての output へBOOL型の入力値をセットするように記述を行う。具体的には、msg ?output:BOOL などとして、BOOL型sortsの値を代入することを指示する。
プロセス PBL_BODYとLIGHT は、ゲート msg によって同期化されている。前者は msgに対して"出力"を行い、後者はmsgから"入力"を期待している。 この仕様を、ゲートmsgを利用した"メッセージパッシング"であると捉えると、プロセスPBL_BODYから、ランプのオン/オフの指示が、ボタンpushのアクションの度に、true/falseという値をともなったメッセージとして送出されている様子が見て取れる。LIGHT側からのackは仕様に無いので、push動作と実際のon/offのアクションは遅れがあることも仕様として盛り込まれている。(もし、ゲートmsgの通信路がlossyであれば、時々、電灯の点滅動作は異常となるであろう) 他方、ゲートmsgによる同期化(rendezvous)であると捉えると、これは単に PBL_BODY側でpushボタンが押されるのを、LIGHT側は待っている、と見ることができる。抽象データ型の導入前の仕様では、ここまでの同期化が盛り込まれるはずである。 2.3 Processes with values引き続いて、上述の PBL_BODY の出力値(true/false)の"変化"に応じて、実際の電灯のオン/オフを制御するようなプロセス LIGHT2 を接続することを考えてみる。 今回は、msgの状態変化 false <=> true といったedgeトリガが生起した場合に、電灯のオン/オフの出力変化を行う、という仕様とする。ちょうど、pushアクションに対するフリップフロップが、LIGHT2プロセスに実装されているようである。
図6.3 PBL4 の構成 プロセス LIGHT2 の定義として新たに必要な機能は、プロセスの内部で、1ステップ前のmsgメッセージ値 を保存しておく「状態記憶」の記述である。 このために、プロセス LIGHT2 のインスタンス生成・呼び出しを行う際、現在の状態を含めてプロセスを起動する「値付きプロセス」の定義を行う。 specificationブロックでのプロセス LIGHT2 のインスタンス生成時には、状態値 status を false に初期化する必要がある。次に、msgからのメッセージ入力を検査し、状態変化 false <=> true といったedgeトリガが生起した場合に、状態値 statusを、true <=-> false へ交番するため、新たな値を含めたプロセス呼び出しを行う。
<付記>
●Full LOTOS版 "Simple Protocol"5.1節にてBasic-LOTOSで記述した、簡単なプロトコル(Simple Protocol)について、これの Full LOTOS版 を作成してみよう。 3.1 伝達可能メッセージの種類を導入したSPROTの仕様 3.1 伝達可能メッセージの種類を導入したSPROTの仕様入出力チャンネル PUT/GET、ならびに通信チャンネル channel は、伝達可能なメッセージのとして MSG というAbstract Data Typeをとるものとする。 片方向のメッセージ転送を行う簡単なプロトコル(SPROT)のモデルについて、以下に示す。 【条件】
図6.4 Simple Protocol の構成 3.2 Full LOTOS版 SPROTの仕様SPROTの動作を記述した Full LOTOS仕様は、以下のようになる。 メッセージタイプ:MSGについては、別ファイル SPROT.lib で定義する。MSG型の取り得る値の範囲については、別ファイル SPROT.t で定義する。これらのAbstract Data Typeに対する前処理は、 caesar.adtアプリケーションによって行われる。
次に、Abstract Data Typeを導入し、伝達可能なメッセージの型である MSG を 自然数値:NATURAL と見做したい。このため、Pre-definedなライブラリである BOOLEANとNATURALを導入し、メッセージタイプ MSG が、NATURALと同等である(renamedby)と定義するためのライブラリファイル SPROT.lib を作成・編集する。
このままでは、自然数値NATURALは、その範囲を限定しない場合、Abstract Data Typeとしての数値、0..255までの256種類の値をとる。このままではメッセージの種類が多すぎるので、ここでは、4つの数値 = {0,1,2,3} に限定してみる。 Abstract Data Type : NAT の範囲を制限するため、前処理を行う caesar.adtアプリケーションへの指示を与えるための SPROT.t ヘッダファイルを作成・編集する。
3.3 Full LOTOS版 SPROTのLTS生成・トレースグラフの観察上記で作成した Full LOTOS版 SPROTのモデル SPROT.lotos から LTS生成を行うためには、同一ディレクトリに、SPROT.lib と SPROT.t を置き、 (1)caesar.adtによって前処理 を順次実行する。 ------------------------------------------------------------ $ caesar.adt SPROT.lotos $ cassar SPROT.lotos ------------------------------------------------------------ 実行後、トレースグラフファイル SPROT.bcg を得る。 ※トレースグラフ SPROT.bcg はここから参照(PDF) 図6.5 トレースグラフ SPROT.bcg 途中の不可観測なアクション(channel, ack)を隠すために、bcg_minアプリケーションにより、observational reductionを行い、グラフの縮小を行う。 ------------------------------------------------------------ $ bcg_min -observational SPROT.bcg SPROT_omin.bcg ------------------------------------------------------------ 実行後、縮小済みトレースグラフファイル SPROT_omin.bcg を得る。 ※トレースグラフ SPROT_omin.bcg はここから参照(PDF) 図6.6 縮小済みトレースグラフ SPROT_omin.bcg
3.4 SPROTのobservationalな仕様(SERVICE)このプロトコルを外から見る(つまり、内部のプロセスPSEND,PRECV間で行われるaction msg,ackで何が行われているかは気にしない(hidden))ならば、SPROTへのPUTとGETのactionの順序(SERVICE)は、常に以下のように行われることが期待されている。 SERVICE = PUT;GET;PUT;GET;… = *[PUT;GET] Abstract Data Type : MSG を用いた、Full LOTOS版のSERVICEの仕様は以下のようになる。
SERVICEについても、SPROT.lib, SPROT.t と同様のAbstract Data Type用の定義ファイルを設置する(SERVICE.lib, SERVICE.t)。そして、caesar.adt + caesarによって、SERVICE.bcg を得る。
------------------------------------------------------------ $ bcg_cmp -observational SPROT.bcg SERVICE.bcg ------------------------------------------------------------ これにより、メッセージタイプ:MSGにおいても、この2つの仕様は (SPROT == SERVICE) → TRUE であることが確かめられた。
●Full LOTOS版 "通信路誤り無しABP"通信路誤りが無い場合の交番ビットプロトコル(Alternating Bit Protocol (ABP))について、そのFull LOTOS版を考える。 通信路誤り無しABPのFull LOTOS仕様【条件】
図6.7 Alternating Bit Protocol (ABP) の構成(通信路誤りなし) ABP の動作を記述した Full LOTOS仕様は、以下のようになる。
先のSPROTの場合と同様、Abstract Data Typeを導入し、伝達可能なメッセージの型である MSG と、交番ビットである BIT を定義する。 Pre-definedなライブラリである BOOLEANとNATURALを導入し、メッセージタイプ MSG を、NATURALと同等である(renamedby)とし、さらに、交番ビットのための BIT というデータ型を定義するためのライブラリファイル ABP.lib を作成・編集する。
SPROT同様、NAT の範囲を制限するため、ABP.t ヘッダファイルを作成・編集する。
●練習問題6-1[1] 6.3節で説明した SPROTとSERVICE について、caesar.adt + caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察せよ。 [2] (SPROT == SERVICE) → TRUE を bcg_cmpアプリケーションを用いて確かめよ。 [3] 6.4節で説明した ABP について、caesar.adt + caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察せよ。 [4] (ABP == SERVICE) → TRUE を bcg_cmpアプリケーションを用いて確かめよ。 ★レポート課題3<課題> 提出するファイルは以下の通り(tar+gzipでアーカイブした後、提出)。 <演習手順> (1)6.4節で作成したABPの交番ビットについて、現在の2値 {0,1} から、4値 {00,01,10,11} へ拡張しなさい。bit alternatingの順序は、00-->01-->10-->11-->00....とする。拡張した抽象データ型のライブラリファイルはABP4.libとせよ。(ヒント:NATURALには、関数Succ()が定義されている)。 (2)ABP4 について、caesar.adt + caesarアプリケーションを用いてLTS生成を行い、そのトレースグラフを観察しなさい。(メッセージは4種類。デッドロック状態の有無を確認) (3)(ABP4 == SERVICE) → TRUE を bcg_cmpアプリケーションを用いて確かめなさい。 (4)obs. reducedしたプロセスグラフファイル:ABP4_omin.bcg を bcg_min を用いて生成しなさい。また、そのトレースグラフを観察しなさい。 <レポート提出の手順> ・LOTOSファイル:ABP4.lotos (2)以下のいずれかの形式でarchiveし、一本のファイルにまとめなさい。 ※提出可能形式 |
|||||||||||||||
wasaki@cs.shinshu-u.ac.jp |