モデル検査（1）概要 - 知能ソフトウェア研究室

表現系工学特論
(model checking)
モデル検査（２）
プロセス代数に基づくモデリング
(modeling in process algebra)
１．プロセス代数
２．逐次プロセスのモデリング
3．並行プロセスのモデリング
参考文献
Concurrency: State Models & Java Programming,
J. Magee & J. Kramer, Wiley (2006)
モデル検査 (復習)
モデル
model
（状態遷移系）
モデル記述言語
•C言語風のもの
•プロセス代数
モデル検査器
model checker
性質
property
（安全性，活性）
性質の記述
•時相論理
検査結果
ＯＫ
反例
The result is
either OK or
a counterexample
(process algebra)
１．プロセス代数
代数とは何か
プロセス代数とは
プロセス代数に基づく言語
(algebra)
代数とは何か
 要素の集合（台）およびその上での演算の集
まりからなる計算系
a
台(universe)
b
演算
e
d
(operation)
c
c=a○b
(operator)
演算子
例：（整数の集合，＋，×）
等号
(equality)
(process algebra)
プロセス代数とは
 プロセスやイベント等の集合を台とし，
プロセスの合成などの演算を定義した代数
a
Event
e
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
今回の講義ではこれを紹介
(modeling sequential processes)
２．逐次プロセスのモデリング
プロセス＝アクション＋状態遷移
ラベル付き遷移系とFSPによるモデリング
アクション接頭辞
選択
添え字付きアクション
ガード付きアクション
(process)
(action)
(state transition)
プロセス＝アクション＋状態遷移
 状態(state)
(program counter)
 プログラムカウンタの値と
 （明示的あるいは暗黙的な）変数の値からなる
 状態遷移(state transition)
(variable)
 割り込み不能の原子アクション(atomic action)
により状態が遷移する
 プロセス(process)
 １つの逐次プログラムの実行のこと．
 有限状態機械（オートマトン）でモデル化される
(finite state machine: automaton)
ラベル付き遷移系とFSPによるモデリング
 ラベル付き遷移系(Labeled Transition System)
 有限状態機械を図式的に表現したシステム
 FSP
(Finite State Processes)
 ラベル付き遷移系を代数的に表現する言語
