モデル検査（３） 手続き型言語に基づくモデリング

Presentation on theme: "モデル検査（３） 手続き型言語に基づくモデリング"— Presentation transcript:

1 モデル検査（３） 手続き型言語に基づくモデリング
表現系工学特論 モデル検査（３） 手続き型言語に基づくモデリング １．NuSMVによるモデリング ２．SPINによるモデリング 参考文献 4日で学ぶモデル検査　初級編，産業技術総合研究所システム検証センター，ＮＴＳ(2006)

2 モデル検査の概要(復習) モデル検査器 検査結果 モデル model checker model ＯＫ （状態遷移系） 反例 モデル記述言語
モデル検査の概要(復習) 　　 モデル検査器 model checker 検査結果 モデル model （状態遷移系） ＯＫ 反例 モデル記述言語 C言語風のもの プロセス代数 性質 property （安全性，活性） The result is either OK or a counterexample 性質の記述 時相論理

3 １．NuSMVによるモデリング NuSMVの概要 例題：スイッチシステム

4 NuSMVの概要(1/3) SMV（Symbolic Model Verifier:カーネギーメロン大学開発）の再実装 モデリング 検証
代入文やcase式からなる簡単な言語によって，各状態に現れる変数の変化を一元的に制御 電子回路のようなシステムの記述に適している 検証 線形時相論理（LTL）と計算木論理（CTL）で性質を記述

5 NuSMVの概要(2/3) 全体の構造 MODULE モジュール名 VAR 変数宣言部 ASSIGN 遷移記述部 LTLSPEC
検査式記述部

6 NuSMVの概要(3/3)代入文とcase式
<変数名>:=<式> case式 case <条件> : <式>; <条件> : <式>; : <式>; esac; 上から順に＜条件＞を評価する． 最初に真(=1)となる＜条件＞に対応する＜式＞の値を返す．

7 例題：スイッチシステム(1/10) 概要 １ ０ 変数a,bは0,1,2いずれかの値をとる． スイッチはonまたはoffの２状態をとる．

8 スイッチシステム(2/10) 動作仕様 変数a,bは同期して値が変化する．
変数bも0→1→2→0と繰り返して変化する． ただし，a=bのときは次の時点でもその値を保ち変化しない．初期状態は0とする． スイッチは，a=b=2なら次の時点でonとなり，a=b=1なら次の時点でoffとなる．それ以外の場合は次の時点でもその値を保ち変化しない．初期状態はoff とする．

9 スイッチシステム(3/10) 検査項目 スイッチがoffならば，いずれonになる． スイッチがonならば，いずれoffになる．

10 スイッチシステム(4/10) 紙の上でのモデル検査
状態＝(aの値，bの値，スイッチの状態) スイッチがoffならば，いずれonになる (0,0,off) 成り立つ (1,0,off) スイッチがonならば，いずれoffになる bは　a=bのときは 変化しない (2,1,off) 成り立たない (2,2,off) aは　b=1のときは 変化しない (0,2,on) (2,2,on) スイッチは　a=b=2ならon (1,0,on) (2,1,on)

11 スイッチシステム(5/10) 変数宣言 ---- SWITCH.smv MODULE main VAR a : { 0, 1, 2};
b : { 0, 1, 2}; sw : { on, off };

12 スイッチシステム(6/10) 遷移記述 ASSIGN
init(a) := 0; next(a) := case b = 1: a; : (a+1) mod 3; esac;

13 スイッチシステム(7/10) 遷移記述（続） init(b) := 0; next(b) := case a = b: b; : (b+1) mod 3; esac; init(sw) := off; next(sw) := case a = 2 && b = 2: on; a = 1 && b = 1: off; : sw; esac;

14 スイッチシステム(8/10) 線形時相論理 線形時相論理 LTL 時相論理式 読み方 解釈 Gp Globally p Always p
(Linear Temporal Logic) 詳しくは次回 線形時相論理　LTL 状態遷移系における任意の１本の計算経路を考える ．．． 時相論理式 読み方 解釈 Gp Globally p Always p pがいつでも成り立つ Fp Finally p Future p Eventually p pがいつか成り立つ

15 スイッチシステム(9/10) 検査式記述 スイッチがoffならば，いずれonになる G(sw = off → F(sw = on))
成り立つ 成り立たない off off on on off LTLSPEC G(sw = off -> F(sw = on)) LTLSPEC G(sw = on -> F(sw = off))

