On Model Checking Distributed Algorithms

モデル検査のためのコンカレント
システムの仕様記述
土屋達弘 (大阪大学)
1
日本語でよめるモデル検査関連の
文献




米田，梶原，土屋，ディペンダブルシステム，
共立出版，2005.
電子情報通信学会ハンドブック／知識ベース，
７群１編「ソフトウェア基礎」
土屋，菊野，”モデル検査入門,” 計測と制御，
2009.
他．Amazonで検索
2
モデル検査とは

形式的検証手法




2007 Turing Award (Clarke, Emerson, Sifakis)
入力: 設計 + 特性 (仕様)
出力: Yes or No
方法: 状態探索
モデル検査器
設計
特性 (仕様)
状態機械
Yes
No
(＋反例)
3
コンカレントシステムとは

並行に処理が実行されるシステム
通常は停止しない (リアクティブシステム)

講演者の教育経験




大阪大学・大学院前期課程
組込み適塾
プログラムを中心に
講義
4
マルチスレッドのプログラム
例：Java プログラム
public class MutualExclusion extends Thread {
static volatile int t = 1;
int id;
MutualExclusion(int id) {
this.id = id;
}
public static void main(String[] args) {
new MutualExclusion(0).start();
new MutualExclusion(1).start();
}
public void run() {
while (true) {
while (t != id);
// Critical Section
t = 1 - t;
}
}
}
5
状態遷移モデル

状態遷移モデル


初期状態集合
遷移関係(遷移集合)
0: while (true) {
1:
while (t != id);
// CS
2:
t = 1 - t;
}
}
状態：(pc0, pc1, t)
0,0,1
0,0,0
0,1,0
2,0,0
1,1,0
2,1,0
1,0,1
0,1,1
1,0,0
1,1,1
0,2,1
1,2,1
6
システムをどう記述するか

コード，擬似コード
…

数式




分りやすさ



t=1
t=1–t
TLA by Lamport
証明のしやすさ
モデル検査（自動検証）のしやすさ
7
数式によるシステムの表現

状態とは？

グラフ表現:頂点

数式表現:変数への付値
例．pc0 = 0, pc1 = 2, t = 1
0,1,0
状態：(pc0, pc1, t)

遷移とは？

グラフ表現:辺


0,0,1
0,0,0
2,0,0
1,1,0
2,1,0
1,0,1
0,1,1
1,0,0
1,1,1
0,2,1
1,2,1
数式表現:変数とそのコピーへの付値
例．pc0 = 0, pc1 = 2, t = 1, pc‘0 = 1, pc‘1 = 2, t‘ = 1
プライムつき変数は，次状態に対応
8
変数と述語

変数



状態変数
プライムつき状態変数
述語
ブール値をもつ式
 状態述語: 状態変数上の述語
 遷移述語: 状態変数，プライムつき状態変数上の述
語
9
数式表現：状態集合

状態集合Sとは？

状態述語S
S = True  sS が付値


状態集合Sと状態述語Sを同一視
例．初期状態集合


I = {(pc0,pc1, t)=(0, 0, 0)}
数式表現
I := pc0=0  pc1=0  t=0
0,0,1
0,0,0
0,1,0
2,0,0
1,1,0
2,1,0
1,0,1
0,1,1
1,0,0
1,1,1
0,2,1
1,2,1
10
数式表現：遷移関係

遷移関係T (遷移集合) とは？


遷移述語T
T = True  (s, s’)T が付値
例．状態変数: x (整数型)のみ

T := (x  3  x’ = x + 1)  (x > 3  x’ = x)
x=0
x=1
x=2
x=3
x=4
x=5
x=6
11
どう数式表現を得るか？

コンカレントシステムの遷移関係を表す数式を，
どうやってもとめればよいか？

数式は設計そのもの
12
動作の表現

コンカレントシステム


並行に処理が実行されるシステム
ひとつひとつの処理
Ti := Guardi  Actioni


Guard: アクションが起こり得る条件を表す状態述語
Action: 処理による変数値の変化を表す遷移述語
13
各処理の表現
Ti := Guardi  Actioni



