モデル検査のためのコンカレントシステムの仕様記述

Presentation on theme: "モデル検査のためのコンカレントシステムの仕様記述"— Presentation transcript:

1 モデル検査のためのコンカレントシステムの仕様記述
土屋達弘 (大阪大学)

2 日本語でよめるモデル検査関連の文献 米田，梶原，土屋，ディペンダブルシステム， 共立出版，2005.
電子情報通信学会ハンドブック／知識ベース， ７群１編「ソフトウェア基礎」 土屋，菊野，”モデル検査入門,” 計測と制御，2009. 他．Amazonで検索

3 モデル検査とは 形式的検証手法 入力: 設計 + 特性 (仕様) 出力: Yes or No 方法: 状態探索 モデル検査器 状態機械 設計
2007 Turing Award　(Clarke, Emerson, Sifakis)  入力: 設計 + 特性 (仕様) 出力: Yes or No 方法: 状態探索 モデル検査器 状態機械 設計 Yes No (＋反例) 特性 (仕様)

4 コンカレントシステムとは 並行に処理が実行されるシステム 通常は停止しない (リアクティブシステム) 講演者の教育経験
大阪大学・大学院前期課程 組込み適塾 プログラムを中心に 講義

5 マルチスレッドのプログラム 例：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;

6 状態遷移モデル 状態遷移モデル 初期状態集合 遷移関係(遷移集合) 状態：(pc0, pc1, t) 0: while (true) {
1: while (t != id); // CS 2: t = 1 - t; } 0,0,0 0,0,1 0,1,0 1,0,0 0,1,1 1,0,1 1,1,0 2,0,0 0,2,1 1,1,1 2,1,0 1,2,1

7 システムをどう記述するか コード，擬似コード …  数式  分りやすさ 証明のしやすさ モデル検査（自動検証）のしやすさ
数式  分りやすさ t = 1 t = 1 – t 証明のしやすさ モデル検査（自動検証）のしやすさ TLA by Lamport

8 数式によるシステムの表現 状態とは？ 遷移とは？ グラフ表現:頂点 数式表現:変数への付値
グラフ表現:頂点 数式表現:変数への付値 例．pc0 = 0, pc1 = 2, t = 1 遷移とは？ グラフ表現:辺　 数式表現:変数とそのコピーへの付値 例．pc0 = 0, pc1 = 2, t = 1, pc‘0 = 1, pc‘1 = 2, t‘ = 1 プライムつき変数は，次状態に対応 0,0,0 0,0,1 0,1,0 1,0,0 0,1,1 1,0,1 状態：(pc0, pc1, t) 1,1,0 2,0,0 0,2,1 1,1,1 2,1,0 1,2,1

9 変数と述語 変数 述語 状態変数 プライムつき状態変数 ブール値をもつ式 状態述語: 状態変数上の述語
遷移述語: 状態変数，プライムつき状態変数上の述語

10 数式表現：状態集合 状態集合Sとは？ 例．初期状態集合 状態述語S S = True  sS が付値
I = {(pc0,pc1, t)=(0, 0, 0)} 数式表現 I := pc0=0  pc1=0  t=0 0,0,0 0,0,1 0,1,0 1,0,0 0,1,1 1,0,1 1,1,0 2,0,0 0,2,1 1,1,1 2,1,0 1,2,1

11 数式表現：遷移関係 遷移関係T (遷移集合) とは？ 例．状態変数: x (整数型)のみ 遷移述語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

12 どう数式表現を得るか？ コンカレントシステムの遷移関係を表す数式を，どうやってもとめればよいか？ 数式は設計そのもの

13 動作の表現 コンカレントシステム ひとつひとつの処理 Ti := Guardi  Actioni 並行に処理が実行されるシステム

14 各処理の表現 Ti := 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,0 0,0,1 0,1,0 1,0,0 0,1,1 1,0,1 1,1,0 2,0,0 0,2,1 1,1,1 2,1,0 1,2,1

15 動作全体の表現 各処理iに関する遷移集合 遷移関係全体 遷移関係はtotalでないといけない Ti := Guard1  Action1
T :=T1 T2 …  Tn  ¬(Guard1 … Guardn )pc’0=pc0pc’1=pc1t’=t 遷移関係はtotalでないといけない どの状態についても次状態があること テクニカルな理由による要求 実行できる命令がないなら「次状態 = 現状態」

16 Stuttering遷移 Stuttering遷移 遷移関係をtotalにする別の方法
同じ状態にとどまる遷移 遷移関係をtotalにする別の方法 T :=T1 T2 …  Tn  pc’0=pc0pc’1=pc1t’=t 遷移を付加しても， 多くの性質は保存される Stuttering遷移: 「次状態 = 現状態」 0,0,0 0,1,0 1,1,0 2,0,0 2,1,0 1,0,0 0,1,1 0,2,1 1,1,1 1,2,1 0,0,1 1,0,1

17 擬似コード vs. 数式表現 (Bakeryアルゴリズム)
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);

