Full LOTOS

■Full LOTOS

1. Abstract Data Type (ADT)

2. Full LOTOS

3. Full LOTOS版 "Simple Protocol"

4. Full LOTOS版 "通信路誤り無しABP"

参考資料・リンク集

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)
2. Full LOTOS
3. Full LOTOS版 "Simple Protocol"
4. Full LOTOS版 "通信路誤り無しABP"

練習問題6-1

●Abstract Data Type (ADT)

先述の通り、LOTOSは次の2つのパートから構成されている。
・1つ目は、CCS(Milner's Calculus of Communicating Systems)+CSP(Hoare's Communicating Sequential Processes)に基づいて構成されるプロセス代数による定義である。
・2つ目は、ACT ONE と呼ばれる抽象データ型による定義(abstract data type)である。

LOTOSにおけるこれら2つのパートは、お互いに独立しており、関連性が無い。
プロセス代数仕様のパートは、各モジュールの動的振る舞いについて定義する。
他方、抽象データ型のパートは、各モジュールにおけるデータ構造とモジュール間通信(メッセージパッシング)について定義する。

プロセス代数のパートのみをサポートするのがBasic LOTOS である。2つ目の定義も含むような仕様は Full LOTOS 、あるいは単に LOTOS仕様 と呼ばれる。

1.1 ACT ONE 抽象データ型(ADT)の仕様
1.2 caesar.adtアプリケーションによるADTのサポート
1.3 ADTライブラリ


1.1 ACT ONE 抽象データ型(ADT)の仕様

ここで ACT ONE に関する詳細な解説を再掲するのは適切でない。
詳しくは、以下のドキュメントを見るように。

The Formal Specification Language LOTOS: A Course for Users(local copy)
Kenneth J. Turner
Technical Report, Dept of Computer Science and Mathematics, University of Stirling, Scotland August 1989, 87 pages

chapter 4. Data Typing
page.52 -- 66


1.2 caesar.adtアプリケーションによるADTのサポート

caesar.adt ユーザマニュアル
http://www.inrialpes.fr/vasy/cadp/man/caesar.adt.html

Questions specific to CAESAR.ADT
http://www.inrialpes.fr/vasy/cadp/faq.html#7

