Subscribed unsubscribe Subscribe Subscribe

MacBookAir欲しい日記改めSpinを使ったモデル検査入門

明けましておめでとうございます.今日はMacBookが欲しいので日本語の情報がちょっと少ないので,修論関係で触っているモデル検査ツール,Spinについて軽くまとめてみます.

モデル検査とは

厳密さに欠ける言い回しでアレですが,「間違いなく正しく動くソフトウェア」が欲しいときにどうするか.テストはバグの早期検出に有効ですが,テストで得られるのは
「テストで検査した範囲においてソフトウェアが仕様を満たす」
という結論であって,当然
すべての範囲においてソフトウェアが仕様を満たす」
ことではありません.たとえば人工衛星みたいなクリティカルな組み込み分野だと,「そのコードで『人工衛星の角速度が発散しない』ことを証明できるのかねキミ?衛星はメンテナンスできないってこと位分かってるよね?」とか言われた日には,テストケースを書いた我が脳味噌の完璧さに全てを賭けるか,泣きながら宇宙服の調達を開始するかの二択を迫られることになります….

しかしながら後者の結論を得るには,よほど単純なコードでも無い限りは総当たりによる検査を行わざるを得ません*1.モデル検査とは,その総当たりを実際に行ってしまい,「間違いなく正しく動く」ことを証明したり,満たされない場合の反例ケースを探し出したりすることが可能になる手法です.
但し力ずくで全状態空間を探索することもあって,実際には検査する対象はソースコードではなくそのモデルであることに注意が必要です.プログラマはシステムを忠実に表現し,かつ充分に簡潔なモデルをコードとは別に用意する必要があります*2

Spin

ともかく,今回はSpinというモデル検査ツールを使って,簡単な検証を行ってみます.環境の導入はSpinのインストールなどを参考にすれば簡単*3.SpinではPromelaというモデル記述言語を使ってシステムをモデル化します.とりあえず,ある変数iを1つインクリメントするだけのPromelaモデルを書いてみます.

int i = 0;

active proctype P(){
   printf("hello,world!");
   i++;
}

Promelaの文法はC言語的で,実際コンパイル時にはCプリプロセッサを最初に呼び出すため,#includeや#define文なんかが普通に使えます.ただしモデル記述言語であるために,あまり高度なことはできません.オブジェクト指向どころか,関数呼び出しも浮動小数もサポートしない男前っぷり*4…!それ故文法はとても簡単なのですが,ここでは文法の参考になりそうなページを纏めておくにとどめます.

Promela Manual Pages -- Index
公式マニュアル(英語).当然一番詳しい.
0.PROMELAの基本文法
初心者向け解説.
http://www002.upp.so-net.ne.jp/mamewo/spin.html
Promelaのサンプルコードなど.
SPINによるモデル検査
Spin入門のスライド.
ツール:SPIN(Promela言語) - 佐々研・PukiWiki
Spin/Promelaに関するメモ.後半は割と悲哀にあふれている….

線形時相論理

モデル検査を行うためには,モデルに対する検査式の記述が必要です.Spinでは線形時相論理(LTL)というものを使います.
線形時相論理 - Wikipedia
LTLがとても強力なのは,「いつかAが真になる」とか,「Aが真になるまでの間,Bは真である」といった表現が簡単にできる点.SpinにおけるLTL式の表記を下にまとめておきます.下4つがLTLに特有の記号(詳しくはWikipediaなどを参照).たとえば「iがいつか1になる」をSpinで表現すると「<>(i==1)」となります.「iが0になったら,その後は必ず0→1→2→3と推移する」という性質は,i==nという論理式をqnと定義すると,「G( q0 -> ( ( q1 U q2) U q3) )」というUntilの入れ子で表現できます.

記号/結合子意味Spinでの記法
\wedgeand&&
\veeor||
\negnot!
\rightarrowimp->
G常に〜が成立する(Globally)[]
Fいつか〜が成立する(Finally)<>
U〜となるまで…が成立する(Until)U
X次の時点で〜が成立する(Next)X