16 スイッチシステム(10/10) モデル検査 $ NuSMV SWITCH.smv
-- specification G(sw = off -> F sw = on) is true -- specification G(sw = on -> F sw = off) is false -- as demonstrated by the following execution sequence Trace Type: Counterexample -> State 1.1 <- a = 0, b = 0, sw = off -> State 1.2 <- a = 1 -> State 1.3 <- a = 2, b = 1 -> State 1.4 < b = 2 -> State 1.5 <- a = 0, sw = on -- Loop starts here -> State 1.6 <- a = 1, b = 0 -> State 1.7 <- a = 2, b = 1 -> State 1.8 < b = 2 -> State 1.9 <- a = 0 -> State 1.10 <- a = 1, b = 0 変化した変数 だけを表示 ループの入り口 ループの入り口 の状態に戻っている

17 SPINの概要 Promelaの基本 例題：スイッチシステムの記述

18 SPINの概要 SPIN (Simple Promela Interpreter)：ベル研究所が開発 モデリング 検証
Ｃ言語風のPromela (Process Meta-Language)で各プロセスを記述 分散システムの検証に適している 検証 線形時相論理LTLで性質を記述 その他の機能も豊富

19 Promelaの基本(1/4) 全体の構造 mtype = .... int ... inline ... proctype ...
メッセージ型の宣言 変数宣言 マクロの定義 プロセス型の定義

20 Promelaの基本(2/4) atomic文
} インタリーブされずに常に連続して実行してほしい文(atomic action)は，atomicで囲む． モデルの状態数削減に役立つ．

21 Promelaの基本(3/4) 選択文 if ::<ガード> -> <処理> ．．．．．．．．
::<ガード> -> <処理> fi すべての<ガード>の実行可能性（trueなら実行可能）を評価する． 実行可能な<ガード>を１つ非決定的に選び， それに続く<処理>を実行する． 実行可能な<ガード>がないときは， いずれかの<ガード>が実行可能になるまでプロセスの実行が中断(block)し，その後，実行可能になってから実行を再開する．

22 Promelaの基本(4/4) 反復文 do ::<ガード> -> <処理> ．．．．．．．．
::<ガード> -> <処理> od if ... fi と同様の動作をする． <ガード>に続く<処理>を実行した後，doに戻って同様の動作を繰り返す． ループから出るときには break を使う．

23 例題：スイッチシステム(1/6) 概要 再掲 １ ０ 変数a,bは0,1,2いずれかの値をとる． スイッチはonまたはoffの２状態をとる．

24 スイッチシステム(2/6) 状態遷移モデル 変数 a,b,swに初期値を代入する． 変数 a の次の値Naを決める．
b==1ならば，Na=a b!=1ならば， Na=(a+1) % 3 変数 b の次の値Nbを決める． a==bならば，Nb=b a!=bならば， Nb=(b+1) % 3 変数 sw の次の値Nswを決める． a==b==2ならば，Nsw=on a==b==1ならば，Nsw=off それ以外のとき， Nsw=sw % は剰余（余り）を求める演算

25 スイッチシステム(3/6) メッセージ型と変数の宣言
スイッチシステム(3/6) メッセージ型と変数の宣言 この例題では，メッセージをユーザ定義シンボルとして利用 /* switch.pml */ mtype = {on, off}; int a, b, Na, Nb; mtype sw, Nsw;

26 他のどのガードも実行可能でないときに，else が実行可能
スイッチシステム(4/6) プロセスの定義 active proctype switch() { a = 0; b = 0; sw = off; do :: true -> if ::(b==1) -> Na = a :: else -> Na = (a+1)% fi; 他のどのガードも実行可能でないときに，else が実行可能

27 スイッチシステム(5/6) プロセスの定義 if ::(a==b) -> Nb = b :: else -> Nb = (b+1)% fi; if ::(a==2 && b==2) -> Nsw = on ::(a==1 && b==1) -> Nsw = off :: else > Nsw = sw fi; atomic{a = Na; b = Nb; sw = Nsw } od }

28 スイッチシステム(6/6) モデル検査 SPINでは次のように入力する： Gの代わりに □ （タイピングは[]）
Fの代わりに ◇ （タイピングは<>） スイッチがoffならば，いずれonになる G(sw = off → F(sw = on)) #define p sw==off #define q sw==on [](p -> <>q)

29 演習問題 　図のような電気回路がある．スイッチにはonとoffの状態がある．スイッチにはそれぞれにタイマが付いている．（スイッチnにはタイマnが付いている．） 　各タイマは各時点で１だけカウントアップし，最大値になったら次の時点で１に戻る．タイマの最大値は，タイマ１が５，タイマ２が４，タイマ３が６，タイマ４が３である． 　タイマの初期値は，タイマ１が２，タイマ２が３，タイマ３が１，タイマ４が２である． 　各スイッチは，対応するタイマが最大値になると，次の時点でonとなる．それ以外のときはoffとなる． 　このモデルをNuSMVまたはPromelaで記述せよ．また，「豆電球が消灯していれば，いずれ豆電球が点灯する」という性質をＬＴＬで記述せよ．命題の論理積と論理和には，C言語等と同様に，&&と||を使用できるので，それを利用すること． 1 2 3 4