Predefined ADT library(CADP)
Boolean, NaturalNumber, Natural, Bit, .....
$CADP/lib/*.lib


1.3 ADTライブラリ

BOOLEAN
NATURAL (NATURALNUMBER)
BIT
BITSTRING

●Full LOTOS

Abstract Data Typeに対する前処理は、 caesar.adtアプリケーションによって行われる。Full LOTOS仕様で定義・導入された種々のデータ型について、これを解析することによって、先述の caesar アプリケーションによるLTS生成を可能とするものである。

2.1 caesar.adtによる抽象データ型の解決
2.2 同期化とデータパッシングの考え方(guard expression)
2.3 Processes with values


2.1 caesar.adtによる抽象データ型の解決

caesarアプリケーションによって実際のLTS生成を行うためには、Abstract Data Typeによって記述された種々のデータ型(Boolean型、自然数型、ビット型など)について、具体的な抽象データとして見做すことで、例えば以下に説明する型付きguardの記述を、Basic LOTOSのnon-deterministic choiceへ変換する必要がある。

この解析と変換のために、caesar.adtアプリケーションを使用する。

caesar.adt ユーザマニュアル
http://www.inrialpes.fr/vasy/cadp/man/caesar.adt.html

2.1.1 抽象データ型解決の実際(PBL2)

Boolean型のADTを用いた例として、先述のプッシュボタンのBasic-LOTOSによる記述例(PBL)の出力を、true/falseの2値出力に拡張することを考えてみる。

ボタンが1回押される(push)毎に、出力(output)メッセージとして true/falseを交互に発信するようにすればよい。

 
spec: PBL2

        +----------+
        |          |
push--->| PBL_BODY |--->output:BOOL
        |          |
        +----------+

図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) を"出力する"、と見做すことができる。

【PBL2.lotos】

 
specification PBL2 [push,output] : noexit

  library BOOLEAN endlib 

  behaviour

    PBL_BODY[push,output]

  where

    process PBL_BODY [push,output] : noexit :=

       push; output !(true of BOOL);
       push; output !(false of BOOL);
          PBL_BODY[push,output]

    endproc

endspec

 

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 を発信するようにすればよい。

 
spec: PBL3

        +----------+          +---------+
        |          |          |         |---->on
push--->| PBL_BODY |--------->|  LIGHT  |
        |          | msg:BOOL |         |---->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の値を代入することを指示する。

【PBL3.lotos】

 
specification PBL3 [push,on,off] : noexit

  library BOOLEAN endlib 

  behaviour

    hide msg in

    PBL_BODY[push,msg]
    |[msg]|
    LIGHT[msg,on,off]

  where

    process PBL_BODY [push,msg] : noexit :=

       push; msg !(true of BOOL);
       push; msg !(false of BOOL);
          PBL_BODY[push,msg]

    endproc

    process LIGHT [msg,on,off] : noexit :=

       msg ?output:BOOL;
       (
        [ output eq (true of BOOL) ] -> on;exit
        []
        [ output eq (false of BOOL) ] -> off;exit
       )
        >> LIGHT [msg,on,off]

    endproc

endspec

プロセス 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プロセスに実装されているようである。

 
spec: PBL4

        +----------+          +----------+
        |          |          |          |---->on
push--->| PBL_BODY |--------->|  LIGHT2  |
        |          | msg:BOOL | [status] |---->off
        +----------+          +----------+

図6.3 PBL4 の構成

プロセス LIGHT2 の定義として新たに必要な機能は、プロセスの内部で、1ステップ前のmsgメッセージ値 を保存しておく「状態記憶」の記述である。

このために、プロセス LIGHT2 のインスタンス生成・呼び出しを行う際、現在の状態を含めてプロセスを起動する「値付きプロセス」の定義を行う。
内部状態値 status として必要な値は、true/false といった2値でよい。従って、ここでも BooleanライブラリのBOOL型sortsを利用することとする。

specificationブロックでのプロセス LIGHT2 のインスタンス生成時には、状態値 status を false に初期化する必要がある。次に、msgからのメッセージ入力を検査し、状態変化 false <=> true といったedgeトリガが生起した場合に、状態値 statusを、true <=-> false へ交番するため、新たな値を含めたプロセス呼び出しを行う。

【PBL4.lotos】

 
specification PBL4 [push,on,off] : noexit

  library BOOLEAN endlib 

  behaviour

    hide msg in

    PBL_BODY[push,msg]
    |[msg]|
    LIGHT2[msg,on,off](false of BOOL)

  where

    process PBL_BODY [push,msg] : noexit :=

       push; msg !(true of BOOL);
       push; msg !(false of BOOL);
          PBL_BODY[push,msg]

    endproc

    process LIGHT2 [msg,on,off] (status:BOOL) : noexit :=

       msg ?output:BOOL;
       (
        [ (status eq (false of BOOL)) and (output eq (true of BOOL)) ]
           -> on; LIGHT2 [msg,on,off](true of BOOL)
        []
        [ (status eq (true of BOOL)) and (output eq (false of BOOL)) ]
           -> off; LIGHT2 [msg,on,off](false of BOOL)
       )

    endproc

endspec

<付記>
当然のことながら、( PBL3 == PBL4 ) → TRUE である。
しかし、PBL4は、下記の点において、PBL3より堅牢であると考えられる。
(1)msg入力のedgeトリガによって出力変化を行うため、msg通信路がlossyであってもある程度の伝送誤りに対しても耐性がある。
(2)内部に現在の電灯点滅状態 status を有するため、msg通信路がlossyであっても2重に on;on; といったような出力を行うことはない。

 

●Full LOTOS版 "Simple Protocol"

5.1節にてBasic-LOTOSで記述した、簡単なプロトコル(Simple Protocol)について、これの Full LOTOS版 を作成してみよう。

3.1 伝達可能メッセージの種類を導入したSPROTの仕様
3.2 Full LOTOS版 SPROTの仕様
3.3 Full LOTOS版 SPROTのLTS生成・トレースグラフの観察
3.4 SPROTのobservationalな仕様(SERVICE)


3.1 伝達可能メッセージの種類を導入したSPROTの仕様

入出力チャンネル PUT/GET、ならびに通信チャンネル channel は、伝達可能なメッセージのとして MSG というAbstract Data Typeをとるものとする。

片方向のメッセージ転送を行う簡単なプロトコル(SPROT)のモデルについて、以下に示す。

【条件】
・SPROTプロトコルは、2つの送受信プロセス:PSEND, PRECV から構成される。
・PSENDは、入力PUT(:MSG)をメッセージ転送チャンネル channel を使って PRECVへ送る。
・PRECVは、チャンネル channel から送られてきたメッセージを出力GET(:MSG)とし、ackを返す。
・PSENDは、ackを受信したら、次のメッセージ転送手順を開始する。


【SPROTのプロセス構成図】

 
spec: SPROT

      +---------+ channel  +---------+
      |         |--------->|         |
PUT-->|  PSEND  |          |  PRECV  |-->GET
:MSG  |         |<---------|         |   :MSG
      +---------+   ack    +---------+

図6.4 Simple Protocol の構成


3.2 Full LOTOS版 SPROTの仕様

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

メッセージタイプ:MSGについては、別ファイル SPROT.lib で定義する。MSG型の取り得る値の範囲については、別ファイル SPROT.t で定義する。これらのAbstract Data Typeに対する前処理は、 caesar.adtアプリケーションによって行われる。

【SPROT.lotos】

 
specification SPROT [PUT,GET] :noexit

  library SPROT endlib 

  behaviour

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

where

   process PSEND [PUT,channel,ack] :noexit :=
     PUT ?message:MSG;
       channel !message;
         ack;
           PSEND[PUT,channel,ack]
   endproc

   process PRECV [channel,GET,ack]:noexit:=
     channel ?message:MSG;
       GET !message;
         ack;
           PRECV[channel,GET,ack]
   endproc

endspec

次に、Abstract Data Typeを導入し、伝達可能なメッセージの型である MSG を 自然数値:NATURAL と見做したい。このため、Pre-definedなライブラリである BOOLEANとNATURALを導入し、メッセージタイプ MSG が、NATURALと同等である(renamedby)と定義するためのライブラリファイル SPROT.lib を作成・編集する。

【SPROT.lib】

 
library 
   BOOLEAN, NATURAL
endlib 

type MESSAGES is NATURAL renamedby
   sortnames MSG for NAT
endtype

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

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

【SPROT.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..3 */

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

 