例:モデル記述

では,さっそく例を考えてみます.「応募を表明したユーザーの中から抽選で1名にMacBookが当たる」というキャンペーンを想定してみましょう.こんなモデルを作ってみます.

01: /* campaign.pml */
02: bool want_iMac[2];
03: bool get_iMac[2];
04: bool campaign = true;
05: 
06: active [2] proctype User() provided(campaign){/*campaign==trueのときにだけ実行可能なプロセス*/
07:   do
08:   :: want_iMac[_pid] = true;
09:        printf("MacBook Air 11インチ欲しい!");
10:   :: want_iMac[_pid] = false;
11:        printf("MacBook Air 11インチ欲しくない…");
12:   od
13: }
14: 
15: active proctype Hatena(){
16:   do
17:   :: 
18: 	campaign = false;/*キャンペーン終了*/
19: 	if
20: 	::want_iMac[0] ->/*0が当選*/
21: 		get_iMac[0] = true;
22: 		get_iMac[1] = false;
23: 	::want_iMac[1] ->/*1が当選*/
24: 		get_iMac[0] = false;
25: 		get_iMac[1] = true;
26: 	::else ->/*応募者が0*/
27: 		get_iMac[0] = false;
28: 		get_iMac[1] = false;			
29: 	fi;
30: 	campaign = true;/*次のキャンペーン開始*/
31:   od
32: }

Userプロセスが2つ,Hatenaプロセスが1つ存在しており,どれもactive宣言(つまり,初期状態から実行可能)されています.Promela言語は実行可能なプロセスの中から非決定的に次のプロセスを選択して1行進めていきます.User[0]の7行目を実行→Hatenaの16行目を実行→User[1]の7行目を実行…といった感じ.
do...odやif...fiブロックで囲んだ構文はPromelaに独特の非決定的な分岐選択文で,->符号左側の式が真と評価されたものの中から,ランダムに分岐先が選択されます(左辺が省略された場合は常にtrue).これも詳しくはPromela言語のリファレンスを参考に.それぞれのプロセスの動作を日本語で表現すると,以下のような感じでしょうか.

User:「キャンペーンの間,自身に対応したwant_iMacの値をtrueまたはfalseに更新する.」

Hatena:「キャンペーン終了後,iMacを欲しがっているUserから1人を当選者として選び,次のキャンペーンを開始する.但し応募者が0の場合は当選者を選ばない.」

例:LTL式による検査

この懸賞に必要な条件は色々あるはずですが,とりあえずこんな条件式を考えてみましょう.
「当選者の数は常に1名以下である」
これをLTL式で表現すると,「[](get_iMac[0] + get_iMac[1] < 2)」と書けます*5.さっそくこれをSPINでの検証にかけてみます.

spin -a -f "[](get_iMac[0] + get_iMac[1] < 2" campaign.pml
gcc -o pan pan.c
./pan

するとerrors:1と,何と与えたLTL式が満たされないことが判明しました.反例を出力してみます.

