2009-04-22

sequential(逐次)

seqential ';' は P;Q で、プロセスP,Q の逐次処理を表わす。ただし、プロセスP が SKIP になったときにのみプロセスQに実行が移る。

２回の販売で終了する自動販売機は以下のように書けた。

channel coin, juice
VM2 = coin -> juice -> coin -> juice -> SKIP

このプロセスVM2は ';' を使って次のように書くこともできる。

 VM = coin -> juice -> SKIP
 VM2 = VM ; VM
 -- VMはイベントではないので、VM -> VM と記述するのは誤り。

プロセスVM2 はまず、最初のVMを実行する。イベントcoin,juiceの後、SKIP;VM の状態になったら後ろの VM に実行が移る。
5回の販売で終了する販売機VM5は

VM5 = VM ; VM ; VM ; VM ; VM

また、n回繰り返したい場合は以下のような書き方も用意されている。

 VMN = ;i:<1..n>@ VM   -- replicated sequential、iが1〜nまで繰り返す。
 
 -- VM5 = ;i:<1..5>@ VM である。

2009-04-22

prefix(接頭辞)

代数演算子

簡単な例

これから幾つかの代数演算子を簡単な例を用いて解説していく。CSPは主に並行システムを記述するものであるが、まずは身近な例であるジュースの自動販売機と購入者の相互作用を例にモデル記述していくことにする。

自販機と購入者の動作（イベント）については以下のものを考える。

お金を入れる(coin)
ジュースを出す(juice)

prefix（接頭辞）

prefix '->' は (event) -> (PROCESS) のように使われ、event の後に PROCESS が実行される。(event)->(PROCESS) 自体もまたプロセスとなる。

コインを入れるとジュースが出る自動販売機VM(VendingMachine)の例*1

 -- FDR2ではキーワード 'channel' を使ってイベントを定義する。
 channel coin, juice          -- coin, juice をイベントとして定義
 VM = coin -> juice -> SKIP   -- SKIPは正常終了を表すプロセス

プロセスVMは一回の販売で終了となる自動販売機である。

VMは coin のイベントが起きた後 (juice -> SKIP) というプロセスに移る。このプロセスはイベント juice の後、SKIP（正常終了）となる。

２回販売して終了する自動販売機VM2は

VM2 = coin -> juice -> coin -> juice -> SKIP

*1:CSPマシンリーダブルで表記する。また、FDR2では'--' ではじまる行と、'{-' と '-}' の間はコメント扱いとなり無視される。

2009-04-22

FDR2とは

FDR2

FDR2(Failures/Divergence Refinement 2)とはFormal Systems Europe Ltd. が開発したCSPの自動検証ツールである。

CSPで記述したプロセスのRefinment,Deadlock,Livelock,Determinismをチェックすることができる。

上記 Formal Systems のサイトからFDR2、マニュアル等がダウンロードできる。

実行には、環境変数FDRHOMEにFDR2をインストールしたルートディレクトリをセットする必要がある。

FDRHOME=~/FDR2/fdr-2.83-linux-academic
export FDRHOME

実行するとまず、下のようなファイルを選択する画面が出てくる。

CSP記述を含んだファイル（拡張子は.csp）を選択すれば、下記のようなFDR2の実行画面が出てくる。

このツールの使い方についても随時説明していく。

2009-04-22

プロセス代数CSP

CSP概要

Communicating Sequential Processes（CSP）とは並行システムを相互作用するプロセスの群として捉え記述し、その正しさを数学的に証明するための仕様記述言語である。
ここで、相互作用とは特にイベントと呼ばれシステムに応じて定義する。プロセスはイベントとCSPの代数演算子により以下のように定義される。

PROC = SKIP                     (正常終了)
       STOP                     (停止)
       event   ->     PROC      (接頭辞 prefix)
       PROC     \     {c}       (隠蔽 hiding)
       PROC [[e1<-e2]]          (変更 renaming)
       PROC     ;     PROC      (逐次 sequential)
       PROC    /\     PROC      (割り込み interrupt)
       PROC    [>     PROC      (untimed timeout)
       PROC    []     PROC      (外部選択 external choice)
       PROC    |~|    PROC      (内部選択 internal choice)
       PROC    |||    PROC      (interleaving)
       PROC   [|c|]   PROC      (sharing)
       PROC [c1||c2]  PROC      (alphabetized parallel)
       PROC [e1<->e2] PROC      (linked parallel)
       if b then PROC else PROC (条件選択 boolean)

PROC  :プロセス
e1,e2 :イベント
c1,c2 :イベントの集合
b     :boolean式

例えば、a,bをイベントとすると prefixにより、 a -> SKIP や b -> STOP はプロセスとなる。さらにこれらプロセスの外部選択 (a -> SKIP) [] (b -> STOP) もプロセスとなる。さらに・・・

このようにして複雑な振る舞いをするプロセス（システム）を記述していく。各演算子について次章以降で例を交え説明していく。