PPT

関数型言語による
Timed CSP 検証技法の提案
数理情報科学専攻
山川武志
シングルコアからマルチコアへ
• シングルコアの問題
CORE
– 発熱、消費電力
– クロックの限界
• マルチコア（プロセッサ）
– 高速処理
– 低消費電力
February 5, 2010
CORE
CORE
CORE
CORE
Yamakawa Takeshi
2
並列処理の問題
プロセスA プロセスB プロセスC
• 複数の流れを考慮した
設計が必要
– 競合の危険性
– デッドロック
• デバック＆検証が困難
February 5, 2010
Yamakawa Takeshi
3
形式手法(Formal method)
• システム開発の課題
– システムが複雑になるにつれ、テスト工程が増大
– 潜在的なバグを持ったまま運用の可能性あり
要求
分析
設計
仕様
実装
テスト・
デバック
運用
保守
設計ミス発覚！
モデル
検証
February 5, 2010
Yamakawa Takeshi
4
形式手法(Formal method)
• システム開発の課題
– システムが複雑になるにつれ、テスト工程が増大
– 潜在的なバグを持ったまま運用の可能性あり
要求
分析
設計
仕様
仕様書
形式仕様記述
自然言語
図、表
CSP,VDM
B-Method
Z記法
モデル
検証
• 形式手法
– 設計の工程で仕様記述言語を使用
– 設計の誤り、曖昧さを早い段階で除去
February 5, 2010
Yamakawa Takeshi
5
CSP(communicating sequential processes)
•
CSP理論では並行システムを、チャネルにより通信(communicating)を
行う逐次プロセス(sequential processes)の群として設計する。
•
プロセスはイベント、通信によって状態変化し、その動きは下記の代数
演算子によって定義される。
PROC :=
|
|
|
|
|
|
|
|
|
|
|
|
|
|
SKIP
STOP
ch!v
→
ch?x
→
PROC
＼
PROC [e1←e2]
PROC
;
PROC
△
PROC
＞
PROC
□
PROC
П
PROC
|||
PROC
[|c|]
PROC
||
if b then PROC
February 5, 2010
PROC
PROC
{c}
PROC
PROC
PROC
PROC
PROC
PROC
PROC
PROC
else
(正常終了)
(停止)
(output)
(input)
(hiding)
(renaming)
(sequential)
(interrupt)
(untimed timeout)
(external choice)
(internal choice)
(interleaving)
(sharing)
(parallel)
PROC (boolean)
Yamakawa Takeshi
P1
ch1
P2
ch2
P3
6
CSP(communicating sequential processes)
•
CSP理論では並行システムを、チャネルにより通信(communicating)を
行う逐次プロセス(sequential processes)の群として設計する。
•
プロセスはイベント、通信によって状態変化し、その動きは下記の代数
演算子によって定義される。
P1
P2 = ch1!10 → P2’
P1 = (ch1?x → P1’) □ (ch2!3 → SKIP)
P3 = ch2?x → if x=0 then SKIP
else P3’
ch1
P2
ch2
P3
P1 || P2 || P3
February 5, 2010
Yamakawa Takeshi
7
CSP(communicating sequential processes)
•
CSP理論では並行システムを、チャネルにより通信(communicating)を
行う逐次プロセス(sequential processes)の群として設計する。
•
プロセスはイベント、通信によって状態変化し、その動きは下記の代数
演算子によって定義される。
P1’
P2 = ch1!10 → P2’
P1 = (ch1?x → P1’) □ (ch2!3 → SKIP)
P3 = ch2?x → if x=0 then SKIP
else P3’
P1 || P2 || P3
February 5, 2010
ch1.10
P2’
ch1
ch2
P3
P1’ || P2’ || P3
Yamakawa Takeshi
8
プロセスのtrace＆failure
• CSPで記述したプロセスはtraceや
failureといった集合でとらえられる。
– Traces(P)
P1’
• プロセスPの実行可能なイベント列(trace)
すべての集合
P2’
ch1
ch2
P3
– Failures(P)
• プロセスPのtrace trとその時点で
実行不可能なイベント集合Xの組(tr,X)の集合
February 5, 2010
Yamakawa Takeshi
9
Verification&Refinement
• CSPで記述したモデルは仕様を満たしている
かどうかを数学的にチェックできる
– trace refinement（安全性）
• SPEC
SPEC
T P ⇔ Traces(SPEC) ⊇ Traces(P)
P2 = ch1!10 → P2’
P1 = (ch1?x → P1’) □ (ch2!3 → SKIP)
P3 = ch2?x → if x=0 then SKIP
else P3’
P = P1 || P2 || P3
P
P1
P2
P3
SPEC = ch1.v → ch2.v’ → SPEC
February 5, 2010
Yamakawa Takeshi
10
ツールの必要性
Verification
Design
Implementation
✔ OK
× failure
• 利便性や人為的なミスを防ぐためには検証
ツールの利用が望ましい。
• 現在、CSPを拡張した理論であるTimed CSP
に関するツールがない。
Timed CSP検証用ツールの開発へ
February 5, 2010
Yamakawa Takeshi
11
TIMED CSP
•
TIMED CSPは時間に関する代数演算子をCSPに加え、さらに理論を拡
張したものである。
•
時間を考慮した動作が表現可能であり、各プロセスはイベント、通信、時
間によって状態変化する。
PROC := SKIP
(正常終了)
| STOP
(停止)
| ch!v
→
PROC
(output)
ch?x d →
PROC
• | WAIT
wait
process (input)
| PROC
＼
{c}
(hiding)
• | c@u
P(u)
timed event prefix
PROC→
[e1←e2]
(renaming)
| PROC
;
PROC
(sequential)
d
• | cPROC
→ P △ timed
PROC prefix (interrupt)
d
| PROC
＞
PROC
(untimed timeout)
• P►Q
timeout
| PROC
□
PROC
(external choice)
PROC interrupt
(internal choice)
• | PPROC
△d Q П
timed
| PROC
|||
PROC
(interleaving)
| PROC
[|c|]
PROC
(sharing)
| PROC
||
PROC
(parallel)
| if b then PROC else PROC (boolean)
February 5, 2010
Yamakawa Takeshi
3 time
P1
P2
P3
12
TIMED CSP
•
TIMED CSPは時間に関する代数演算子をCSPに加え、さらに理論を拡
張したものである。
•
時間を考慮した動作が表現可能であり、各プロセスはイベント、通信、時
間によって状態変化する。
PROC := SKIP
(正常終了)
| STOP
(停止)
| ch!v
→
PROC
(output)
ch?x d →
PROC
• | WAIT
wait
process (input)
| PROC
＼
{c}
(hiding)
• | c@u
P(u)
timed event prefix
PROC→
[e1←e2]
(renaming)
| PROC
;
PROC
(sequential)
d
• | cPROC
→ P △ timed
PROC prefix (interrupt)
d
| PROC
＞
PROC
(untimed timeout)
• P►Q
timeout
| PROC
□
PROC
(external choice)
PROC interrupt
(internal choice)
• | PPROC
△d Q П
timed
| PROC
|||
PROC
(interleaving)
| PROC
[|c|]
PROC
(sharing)
| PROC
||
PROC
(parallel)
| if b then PROC else PROC (boolean)
February 5, 2010
Yamakawa Takeshi
5 time
P1’
P2
P3
13
TIMED CSP
•
TIMED CSPは時間に関する代数演算子をCSPに加え、さらに理論を拡
張したものである。
•
時間を考慮した動作が表現可能であり、各プロセスはイベント、通信、時
間によって状態変化する。
PROC := SKIP
(正常終了)
| STOP
(停止)
| ch!v
→
PROC
(output)
ch?x d →
PROC
• | WAIT
wait
process (input)
| PROC
＼
{c}
(hiding)
• | c@u
P(u)
timed event prefix
PROC→
[e1←e2]
(renaming)
| PROC
;
PROC
(sequential)
d
• | cPROC
→ P △ timed
PROC prefix (interrupt)
d
| PROC
＞
PROC
(untimed timeout)
• P►Q
timeout
| PROC
□
PROC
(external choice)
PROC interrupt
(internal choice)
• | PPROC
△d Q П
timed
| PROC
|||
PROC
(interleaving)
| PROC
[|c|]
PROC
(sharing)
| PROC
||
PROC
(parallel)
| if b then PROC else PROC (boolean)
February 5, 2010
Yamakawa Takeshi
5 time
P1’
P2
P3’
14
Timed CSP Explorerの開発
• ツールの開発には関数型言語MLを用
いた。
• Timed CSPのプロセスはイベントまたは
時間により次のプロセスに移る。
P
ch.10
P: event∪time → process
P’
P(ch.10) ≡ P’
• プロセスはイベントを引数にとりプロセス
（関数）を返す関数としてとらえる。
February 5, 2010
Yamakawa Takeshi
15
Timed CSP Explorer構成
• コード生成部
– CSP記述を解析し、実行用ML記述を
出力する。
• CSP検証部
– 代数演算子等を関数定義し、ML記述を
実行する。
CSP記述
コード生成部
channel in,out:Int
P = in?x -> out!fact(x) -> P
fact(x) =
if x>1 then x*fact(x-1)
else 1
February 5, 2010
CSP検証部
Yamakawa Takeshi
ML記述
channel in,out:Int
fun P =
prefix( input(in,x),
prefix( output(out,fact(x)),
Recur(P) )
fact(x) =
if x>1 then x*fact(x-1)
else 1
16
コード生成部
• コンパイラの字句解析、構文解析技術
を用いてプロセスの構造を木構造でと
らえる。
• 木を行きがけ順（根→左→右）で探索
しながら目的のMLコードを出す。
TEST = out!10 → ( (a → P || b → Q) △t1 c →t2 R )
test = prefix(out.10,
tinterrupt(
parallel( prefix(a,P), prefix(b,Q) ),
Time t1,
tprefix(c, Time t2, R )
)
)
February 5, 2010
Yamakawa Takeshi
17
CSP検証部
• 生成部により出力された関数はCSP
プロセスの実装になっている。
• プロセスに対応した関数にイベントを
与えることで、プロセスの振る舞いを
検査することができる。
TEST = out!10 → ( (a → P || b → Q) △t1 c →t2 R )
test = prefix(out.10,
tinterrupt(
parallel( prefix(a,P), prefix(b,Q) ),
Time t1,
tprefix(c, Time t2, R )
)
)
February 5, 2010
Yamakawa Takeshi
18
例 Fischer’s algorithm
• 相互排他アルゴリズム
• 共有変数によりenterできるプロセスを唯一に制御
Qi = req.i → read?x →
if x≠0 then SKIP
else ( write!i → enter.i → exit.i → SKIP )
V(value) = read!value → V(value) [] write?i → V(i)
FISCHER =
(|||n∈3Qn) || V(0)
enter.1
req.1
FISCHER
enter.2
Q1
write
write
exit.3
req.3
Q2
read
enter.3
exit.2
req.2
SPEC =
[] n∈3 enter.i → exit.i → SKIP
SPEC
exit.1
Q3
0
read
write
read
2
0
Shared variable
V
February 5, 2010
Yamakawa Takeshi
19
例 Fischer’s algorithm
• 相互排他アルゴリズム
• 共有変数によりenterできるプロセスを唯一に制御
Qi = req.i → read?x →
if x≠0 then SKIP
else ( write!i → enter.i → exit.i → SKIP
V(value) = read!value → V(value) [] write?i → V(i)
FISCHER =
(|||n∈3Qn) || V(0)
enter.1
req.1
FISCHER
enter.2
exit.2
req.2
SPEC =
[] n∈3 enter.i → exit.i → SKIP
SPEC
exit.1
Q1
write
read
exit.3
req.3
Q2
0
enter.3
write
Q3
0
read
write
read
0
February 5, 2010
Yamakawa Takeshi
20
例 Fischer’s algorithm
• 相互排他アルゴリズム
• 共有変数によりenterできるプロセスを唯一に制御
Qi = req.i → read?x →
if x≠0 then SKIP
ε
else ( write!i → read?y →
if y≠i then SKIP
δ
else enter.i → exit.i → write!0 → SKIP ) ► STOP
V(value) = read!value → V(value) [] write?i → V(i)
enter.1
FISCHER =
(|||n∈3Qn) || V(0)
req.1
SPEC =
[] n∈3 enter.i → exit.i → SKIP
SPEC
exit.1
enter.2
exit.2
req.2
Q1
write
read
exit.3
req.3
Q2
0
1
enter.3
write
Q3
1
0
read
write
read
FISCHER
2
1
0
February 5, 2010
Yamakawa Takeshi
21
まとめ
• 研究結果
– 関数型言語の利点をいかすことでCSPのプ
ロセスを簡潔に実装できることを示したうえで、
Timed CSPプロセスの実装を行った。
– 自動検証ツールTimed CSP Explorerを試作
しそれを用いて排他制御アルゴリズムの検証
を行った。
• 今後
– リアルタイムシステムの設計、検証に応用し
ていく。
– 大規模システムに耐えうる状態圧縮のアルゴ
リズムの考案とその実装を行う。
February 5, 2010
Yamakawa Takeshi
22

Download Report