(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.
(Example: a binary switch)
スイッチの例(1) ラベル付き遷移系
action
on
initial
state
OFF
0
ON
ラベル付き遷移系
1
off
トレース(trace) : 実行可能なアクションの列のこと
onoffonoffonoff ……….
スイッチの例(2) FSPによる記述
FSP
SWITCH = OFF,
OFF
= (on -> ON),
ON
= (off-> OFF).
on
OFF
0
ON
ラベル付き遷移系
1
off
プロセス名は大文字
アクション名は小文字
代入によってより簡潔な表現を得る：
SWITCH = OFF,
OFF
= (on ->(off->OFF)).
SWITCH = (on->off->SWITCH).
(Simplify the expressions
by substitution)
(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.
(Example: a vending machine)
自動販売機の例
（ボタンの色で飲み物を指定）
DRINKS = ( red->coffee->DRINKS
| blue->tea->DRINKS
).
blue
red
0
1
coffee
tea
2
(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).
toss
0
toss
1
heads
COIN = (toss-> heads -> COIN
|toss-> tails -> COIN
).
tails
2
(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
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).
out
(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]
).
inc
0
inc
1
dec
inc
2
dec
3
dec
(modeling concurrent processes)
３．並行プロセスのモデリング
プロセスの並列合成
アクションのインタリーブ
ラベル付き遷移系の合成
共有アクションとインタラクション
(parallel composition of processes)
プロセスの並列合成
(P||Q)
プロセス P と Q の並行実行を表すプロセス．
|| は並列合成演算子．
Commutative:
Associative:
(P||Q) = (Q||P)
(P||(Q||R)) = ((P||Q)||R)
= (P||Q||R).
(action interleaving)
アクションのインタリーブ
かゆいところをかく
プロセス
プロセス間で共有されないアクションは
インタリーブされる
共有アクション
無し
ITCH = (scratch->STOP).
CONVERSE = (think->talk->STOP).
会話するプロセス
||CONVERSE_ITCH = (ITCH || CONVERSE).
並列合成は
|| で書き始める
並列合成された
プロセス
thinktalkscratch
thinkscratchtalk
scratchthinktalk
インタリーブによって
可能となるトレース
ラベル付き遷移系の並列合成
scratch
think
ITCH
talk
CONVERSE
0
1
2 states
0
Pの状態pとQの状態qの組(p,q)が，
P||Qの状態となる
A pair (p, q) of states of
processes P and Q is
a state of the
composed process
think
P || Q
CONVERSE_ITCH
from ITCH
1
2
3 states
2 x 3 states
scratch
scratch
scratch
talk
0
1
2
(0,0)
(0,1)
(0,2)
from CONVERSE
(1,2)
5
4
3
talk
(1,1)
think
(1,0)
(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
インタラクションの例
MAKER = (make->ready->used->MAKER).
USER = (ready->use->used ->USER).
3 状態
3 状態
||MAKER_USER = (MAKER || USER).
3 x 3
状態?
make
0
ready
1
use
2
4 状態
3
インタラクションは
振舞いを制約する
used
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)
４．ＦＳＰの意味論の概要
ラベル付き遷移系の形式的定義
ＦＳＰの意味論の枠組み
アクション接頭辞
選択
並列合成
(Formal definition of Labeled Transition System: LTS)
ラベル付き遷移系(LTS)の形式的定義(1)
States : すべての状態の集合
Act  L    : すべてのアクションの集合．
Ｌは観測可能なアクションの集合（ラベル）．
τは LTS から観測できない内部アクション
(States is the set of all the states)
(Act is the set of all the actions)
ラベル付き遷移系(LTS)の形式的定義(2)
有限 LTS は四ツ組 P  S , A, , q である．
S  States
状態の有限集合
A  Act
アクションの集合．
  S  A S
遷移関係
(a set of states)
(a set of actions)
(a transition relation)
（現状態，アクション，次状態）
qS
初期状態
(an initial state)
ラベル付き遷移系(LTS)の形式的定義(3)
LTS P  S , A, , q は， (q, a, q)  のとき，
アクション a  A により LTS P  S , A, , q に遷移．
 P と書く．
これを P 
a
P
q
a
P'
q'
ＦＳＰの意味論の枠組み
意味関数
lts : Exp  Ps
により意味を定義．
Exp は FSP で記述されるプロセス表現の集合．
Ps は LTS の集合．
構文領域 Exp
意味領域 Ps
lts
アクション接頭辞
lts(a > E)  S  p, A a,  ( p, a, q), p
ただし，lts( E)  S , A, , q ，p は新しい状態（ p  S ）
．
lts(a->E)
p
lts(E)
a
q
選択
lts (a1   E1 | a2   E2 )
 S1  S2   p , A1  A2  a1 , a2  ,
1   2  ( p, a1 , q1 ),( p, a2 , q2 ) , p
ただし， lts( Ei )  Si , Ai , i , qi (i  1,2) ，
p は新しい状態（ p  S1  S2 ）．
lts(a1->E1 | a2->E2) a1
q1
lts(E1)
q2
lts(E2)
p
a2
並列合成
lts( P || Q)  lts( P) || lts(Q)
P || Q  S1  S2 , A1  A2 , , (q1 , q2 )
ただし， P  S1 , A1 , 1 , q1 ， Q  S2 , A2 , 2 , q2 ，
 はつぎの推論規則を満たす最小の遷移関係 (a   ) ．
a
a
P 
 P, Q 
 Q
a
P || Q 
 P || Q
a
P 
 P
(a  A2 )
a
P || Q 
 P || Q
インタラクション
a
Q 
 Q
(a  A1 )
a
P || Q 
 P || Q

Download Report