モデル検査（２） プロセス代数に基づくモデリング 表現系工学特論 (model checking) モデル検査（２） プロセス代数に基づくモデリング (modeling in process algebra) １．プロセス代数 ２．逐次プロセスのモデリング 3．並行プロセスのモデリング 参考文献 Concurrency: State Models & Java Programming, J. Magee & J. Kramer, Wiley (2006)

モデル検査 (復習) モデル検査器 検査結果 モデル model checker model ＯＫ （状態遷移系） 反例 モデル記述言語 モデル検査 (復習)　　 モデル検査器 model checker 検査結果 モデル model （状態遷移系） ＯＫ 反例 モデル記述言語 C言語風のもの プロセス代数 性質 property （安全性，活性） The result is either OK or a counterexample 性質の記述 時相論理

代数とは何か プロセス代数とは プロセス代数に基づく言語 １．プロセス代数 (process algebra) 代数とは何か プロセス代数とは プロセス代数に基づく言語

代数とは何か 要素の集合（台）およびその上での演算の集まりからなる計算系 台(universe) 例： （整数の集合，＋，×） (algebra) 要素の集合（台）およびその上での演算の集まりからなる計算系 a b 台(universe) 演算 e (operation) d c c = a ○ b (operator) 演算子 例：　（整数の集合，＋，×） 等号 (equality)

プロセス代数とは プロセスやイベント等の集合を台とし， プロセスの合成などの演算を定義した代数 Q = e ○ P (process algebra) プロセスやイベント等の集合を台とし， プロセスの合成などの演算を定義した代数 a e Event P Process 演算 R Q Q = e ○ P

プロセス代数に基づく言語 CSP (Communicating Sequential Processes) by Hoare CCS (Calculus of Communicating Systems) by Milner FSP (Finite State Processes) by Magee & Kramer 今回の講義ではこれを紹介

プロセス＝アクション＋状態遷移 ラベル付き遷移系とFSPによるモデリング アクション接頭辞 選択 添え字付きアクション ガード付きアクション ２．逐次プロセスのモデリング (modeling sequential processes) プロセス＝アクション＋状態遷移 ラベル付き遷移系とFSPによるモデリング アクション接頭辞 選択 添え字付きアクション ガード付きアクション

プロセス＝アクション＋状態遷移 状態(state) 状態遷移(state transition) プロセス(process) (action) (state transition) 状態(state) プログラムカウンタの値と （明示的あるいは暗黙的な）変数の値からなる 状態遷移(state transition) 割り込み不能の原子アクション(atomic action)により状態が遷移する プロセス(process) １つの逐次プログラムの実行のこと． 有限状態機械（オートマトン）でモデル化される (program counter) (variable) (finite state machine: automaton)

ラベル付き遷移系とFSPによるモデリング ラベル付き遷移系(Labeled Transition System) 有限状態機械を図式的に表現したシステム FSP (Finite State Processes) ラベル付き遷移系を代数的に表現する言語

アクション接頭辞 (a-> P) 最初にアクション a を実行し，つぎにプロセス Pと同じ振る舞 いをするプロセス． (action prefix) (a-> P) 最初にアクション a を実行し，つぎにプロセス Pと同じ振る舞 いをするプロセス． (a -> P) is a process that initially engages in the action a and then behaves exactly as described by the process P.

スイッチの例(1) ラベル付き遷移系 ラベル付き遷移系 トレース(trace) : 実行可能なアクションの列のこと (Example: a binary switch) action initial state OFF ON ラベル付き遷移系 トレース(trace) : 実行可能なアクションの列のこと onoffonoffonoff ……….

スイッチの例(2) FSPによる記述 FSP SWITCH = OFF, OFF = (on -> ON), ON = (off-> OFF). OFF ON ラベル付き遷移系 プロセス名は大文字 アクション名は小文字 代入によってより簡潔な表現を得る： (Simplify the expressions by substitution) SWITCH = OFF, OFF = (on ->(off->OFF)). SWITCH = (on->off->SWITCH).

選択 (choice) (a-> P | b->Q) 最初にアクション a ,bのいずれかを実行する． そのアクションが a ならつぎにプロセス P を実行し， bならつぎにプロセス Q を実行するプロセス． (a->P | b->Q) is a process which initially engages in either a or b. The subsequent behavior is described by P if the first action was a, and Q if the first action was b.

