サイトの説明 並行システムなどを研究していてFormal Methods(形式手法)であるCSPに興味を持ったのだが、日本語であまり良い解説・入門サイトがないようなので自分で書いてみようかと思いました。少しでも役に立てれば幸いです。リンク、コメントなどは自由…
CSPではプロセス間の様々なデータの受け渡しをチャネルを用いたメッセージパッシング方式で行う。 channel ch:{0..7} -- チャネルchの型を{0,1,・・,6,7}とする。 P = ch!5 -> SKIP -- '!'は送信を意味する。 Q = ch?x -> SKIP -- '?'は受信を意味する。 SYS…
昔はよく当たりのある自動販売機が街角にあった。ジュースを買うとルーレットがまわり、当たるともう1本もらえるというものである。今回はそれを単純化しモデリングする。 channel coin, juice VMB(n) = coin -> juice -> ( VMB(n-1) |~| juice -> VMB(n-2)…
conditional choice "if b then P else Q" は bがTRUEの場合プロセスPが、bがFALSEの場合はプロセスQが実行される。例えば、ジュースの残数を保持している自販機VMRの例を考える。 channel coin, juice VMCNT(n) = coin -> juice -> VMCNT(n-1) VMR = VMCNT(…
renaming P[ [e channel coin,coke,lemonade,cider,drink PERSON = coin -> ( coke -> drink -> SKIP |~| lemonade -> drink -> SKIP ) MIKE = PERSON[[ lemonade<-cider ]] -- このプロセスは次のようになる。 MIKE = coin -> ( coke -> drink -> SKIP |~| …
interrupt '/\' は P/\Q でプロセスPの実行中に Q が割り込む可能性を表す。プロセスP 実行中にプロセス Q のイベントが起こると Q に実行が移る。その後 P に実行は戻らない。親子が自販機でジュースを買うときに、親がコインを入れボタンを押そうとすると…
購入者、自動販売機をそれぞれCSPでモデリングし、正しく動作するシステムを検証しながら設計してみよう。まず、下記のような購入者3人と自動販売機をモデリングする。購入者の動作はコインを入れ、ジュースのボタンを押す。 channel coin, juice PERSON = c…
hiding'\'は (PROCESS) \ {(events)} と記述し、プロセスのアルファベット(インターフェイス)から指定したイベントを隠蔽する。下記の sharing で考えた例を使って解説する。 channel coin, coke, cider, lemonade, drink MIKE = coin -> ( coke -> drink …
interleaving P|||Q はプロセスP,Q がイベントで同期せずに、完全に独立して動作することを表す。例えば、以下のようなMIKEとRISAの動作を考える。 channel coin, coke, cider,lemonade, drink MIKE = coin -> ( coke -> drink -> SKIP |~| cider -> drink -…
interleaving の例において、MIKEとRISAはコインを別々に入れるが、二人で乾杯して同時に飲み始めるような場合はsharing(共有)を使う。 P[|{event}|]Q のように記述すると指定されたイベントで同期し、それ以外のイベントについては interleavingと同じく…
アルファベット プロセスのアルファベットを定義しておく。プロセスP のアルファベットαP とは P の持つべきイベントの集合である。例えば、 channel coin, coke, lemonade,drink VMS = coin -> ( coke -> VMS [] lemonade -> VMS ) aVMS = {coin, coke, lem…
internal choice '|~|'はプロセスの内部選択を表す。外部選択との違いを購入者の例を使って説明する。購入者はコインを入れ、コーラかレモネードを購入した後にそれを飲む。コーラとレモネードの選択は購入者自身の好みや気分によって決定されるとする。 cha…
external choice P[]Q はプロセスの選択を意味する。プロセスP,Q のどちらのイベントが先に起こるかによって実行するプロセスが決定される。 例えば、コインを入れた後、いくつかの種類が選べる自動販売機は次のようになる。 channel coin, coke, lemonade V…
何度も繰り返し販売できる自動販売機は再帰を用いて次のように記述できる。 VMR = coin -> juice -> VMR プロセスVMRはイベント coin,juice の後、再び自身VMRに移っている。VMRはcoin,juice,coin,juice,・・・を繰り返すプロセスである。また、VMRは次のよ…
seqential ';' は P;Q で、プロセスP,Q の逐次処理を表わす。ただし、プロセスP が SKIP になったときにのみプロセスQに実行が移る。2回の販売で終了する自動販売機は以下のように書けた。 channel coin, juice VM2 = coin -> juice -> coin -> juice -> SK…
簡単な例 これから幾つかの代数演算子を簡単な例を用いて解説していく。CSPは主に並行システムを記述するものであるが、まずは身近な例であるジュースの自動販売機と購入者の相互作用を例にモデル記述していくことにする。自販機と購入者の動作(イベント)…
FDR2(Failures/Divergence Refinement 2)とはFormal Systems Europe Ltd. が開発したCSPの自動検証ツールである。CSPで記述したプロセスのRefinment,Deadlock,Livelock,Determinismをチェックすることができる。上記 Formal Systems のサイトからFDR2、マニ…
Communicating Sequential Processes(CSP)とは並行システムを相互作用するプロセスの群として捉え記述し、その正しさを数学的に証明するための仕様記述言語である。 ここで、相互作用とは特にイベントと呼ばれシステムに応じて定義する。プロセスはイベン…