3.3 Full LOTOS版 SPROTのLTS生成・トレースグラフの観察

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

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

を順次実行する。

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

$ 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


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


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.lotos】

 
specification SPROT_service [PUT,GET] :noexit

  library SERVICE endlib 

  behaviour

    SERVICE [PUT,GET]

where

   process SERVICE [PUT,GET] :noexit :=
     PUT ?message:MSG;
       GET !message;
         SERVICE [PUT,GET]
   endproc

endspec

 

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


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

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

$ bcg_cmp -observational SPROT.bcg SERVICE.bcg
TRUE

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

これにより、メッセージタイプ:MSGにおいても、この2つの仕様は

(SPROT == SERVICE) → TRUE

であることが確かめられた。

 

●Full LOTOS版 "通信路誤り無しABP"

通信路誤りが無い場合の交番ビットプロトコル(Alternating Bit Protocol (ABP))について、そのFull LOTOS版を考える。

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

【条件】
・メッセージタイプは MSG で定義する。
・PUT/GETされるメッセージに交番ビット 0/1 を付与する。
・ACK通知の種類は、交番ビット 0/1 の2種類とする。
・lossyな通信路はないので、再送処理は行う必要がない。


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

 
spec: ABP

      +---------+  channel +---------+
      |         |--------->|         |
PUT-->|  TRANS  |          |  RECV   |-->GET
:MSG  |  (BIT)  |<---------|  (BIT)  |   :MSG
      +---------+  ack:BIT +---------+

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

ABP の動作を記述した Full LOTOS仕様は、以下のようになる。
なお、"通信路"としての channel, ack は、gate hiding してある。

【ABP.lotos】

 
specification ABP_reliable [PUT,GET] : noexit

  library ABP endlib 

  behaviour

    hide channel,ack in
    (
      TRANS [PUT,channel,ack] (0 of BIT)
      |[channel,ack]|
      RECV  [GET,channel,ack] (0 of BIT)
    )

  where

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

      PUT ?message:MSG;       (* get next message to be sent *)
        channel !message !B;  (* send current message + control bit *)
          ack !B;             (* rendezvouz ack B *)
            TRANS [PUT,channel,ack](not (B))  (* bit alternating *)

    endproc

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

      channel ?message:MSG !B; (* get current message + rendezvouz bit *)
        GET !message;          (* output message *)
          ack !B;              (* rendezvouz ack B *)
            RECV [GET,channel,ack](not (B))  (* bit alternating *)

    endproc

endspec

先のSPROTの場合と同様、Abstract Data Typeを導入し、伝達可能なメッセージの型である MSG と、交番ビットである BIT を定義する。

Pre-definedなライブラリである BOOLEANとNATURALを導入し、メッセージタイプ MSG を、NATURALと同等である(renamedby)とし、さらに、交番ビットのための BIT というデータ型を定義するためのライブラリファイル ABP.lib を作成・編集する。

【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

SPROT同様、NAT の範囲を制限するため、ABP.t ヘッダファイルを作成・編集する。

【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..3 */

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

 

●練習問題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

<課題>
6.4節にて取り挙げた、交番ビットプロトコル(Alternating Bit Protocol (ABP))の"通信路誤りなし"のプロセスモデル(ABP)について、以下の<演習手順>に示す種々の拡張を行ったモデル 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)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 を用いて生成しなさい。また、そのトレースグラフを観察しなさい。


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

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

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