On Model Checking Distributed Algorithms

充足可能性判定を利用した
モデル検査
土屋達弘 (大阪大学)
1
モデル検査とは

形式的検証手法




2007 Turing Award (Clarke, Emerson, Sifakis)
入力: 設計 + 特性 (仕様)
出力: Yes or No
方法: 状態探索
モデル検査器
設計
特性 (仕様)
状態機械
Yes
No
(＋反例)
2
簡単な歴史

1980頃


1990年代



Partial Order Reduction -> SPIN
BDD (2分決定グラフ)
-> SMV
1998～


最初の研究成果
SAT (充足可能性判定)
2000年代中～後

記号モデル検査
状態機械を記号
的に表現・操作
今回のトピック
SMT
3
日本語でよめる記号モデル検査
関連の文献




米田，梶原，土屋，ディペンダブルシステム，
共立出版，2005.
電子情報通信学会ハンドブック／知識ベース，
７群１編「ソフトウェア基礎」
土屋，菊野，”モデル検査入門,” 計測と制御，
2009.
土屋，菊野，”記号モデル検査の並行ソフトウェアシ
ステムへの応用,”第17 回回路とシステム軽井沢ワ
ークショップ，2004.
4
Part I
逐次プログラムのモデル検査
5
充足可能性判定問題 (拡張版)

入力：ブール値をもつ式
出力：Yes or No
条件：Yes の必要十分条件は，
式をTrueにする変数への値の割り当て
(付値 valuation)が存在すること

例．




入力: x, y  Z, (x + y > 2)  ((x < 3)  (y < 2))
出力: Yes (付値の例 x = 2, y = 1)
6
逐次プログラムの検証例 (1/2)
(x, yは整数変数とする)
設計
特性
assume(x + y > 2);
if (b)
x = x +1;
else
x = x + 2;
y = y + x;
x = y + 1;
assert(x < 2);
assume(x0 + y0 > 2);
if (b0)
x1 = x0 +1;
else
x2 = x1 + 2;
y1 = y0 + x2;
x3 = y1 + 1;
assert(x3 < 2);
1変数は1度しか更新
されないように変数の
名前を付けかえる
7
逐次プログラムの検証例 (2/2)
assume(x0 + y0 > 2);
if (b0)
x1 = x0 +1;
else
x2 = x1 + 2;
y1 = y0 + x2;
x3 = y1 + 1;
assert(x3 < 2);
 y0 + x0 > 2

 b0  x1 = x0 +1
 b0  x1 = x0

 b0  x2 = x1 + 2
 b0  x2 = x1
 y1 = y0 + x2
 x3 = y1 + 1
 (x3 < 2)
充足可能 ⇔ 言明を満たさない実行が存
在
8
充足可能性判定の実行

SAT/SMT Solverを利用

例．Yices @ SRI
 y0 + x0 > 2

 b0  x1 = x0 +1
 b0  x1 = x0

 b0  x2 = x1 + 2
 b0  x2 = x1
 y1 = y0 + x2
 x3 = y1 + 1
 (x3 < 2)

一定の長さの実行を検査
有界(Bounded)モデル検査
% cat sample.txt
(define b0::bool)
(define x0::int)
(define x1::int)
(define x2::int)
(define x3::int)
(define y0::int)
(define y1::int)
(assert
(and
(> (+ y0 x0) 2)
(or
(and b0 (= x1 (+ x0 1)))
(and (not b0) (= x1 x0))
)
(or
(and (not b0) (= x2 (+ x1 2)))
(and b0 (= x2 x1))
)
(= y1 (+ y0 x2))
(= x3 (+ y1 1))
(not (< x3 2))
)
)
(check)
% yices –e sample.txt
9
式の表現力
ブール式
Separation Formula
整数か実数（一方のみ），(x – y > c)の論理結合
ブール式 + 背景理論
計算量 NP完全
SAT solvers
O. Strichman et al., “Deciding
Separation Formulas with SAT,”
CAV 2002.
SMT solvers
例．整数，実数，加減算大小比較
Presburger Arithmetic
整数，加減算，限量子(一階)
計算量O(22^n)
ツール例．Omega Library
ディオファントス方程式
決定不能
10
SAT Solver
SMT (Satisfiability Modulo Theories) Solver

SAT Solver:ブール式の充足可能性判定器

高速なヒューリステックアルゴリズム


ブール式以外の変数の表現