18 モデル検査とは 形式的検証手法 入力: 設計 + 特性 (仕様) 出力: Yes or No 方法: 状態探索 モデル検査器 状態機械 設計
(＋反例) 特性 (仕様)

19 モデル検査の簡単な歴史 1980頃 1990年代 1998～ 2000年代中～後 最初の研究成果
Partial Order Reduction -> SPIN BDD (2分決定グラフ) > SMV 1998～ SAT (充足可能性判定) 2000年代中～後 SMT 状態グラフを作成，探索 記号モデル検査 状態機械を記号的に表現・操作

20 BDDによる記号モデル検査 (1/2) BDD: ブール式を表現するデータ構造 f = x ¬x y 有限状態に限定すれば，
極めてコンパクトにブール式を表現 高速な演算処理アルゴリズムが存在 有限状態に限定すれば， 状態変数→ブール変数 演算→ブール演算 述語→ブール式 f = x ¬x y x 1 y 1 1

21 BDDによる記号モデル検査 (1/2) S ブール式の演算で幅優先探索が可能 V: 状態変数集合，T： 遷移関係, S: 状態集合
Exist(T(V, V’)  S(V’)) Sへ0歩か1歩でいける状態集合 S  Exist(T(V, V’)  S(V’))　　　　 S  Exist(T, S) Exist(T, S) S

22 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

23 SATを利用したモデル検査 充足可能性判定問題(SAT) （拡張版） 例． 入力：ブール値をもつ式 出力：Yes or No
条件：Yes の必要十分条件は， 式をTrueにする変数への値の割り当て (付値 valuation)が存在すること 例． 入力: x, y  Z, (x + y > 2)  ((x < 3)  (y < 2)) 出力: Yes (付値の例 x = 2, y = 1)

24 SAT Solver / SMT (Satisfiability Modulo Theories) Solver
高速なヒューリステックアルゴリズム MiniSAT, Zchaff, Grasp, … SMT Solver: 「ブール式＋背景理論」を扱う Yices, CVC3, Z3,… 種々の背景理論 （組み合わせても良い） 配列，Linear Arithmetic (整数and/or実数の加減算大小比較)，ビットベクトル

25 有界モデル検査 初期状態から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に置き換え

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 有界モデル検査の長短 長所 短所 初期状態に近い状態を効率良く検証 充足する場合は速い （Bug Huntingに効果的）
メモリの消費量は比較的すくない 短所 時間がかかる 特にコンカレントシステムの場合→　Ogata et al. ATVA’04 完全な検証のためには大きなkが必要 式が大きくなり時間がかかるため検証が困難 十分なkを知るのが困難

28 上限kの解消: Induction 目的: 性質Qが常に成立するか否かを判定 手法:以下の2条件を示す 初期状態で性質Qがなりたつ
I(0)  Q(0) が充足不能 性質Qが成り立っているなら，次状態でも成り立つ Q(0) T(0,1)  Q(1) が充足不能 1, 2 ⇒ Qが常になりたつ

29 アナログ値の扱い 実時間システム，ハイブリッドシステム アナログの変数値をどう扱うか？ 一定時間における増減をひとつの処理とみなす
x_ON:= (at = ON)  t:(t  0  10x’ – 10x  t  5x’ – 5x  t)  (at’ = ON) ON  0.1x 0.2

30 まとめ 数式によるコンカレントシステムの記述と モデル検査 コンカレントシステムの数式表現 BDDによるモデル検査
SAT/SMTソルバによるモデル検査

31 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)