Guardi: アクションが起こり得る条件を表す状態述語
Actioni: 処理による変数値の変化を表す遷移述語
例．「プロセス0はPCが0のとき，PCを1にする」
T1 := pc0=0  pc’0=1  pc’1=pc1 t’ =t
0: while (true) {
1:
while (t != id);
// CS
2:
t = 1 - t;
}
}
0,0,1
0,0,0
0,1,0
2,0,0
1,1,0
2,1,0
1,0,1
0,1,1
1,0,0
1,1,1
0,2,1
1,2,1
14
動作全体の表現

各処理iに関する遷移集合


Ti := Guard1  Action1
遷移関係全体
T :=T1 T2 …  Tn 
¬(Guard1 … Guardn )pc’0=pc0pc’1=pc1t’=t
実行できる命令がないなら「次状態 = 現状態」

遷移関係はtotalでないといけない


どの状態についても次状態があること
テクニカルな理由による要求
15
Stuttering遷移

Stuttering遷移


同じ状態にとどまる遷移
遷移関係をtotalにする別の方法
T :=T1 T2 …  Tn 
pc’0=pc0pc’1=pc1t’=t
Stuttering遷移: 「次状態 = 現状態」

遷移を付加しても，
多くの性質は保存される
0,0,1
0,0,0
0,1,0
2,0,0
1,1,0
2,1,0
1,0,1
0,1,1
1,0,0
1,1,1
0,2,1
1,2,1
16
擬似コード vs. 数式表現
(Bakeryアルゴリズム)
a = 0;
b = 0;
P1 {
T: a = b + 1;
W: wait (a < b || b = 0);
C: go to T;
}
P2 {
T: b = a + 1;
W: wait (b < a || a = 0);
C: go to T;
}
17
モデル検査とは

形式的検証手法



入力: 設計 + 特性 (仕様)
出力: Yes or No
方法: 状態探索
モデル検査器
設計
特性 (仕様)
状態機械
Yes
No
(＋反例)
18
モデル検査の簡単な歴史

1980頃


1990年代



Partial Order Reduction -> SPIN
BDD (2分決定グラフ)
-> SMV
1998～


最初の研究成果
SAT (充足可能性判定)
2000年代中～後

状態グラフを
作成，探索
記号モデル検査
状態機械を記号
的に表現・操作
SMT
19
BDDによる記号モデル検査 (1/2)

BDD: ブール式を表現するデータ構造


極めてコンパクトにブール式を表現
高速な演算処理アルゴリズムが存在
f = x ¬x y
x
0

有限状態に限定すれば，



状態変数→ブール変数
演算→ブール演算
述語→ブール式
1
0
0
20
1
y
1
BDDによる記号モデル検査 (1/2)



ブール式の演算で幅優先探索が可能
V: 状態変数集合，T：遷移関係, S: 状態集合
Sへ１歩でいける状態集合
Exist(T, S)
Exist(T(V, V’)  S(V’))
Sへ0歩か1歩でいける状態集合
S  Exist(T(V, V’)  S(V’))
S  Exist(T, S)
21
S
NuSMVモデル検査器
DEFINE
T1 := (pc1 = R) & (next(pc1) = W) & (next(a) = b + 1)
& (next(pc2) = pc2) & (next(b) = b);
W1 := (pc1 = W) & (a < b | b = 0) & (next(pc1) = C)
& (next(pc2) = pc2) & (next(a) = a) & (next(b) = b);
・・・
TRANS
T1 | W1 | C1 | T2 | W2 | C2 | STUT
INIT
pc1 = R & pc2 = R & a = 0 & b = 0
22
SATを利用したモデル検査

充足可能性判定問題(SAT) （拡張版）




入力：ブール値をもつ式
出力：Yes or No
条件：Yes の必要十分条件は，
式をTrueにする変数への値の割り当て
(付値 valuation)が存在すること
例．


入力: x, y  Z, (x + y > 2)  ((x < 3)  (y < 2))
出力: Yes (付値の例 x = 2, y = 1)
23
SAT Solver /
SMT (Satisfiability Modulo Theories) Solver