MiniSAT, Zchaff, Grasp, …
複数のブール変数からなるビットベクトル
SMT Solver: 「ブール式＋背景理論」を扱う


Yices, CVC3, Z3,…
種々の背景理論（組み合わせても良い）

配列，Linear Arithmetic (整数and/or実数の加減算大小
比較)，ビットベクトル
11
逐次プログラムのモデル検査
CBMCでの手順
CBMC: ANSI C Model Checker (SATを利用)


E. Clarke et al., “A tool for checking ANSI-C programs,” TACAS 2004.
4.
ネストしたループの解消
ループの削除
変数のRenaming
論理式への変換

他の方法も大体同じ
1.
2.
3.

if, if-else のみに
変換
A. Armando et al., “Bounded model checking of software using SMT
solvers instead of SAT solvers,” J. Softw. Tools & Technol.
Transfer, 2009.
12
1. ネストしたループの解消

ループの展開（手順2）でのプログラムのBlow
upを避ける

仮想的なプログラムカウンタ (vpc) を導入
while (B1) {
S1;
while (B2) {
S2;
}
}
while (vpc <= 2) {
switch (vpc) {
case 1:
if (B1) { S1; vpc = 2; }
else vpc = 3;
break;
case 2:
if (B2) S2 else vpc=1;
break;
}
}
13
2. ループの削除

ループを展開

最大何回展開するかはユーザが入力

例．繰り返しが最大3回の場合
while (b) {
S;
}
最後はassert(!条件)に置
き換える
→ ループが指定回数以上
実行される可能性を検出

if (b) {
S;
if (b) {
S;
if (b) {
S;
assert(!b);
}
}
}
for, 後ろ向きのgoto,関数の再帰呼び出しも同様に変換
14
変数のRenamingと論理式への変換
x = x + y;
if (x != 1) {
x = 2;
if (z) x++;
}
assert(x<=3);
静的単一
代入(SSA)
とほぼ同じ
x1 = x0 + y0;
if (x1 != 1) {
x2 = 2;
if (z0) x3 =x2 + 1;
}
assert(x3<=3);
 x1 = x0 + y0
 x2 = ite(x1  1, 2, x1)
 x3 = ite(x1  1  z0, x2 + 1, x2)
 (x3  3)
15
論理式への変換

SATの場合ー CNF (Conjunctive Normal
Form)のブール式に変換