spin -g -l -p -r -s -t -X -u250 campaign.pml
Process Statement          want_iM[0] want_iM[1] 
2 Haten 18  campaign = 0   0          1          
Process Statement          campaign   want_iM[0] want_iM[1] 
2 Haten 23  want_iMac[1]   0          0          1          
2 Haten 24  get_iMac[0][0] 0          0          1          
2 Haten 25  get_iMac[1][1] 0          0          1          
Process Statement          campaign   get_iMa[0] get_iMa[1] want_iM[0] want_iM[1] 
2 Haten 30  campaign = 1   0          0          1          0          1          
1 User  10  printf('iMac欲し 1          0          1          0          1          
1 User  11  want_iMac[pid] 1          0          1          0          1          
0 User  9   want_iMac[pid] 1          0          1          0          0          
2 Haten 18  campaign = 0   1          0          1          1          0          
2 Haten 20  want_iMac[0]   0          0          1          1          0          
2 Haten 21  get_iMac[0][0] 0          0          1          1          0          
2 Haten 22  get_iMac[1][1] 0          1          1          1          0 

出力は左から順にプロセスID,プロセス名,ソースの行番号,ソースの内容(一部),その時点における状態量となっています.どうやら,1番が当選した(25行目)次のキャンペーンで0番が当選(21行目)すると,その瞬間に両者とも当選したかのような状態となってしまうようです.この瞬間に当選情報がユーザーに公開されていると,前回の当選情報が残っている1番のユーザーが「【拡散希望】【一人でも多くの人に知ってほしい】【知らないでは済まされない】連続当選なう!」と勘違いtweetを広めてしまう悲劇に見舞われます….atomicというブロックで19〜29行目を囲うと,今度はこのエラーは生じず,LTL式が真であると判定されます.atomicの追加に相当する仕様/実装側の変更(当選判定の計算中は,ユーザーから当選者の確認ができないようにするetc)が必要になることが分かりました.

15: active proctype Hatena(){
16:   do
17:   :: 
18: 	campaign = false;/*キャンペーン終了*/
19:  	atomic{/*atomic内部にいる間は検査式が判定されず,他プロセスも実行されない*/
20: 	if
21: 	::want_iMac[0] ->/*0が当選*/
22: 		get_iMac[0] = true;
23: 		get_iMac[1] = false;
24: 	::want_iMac[1] ->/*1が当選*/
25: 		get_iMac[0] = false;
26: 		get_iMac[1] = true;
27: 	::else ->/*応募者が0*/
28: 		get_iMac[0] = false;
29: 		get_iMac[1] = false;			
30: 	fi;
31:    	}
32: 	campaign = true;/*次のキャンペーン開始*/
33:   od
34: }

まとめ

「仕様の記述」と「モデルの検査」という作業を通じて,

  • あいまいな仕様を明確化させることができる
  • システムの正しさを保証することができる

という2つのメリットを手に入れることが出来ました.先に挙げた例くらいならふつうに気が付けるかもしれませんが,例えばUserプロセスに「ユーザーはいつでもはてなを退会できる」というモデルを追加すると,まだ考え足りない仕様があることに気づきます.
個人的に使ってみた感想としては,非決定的な動作という点にさえ慣れてしまえば,文法的には非常に身に付けやすく,予想以上に低いコストで導入できるなーという感じです.環境も一瞬で整うので,「形式手法」とか「時相論理」なんて固い名称に怖気づかずに,ぜひ気楽にトライしてみるといいんじゃないでしょうか.

参考文献

モデル検査 初級編―基礎から実践まで4日で学べる (CVS教程)

モデル検査 初級編―基礎から実践まで4日で学べる (CVS教程)

ところで

応募方法はかんたん。あなたのブログ(はてなダイアリー)に、「MacBook Air 11インチ欲しい!」と書きこむだけで、応募完了です。応募の際には、MacBook Airや今年のブログ生活にかける、あなたの想いをぜひ書きこんでください!

MacBook Air 11インチ欲しい!とは - はてなキーワード

と書いてあったのでコード中に書いたんですが,認識されていない….これもモデル検査で検出できる類の仕様の曖昧さかと思います(ドヤ顔).というわけで改めてMacBook Air 11インチ欲しい!

ちょっと細かい話:公平性の検証

<>(get_iMac[0] -> true)というLTL式を考えてみます.これは「応募し続ければいつか0番にiMacが当たる」という意味になります.先のモデルによればキャンペーンは無限回試行されているので,これは直観的に満たされそうな気がしますね.ところが,無情にもこの式は偽と判定されてしまいます….反例を見てみましょう.

Process Statement          campaign   get_iMa[0] get_iMa[1] want_iM[0] want_iM[1] 
2 Haten 32  campaign = 1   0          0          1          0          1          
1 User  10  want_iMac[pid] 1          0          1          0          1          
2 Haten 18  campaign = 0   1          0          1          0          0          
2 Haten 27  else           0          0          1          0          0          
2 Haten 28  get_iMac[0][0] 0          0          1          0          0          
2 Haten 29  get_iMac[1][1] 0          0          1          0          0          
2 Haten 32  campaign = 1   0          0          0          0          0          
0 User  9   want_iMac[pid] 1          0          0          0          0          
1 User  9   want_iMac[pid] 1          0          0          1          0          
2 Haten 18  campaign = 0   1          0          0          1          1          
2 Haten 24  want_iMac[1]   0          0          0          1          1          
2 Haten 25  get_iMac[0][0] 0          0          0          1          1          
2 Haten 26  get_iMac[1][1] 0          0          0          1          1          
2 Haten 32  campaign = 1   0          0          1          1          1          
1 User  9   want_iMac[pid] 1          0          1          1          1          
1 User  10  want_iMac[pid] 1          0          1          1          1          
0 User  9   want_iMac[pid] 1          0          1          1          0          
<<<<<START OF CYCLE>>>>>
1 User  9   want_iMac[pid] 1          0          1          1          0          
2 Haten 18  campaign = 0   1          0          1          1          1          
2 Haten 24  want_iMac[1]   0          0          1          1          1          
Process Statement          campaign   get_iMa[0] get_iMa[1] want_iM[0] want_iM[1] 
2 Haten 25  get_iMac[0][0] 0          0          1          1          1          
2 Haten 26  get_iMac[1][1] 0          0          1          1          1          
2 Haten 32  campaign = 1   0          0          1          1          1          
1 User  9   want_iMac[pid] 1          0          1          1          1          
1 User  10  want_iMac[pid] 1          0          1          1          1          
0 User  9   want_iMac[pid] 1          0          1          1          0          
spin: trail ends after 54 steps

<<<<>>>>は,これ以下の状態が無限に繰り返されるということを意味します.かわいそうなことに,1番が無限回当選し,0番は一度も当選できないケースがあるという結果に….これは景品法違反でもSpinのバグでも無く,Spinによる検証が「強公平性」を満たさないことによる正当な動作です.

弱公平性:文が常に実行可能であれば,その文はいつか必ず実行される.
強公平性:文が無限回実行可能であれば,その文はいつか必ず実行される.

上の検査では,jSpinのデフォルトである「弱公平性」を有効にする-fオプションを有効化しています.仮に弱公平すら満たさないと仮定すると,結果は更に悲惨です.

<<<<<START OF CYCLE>>>>>
2 Haten 18  campaign = 0   
Process Statement          campaign   
2 Haten 27  else           0          
2 Haten 28  get_iMac[0][0] 0          
2 Haten 29  get_iMac[1][1] 0          
2 Haten 32  campaign = 1   0          
spin: trail ends after 7 steps

Userプロセスが応募を表明する暇もなく,Hatenaプロセスは無限回の抽選を実施してしまいました.プログラム開始時点ではUser[0],User[1],Hatenaのいずれも実行可能な文(do)を指しています.弱公平性が満たされている元では,実行可能な状態にあるプロセスはいつか必ず実行されるので,上のような事態には陥りません(これは本来の仕様と合致する動作でもある).

*1:「仕様Aが常に真である」というような恒真問題は一般的にco-NP問題であるから,決定性チューリング機械によって多項式時間で解くことはできないとか何とか

*2:モデルからコードを生成する試みも色々と行われているようです

*3:1つだけ追加すると,公式のGUI環境(iSpin/XSpin/jSpin)でモデルを書くより,Emacspromela-mode.elを使ったほうが100倍効率的

*4:ただしマクロ的に展開されるインライン関数を使ったり,C言語のソースを埋め込むことはできる.詳しくは公式マニュアル参照

*5:Promelaにおけるbool型はbyteのシンタックスシュガーなので,true + trueは2と評価される