自動販売機の例 DRINKS = ( red->coffee->DRINKS | blue->tea->DRINKS (Example: a vending machine) （ボタンの色で飲み物を指定） DRINKS = ( red->coffee->DRINKS | blue->tea->DRINKS ).

非決定的選択 (non-deterministic choice) Process (x-> P | x -> Q) describes a process which engages in x and then behaves as either P or Q. COIN = (toss->HEADS | toss->TAILS), HEADS= (heads->COIN), TAILS= (tails->COIN). COIN = (toss-> heads -> COIN |toss-> tails -> COIN ).

添え字付きアクション i (indexed actions) Single slot buffer that inputs a value in the range 0 to 3 and then outputs that value: BUFF = (in[0]->out[0]->BUFF |in[1]->out[1]->BUFF |in[2]->out[2]->BUFF |in[3]->out[3]->BUFF ). BUFF in i out equivalent to BUFF = (in[i:0..3]->out[i]-> BUFF). or using a process parameter with default value: BUFF(N=3) = (in[i:0..N]->out[i]-> BUFF).

ガード付きアクション (when C a-> P | b->Q) (guarded actions) (when C a-> P | b->Q) ガードCが真のときのみアクションa が選択され得る． アクションbは，ガードがないので，常に選択され得る． COUNT (N=3) = COUNT[0], COUNT[i:0..N] = (when(i<N) inc->COUNT[i+1] |when(i>0) dec->COUNT[i-1] ).

プロセスの並列合成 アクションのインタリーブ ラベル付き遷移系の合成 共有アクションとインタラクション ３．並行プロセスのモデリング (modeling concurrent processes) プロセスの並列合成 アクションのインタリーブ ラベル付き遷移系の合成 共有アクションとインタラクション

プロセスの並列合成 (P||Q) プロセス P と Q の並行実行を表すプロセス． || は並列合成演算子． (parallel composition of processes) (P||Q) プロセス P と Q の並行実行を表すプロセス． || は並列合成演算子． Commutative: (P||Q) = (Q||P) Associative: (P||(Q||R)) = ((P||Q)||R) = (P||Q||R).

アクションのインタリーブ ITCH = (scratch->STOP). (action interleaving) 共有アクション 無し かゆいところをかくプロセス プロセス間で共有されないアクションはインタリーブされる ITCH = (scratch->STOP). CONVERSE = (think->talk->STOP). ||CONVERSE_ITCH = (ITCH || CONVERSE). 会話するプロセス 並列合成された プロセス 並列合成は || で書き始める thinktalkscratch thinkscratchtalk scratchthinktalk インタリーブによって 可能となるトレース

ラベル付き遷移系の並列合成 2 states 3 states 2 x 3 states (0,0) (0,1) (0,2) (1,2) Pの状態pとQの状態qの組(p,q)が，P||Qの状態となる 2 x 3 states A pair (p, q) of states of processes P and Q is a state of the composed process P || Q (0,0) (0,1) (0,2) (1,2) (1,1) (1,0) from ITCH from CONVERSE

共有アクションとインタラクション 共有アクション (shared action)： 並列合成されたプロセスがもつ共通のアクション． (shared action and interaction) 共有アクション (shared action)：　 　　並列合成されたプロセスがもつ共通のアクション． 共有アクションによってプロセスのインタラクション(interaction)をモデル化． 共有アクションは，それを共有するすべてのプロセスにおいて同時に同期(synchronized)して実行されなければならない． A shared action must be executed at the same time by all processes that participate in that shared action. In other words, those executions must be synchronized.

shared actions: ready, used インタラクションの例 shared actions: ready, used MAKER = (make->ready->used->MAKER). USER = (ready->use->used ->USER). ||MAKER_USER = (MAKER || USER). 3 状態 3 状態 3 x 3 状態? 4 状態 インタラクションは 振舞いを制約する The interaction constrains the behavior.

演習問題 二人のユーザーを表すプロセスUSER_A，USER_B，および共有資源を表すプロセスRESOURCE，およびそれらを並列合成したプロセスRESOURCE_SHAREが，FSPでつぎのように定義されている． USER_A = (a_acquire -> a_use -> a_release -> USER_A). USER_B = (b_acquire -> b_use -> b_release -> USER_B). RESOURCE = IDLE, 　　IDLE = (a_acquire -> BUSY　|　b_acquire -> BUSY), 　　BUSY = (a_release -> IDLE |b_release -> IDLE). ||RESOURCE_SHARE = (USER_A || USER_B || RESOURCE). これら４つのプロセスのラベル付き遷移系をそれぞれ描画せよ．

ここから先のスライドは授業では使わない

ラベル付き遷移系の形式的定義 ＦＳＰの意味論の枠組み アクション接頭辞 選択 並列合成 ４．ＦＳＰの意味論の概要 (Introduction to the semantics of FSP) ラベル付き遷移系の形式的定義 ＦＳＰの意味論の枠組み アクション接頭辞 選択 並列合成

ラベル付き遷移系(LTS)の形式的定義(1) (Formal definition of Labeled Transition System: LTS) (States is the set of all the states) (Act is the set of all the actions)

ラベル付き遷移系(LTS)の形式的定義(2) (a set of states) (a set of actions) (a transition relation) (an initial state)

ラベル付き遷移系(LTS)の形式的定義(3) P P' a q q'

ＦＳＰの意味論の枠組み 意味領域　Ps 構文領域　Exp lts

アクション接頭辞 lts(a->E) lts(E) a p q

選択 lts(a1->E1 | a2->E2) a1 q1 lts(E1) p q2 lts(E2) a2

並列合成 インタラクション