変数: 複数のブール変数によるベクトル
演算(+,-,*,/など）: 演算回路
任意のブール式は，充足可能性を保存して線形の大
きさのCNFに変換可能
SMTの場合

1プログラム変数を1変数で表現可能


背景理論：ビットベクトル
背景理論：Linear Arithmetic (上限のない整数,実数変数)
16
SAT vs. SMT

SMTが優れる場合

背景理論によって式がコンパクトになる場合

例．配列を多用する場合

Primのアルゴリズム (最小スパニング木の計算, 4ノード)
時間(sec)
辺の数
A. Armando et al., “Bounded model checking of software using SMT
solvers instead of SAT solvers,” J. Softw. Tools & Technol. Transfer, 2009.
17
適用事例

ANSI C の検証

CBMC @CMU


E. Clarke et al., “A tool for checking ANSI-C
programs,” TACAS 2004.
PHPプログラムの脆弱性検出

@National Taiwan Univ.

Y.W. Huang et al., “Verifying web applications using
bounded model checking,” DSN 2004.
18
Part II
並行システムのモデル検査
19
並行システム

モデル検査の主たる対象


通常は停止しない (リアクティブシステム)
検証の関心



アルゴリズム (cf. 実際のコード)
制御に関する正しさ (cf. データ)
モデル検査問題の入力


設計：アルゴリズム
性質 (仕様)：時相論理 (ex. LTL, CTL)

有界モデル検査ではLTLを扱う
20
例．相互排除（２つの並行プロセス）
設計
状態：(pc0, pc1, t)
P0::
0: while True {
1: wait (t = 0)
2: t = 1;} // CS
0,0,1
0,0,0
0,1,0
P1::
0: while True {
1: wait (t = 1)
2: t = 0;} // CS
2,0,0
1,1,0
1,0,1
0,1,1
1,0,0
2,1,0
1,1,1
0,2,1
1,2,1
特性 (時相論理LTL, G：「常に」，F: 「いつか」)
•相互排除
G¬((pc0 = 2)(pc1 = 2))
Yes
G(pc0 = 1→Fpc0 = 2)
No!
•スタベーションフリー(P0側)
21
システムの記号表現ー記号モデル検査
の基礎
状態：(pc , pc , t)
0

システムの数学的表現

形式的な仕様記述にも有用


0,0,1
0,0,0
0,1,0
2,0,0
1,1,0
1,0,1
0,1,1
1,0,0
1,1,1
0,2,1
2,1,0
1,2,1
状態とは？

グラフ表現:頂点


TLA, TLA+ (by Lamport)
1
記号表現:変数への付値
例．pc0 = 0, pc1 = 2, t = 1
遷移とは？

グラフ表現:辺

記号表現:変数とそのコピーへの付値
例．pc0 = 0, pc1 = 2, t = 1, pc‘0 = 1, pc‘1 = 2, t‘ = 1
22
記号表現：状態集合
P0::

状態集合S

S = True  sS が付値


0: while True {
1: wait (t = 0)
2: t = 1;} // CS
状態集合とその記号表現を同一視
P1::
0: while True {
1: wait (t = 1)
2: t = 0;} // CS
例．初期状態集合

I = {(pc0,pc1, t)=(0, 0, 0), (0, 0, 1)}
0,0,1
0,0,0

記号表現
I := pc0=0  pc1=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
23
記号表現：遷移関係


P1::
変数とそれらのコピー上の論理式
T = True  (s, s’)T が付値
0: while True {
1: wait (t = 1)
2: t = 0;} // CS
例．P0の0行
G1 := pc0=0
T1 := G1 pc’0=1  pc’1=pc1 t’ =t

0: while True {
1: wait (t = 0)
2: t = 1;} // CS
遷移関係T (遷移の集合)


P0::
遷移関係全体
0,0,1
0,0,0
0,1,0
T :=T1T2… Tn 
¬(G1 … Gn )pc’0=pc0pc’1=pc1t’=t
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
実行できる命令がないなら「次状態 = 現状態」
記号表現は設計から直接得られる (状態探索は不要)
(むしろ設計そのもの)
24
記号表現: システム

システム＝状態機械




変数の集合 (状態空間を規定)
初期状態集合I
遷移関係T
3要素によりシステムの動作を完全に記述
記号表現のメリット・・・記号モデル検査

BDDを用いたモデル検査 (1990年ころ)


Burch et al., “Symbolic model checking: 1020 states and beyond,”
LICS 1990.
SATを用いたモデル検査 (1999年ころ)

A. Biere et al., “Symbolic model checking without BDDs,” TACAS
1999.
25
有界モデル検査 (SATを利用)

初期状態からk回の状態遷移を検査


例：到達可能性の判定
I(0)  T(0,1)  …  T(k-1,k)  (P(0)…P(k))
が充足可能 ⇒ Pが成り立つ状態に到達



k回の遷移をブール値の式で表現
I(0): Iの各変数varをvar0に置き換え
T(i, i+1):Tの各変数varをvariに, var’をvari+1に置き
換え
検査する特性としては，任意のLTL式を扱える
26
例．



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が成り立つ状態に到達
27
手法の完全性

充足不能の場合

「Pが成り立つ状態に到達しない」とは結論できない

kを増やすと充足するかもしれない
for (k = 0, 1, 2, 3, …) {
res <- Sat(I(0)  T(0,1)  …  T(k-1,k)  P(k));
if (res = True)
return “reachable”;
}

k は状態グラフの直径までしらべればよい，しかし，


直径を知るのに手間がかかる
kが大きくなると時間が増加する
28
狭義の記号モデル検査 (BDD (2分決定グ
ラフ)を利用)

BDD: 論理関数を表現するデータ構造



ハードウェアの場合，システムの構造に規則性があることが多く，対
応するBDDが非常に小さくなることが多い．
状態集合と遷移関係を表すBDDをつかって，
状態の幅優先探索が可能


高速な演算処理アルゴリズムが存在
f(x, y) = x ¬x y
検証の完全性
x
代表的なモデル検査ツール


0
SMV (@CMU)
NuSMV

1
y
SATを使う有界モデル検査も実装
1
0
0
29
1
有界モデル検査の長短

長所



初期状態に近い状態を効率良く検証
充足する場合は速い（Bug Huntingに効果的）
短所


時間がかかる
完全な検証のためには大きなkが必要


式が大きくなり時間がかかるため検証が困難
十分なkを知るのが困難
30
Part III
有界から無界へ
31
無界モデル検査
Unbounded Model Checking

有界から無界へ

検査する範囲を状態空間全体に拡張
✔1. K-Induction

2.
L. de Moura et al., “Bounded Model Checking and
Induction: From Refutation to Verification,”
CAV 2003.
Craig’s Interpolant
32
K-Induction


目的: 性質Vが常に成立するか否かを判定
手法:以下の2条件を示す
初期状態からのk状態で性質Vが常になりたつ
1.

連続するk状態で性質Vが成り立っているなら，
k+1番目の状態でもVが成り立っている
2.



I(0) T(0,1) …T(k-2,k-1)  (V(0) … V(k-1))
が充足不能
V(0) … V(k-1)  T(0,1)  … T(k-1,k)  V(k)
が充足不能
1, 2 ⇒ Vが常になりたつ
SALモデル検査器でサポート
33
適用事例：コンセンサスアルゴリズムのモ
デル検査

コンセンサスアルゴリズム

耐故障分散アルゴリズムの一種

Paxos (by Lamport)



Chubby lock system @ Google
Practical Byzantine Fault Tolerance (by Castro &
Liskov)
全ノードを同じ決定にみちびく


各ノードが値を提案
全ノードが同じ提案値を選択・決定
34
コンセンサスアルゴリズムの特徴

全プロセスが決定するまで無期限にラウンドをくりか
えす


メッセージの遅延，故障に耐えるため
検証では無限のラウンドを扱わなければならない


手法1: 有限状態への抽象化 (SRDS 2007)
手法2: K-Induction (DISC 2008)
P1
P2
P3
v1,0
u1:= 1
v1
Ack
e1:= v1
u1:= 0 v ,0
2
r1:= 1
v1
Ack
e2:= v2
u2:= 0 v3,0
r2:= 1
e3:= v3
u3:= 0
r3:= 1
v1
e2:= v1
u2:= 1
Ack
e3:= v1
u3:= 1
35
実験結果
(The LastVoting/Paxos Algorithm)
実行時間 (sec)
SPIN
ALV
手法１．
通常のモデル検査(NuSMV)
+ 有限状態への抽象化
手法2. SMT (Yices) + K-Induction
ノード数
36
無界モデル検査
Unbounded Model Checking

1.
✔2.
有界から無界へ
K-Induction
Craig’s Interpolant

K. McMillan, “Interpolation and SAT-Based Model
Checking,” CAV 2003.
37
Craig’s Interpolant

F  Gが充足不能な場合，
FとGのInterpolant IP が存在
F ⇒ IP
IP  G は充足不能
IPの変数は FとGに共通
1.
2.
3.

例

F := p  q, G := : q  r  s, Ip := q
38
Interpolantによる状態探索 (Pへの可到性)
k = 0からスタート
I(0)  T(0,1)  …  T(k-1,k)  P(k)
1.


充足可能: 「Reachable」
充足不能: kステップ目の状態ではPは成り立たない
F:= I(0)T(0,1), G:=T(1,2) …T(k-1,k)  P(k),
IP := FとGのInterpolant
IPはIから1ステップで行ける状態集合の
Overapproximation
2.
1.
2.
3.
F ⇒ IP
IP  G は充足不能
IPの変数は FとGに共通
I
1ステップ後
の状態
39
Interpolantによる状態探索
R <- I  IP
R(0)  T(0,1)  …  T(k-1,k)  P(k)
3.


充足可能: k <- k + 1. 手順1へ
充足不能: 手順4へ．
F:= R(0)T(0,1), G:=T(1,2) …T(k-1,k)  P(k),
IP := FとGのInterpolant
R <- R  IP
4.


Rが変化しない: 「到達しない」
Rが増加：手順3へ．
R
Rから
1ステップ後
の状態
40
適用例

電話通信サービスの競合問題検出


提案手法



電話通信サービス向きの記号表現
Interpolant (ツールFOCI)
従来法1


T. Matsuo et al., “Feature Interaction Verification Using Unbounded
Model Checking with Interpolation,” IEICE Trans. Info & Syst, 2009.
Interpolant (ツールFOCI) + 通常の記号表現
従来法2

Spin (状態グラフを扱うモデル検査ツール)
41
実験結果
•競合あり = 充足する場合: 提案手法は高速
•充足しない場合: Spinの方が速い
42
Part IV
まとめ
43
まとめ

SAT/SMTソルバを利用したモデル検査



逐次プログラム
並行システム
非界モデル検査
44

Download Report