SAT Solver:ブール式の充足可能性判定器

高速なヒューリステックアルゴリズム


MiniSAT, Zchaff, Grasp, …
SMT Solver: 「ブール式＋背景理論」を扱う


Yices, CVC3, Z3,…
種々の背景理論（組み合わせても良い）

配列，Linear Arithmetic (整数and/or実数の加減算大小
比較)，ビットベクトル
24
有界モデル検査

初期状態からk回の状態遷移を検査

k回の遷移をブール値の式で表現
I(0)  T(0,1)  …  T(k-1,k)  (P(0)…P(k))
充足可能 ⇒ 集合P中の状態に到達


I(0): Iの各変数varをvar0に置き換え
T(i, i+1):Tの各変数varをvariに, var’をvari+1に置き
換え
25
例．



I := x = 1
T := (x  3  x’ = x + 1)  (x > 3  x’ = x)
I(0)  T(0,1)  …  T(k-1,k)  (P(0)…P(k))
=  x0 =1
 (x0  3  x1 = x0 + 1)  (x0 >3  x1 = x0)
 (x1  3  x2 = x1 + 1)  (x1 >3  x2 = x1)
…
 (xk-1  3  xk = xk-1 + 1)  (xk-1>3  xk = xk-1)
 (P(x0) … P(xk))
充足可能 ⇒集合P中の状態に到達
26
有界モデル検査の長短

長所




初期状態に近い状態を効率良く検証
充足する場合は速い（Bug Huntingに効果的）
メモリの消費量は比較的すくない
短所

時間がかかる


特にコンカレントシステムの場合→ Ogata et al. ATVA’04
完全な検証のためには大きなkが必要


式が大きくなり時間がかかるため検証が困難
十分なkを知るのが困難
27
上限kの解消: Induction


目的: 性質Qが常に成立するか否かを判定
手法:以下の2条件を示す
初期状態で性質Qがなりたつ
1.

性質Qが成り立っているなら，次状態でも成り立つ
2.


I(0)  Q(0)
が充足不能
Q(0) T(0,1)  Q(1)
が充足不能
1, 2 ⇒ Qが常になりたつ
28
アナログ値の扱い

実時間システム，ハイブリッドシステム

アナログの変数値をどう扱うか？
ON

0.1x 0.2

一定時間における増減をひとつの処理とみなす
x_ON:= (at = ON)
 t:(t  0  10x’ – 10x  t  5x’ – 5x  t)
 (at’ = ON)
29
まとめ

数式によるコンカレントシステムの記述と
モデル検査



コンカレントシステムの数式表現
BDDによるモデル検査
SAT/SMTソルバによるモデル検査
30
MODULE main
VAR
pc1: {R, W, C};
pc2: {R, W, C};
a: 0..10;
b: 0..10;
DEFINE
T1 := (pc1 = R) & (next(pc1) = W) & (next(a) = b + 1) & (next(pc2) = pc2) & (next(b) = b);
W1 := (pc1 = W) & (a < b | b = 0) & (next(pc1) = C) & (next(pc2) = pc2) & (next(a) = a) & (next(b) = b);
C1 := (pc1 = C) & (next(pc1) = R) & (next(pc2) = pc2) & (next(a) = a) & (next(b) = b);
T2 := (pc2 = R) & (next(pc2) = W) & (next(b) = a + 1) & (next(pc1) = pc2) & (next(a) = b);
W2 := (pc2 = W) & (b < a | a = 0) & (next(pc2) = C) & (next(pc1) = pc1) & (next(a) = a) & (next(b) = b) ;
C2 := (pc2 = C) & (next(pc2) = R) & (next(pc1) = pc1) & (next(a) = a) & (next(b) = b);
STUT := (next(pc1) = pc1) & (next(pc2) = pc2) & (next(a) = a) & (next(b) = b);
TRANS
T1 | W1 | C1 | T2 | W2 | C2 | STUT
INIT
pc1 = R & pc2 = R & a = 0 & b = 0
SPEC
AG !(pc1 = C & pc2 = C)
31

Download Report