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での記法 |
| and | && | |
| or | || | |
| not | ! | |
| imp | -> | |
| 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教程)
- 作者: 産業技術総合研究所システム検証研究センター
- 出版社/メーカー: ナノオプトメディア
- 発売日: 2009/11
- メディア: 単行本
- 購入: 2人 クリック: 36回
- この商品を含むブログ (1件) を見る
![【楽天ブックスなら送料無料】SPINモデル検査入門 [ M．ベン・アリ ]](http://thumbnail.image.rakuten.co.jp/@0_mall/book/cabinet/2742/27420844.jpg?_ex=128x128 "【楽天ブックスなら送料無料】SPINモデル検査入門 [ M．ベン・アリ ]")
ところで
応募方法はかんたん。あなたのブログ（はてなダイアリー）に、「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
<<<<
弱公平性：文が常に実行可能であれば，その文はいつか必ず実行される．
強公平性：文が無限回実行可能であれば，その文はいつか必ず実行される．
上の検査では，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)でモデルを書くより，Emacsのpromela-mode.elを使ったほうが100倍効率的
*4:ただしマクロ的に展開されるインライン関数を使ったり，C言語のソースを埋め込むことはできる．詳しくは公式マニュアル参照
*5:Promelaにおけるbool型はbyteのシンタックスシュガーなので，true + trueは2と評価される