研究テーマ/検証

Last-modified: 2014-03-13 (木) 20:16:16

形式的検証†

テストと検証†

作成したプログラムに誤りがないか確かめる方法として，主にテストと検証があります．

テスト(test)とは，実際にプログラムを実行し，結果が期待通りかどうか観察することです．もちろん，1～2通り試しただけで誤りがないとは保証できないので，潜んでいる誤りをなるべくたくさん見つけられるよう，テスト内容を設計する必要があります（その方法については例えば下記文献など）．しかしそれでも，タイミングに起因する誤り，滅多にあらわにならない誤り，偶然が重なってあらわになる誤りなどは，テストで発見することが困難です．

G.J.Myersほか『ソフトウェア・テストの技法』第2版, 長尾監訳, 松尾訳, 近代科学社, 2006.
玉井, 三嶋, 松田『ソフトウェアのテスト技法』共立出版, 1988.

↑

モデル検査†

テストでは見つけにくい誤りを見つけるために，「全ての組合せを機械に試させて，エラー状態に到達するかどうか調べる」という方法があります．これがモデル検査 (model-checking) です．

エラー状態の例
- ヌルポインタ参照
- デッドロック
- プログラム中の指定された位置

ERROR: ...

指定された論理式の不成立

assert(x &gt; 0); // x &lt;= 0 ならばエラー

などなど

CPAcheckerによる簡単な検証例

テストとちがうのは「入力の全組合せを考慮して結果を出している」という点です．

↑

抽象化と模型†

そう聞くと，次のような疑問がわくかも知れません．「int型が32ビットだとすると，例えば3つの整数を入力とするプログラムでは組合せは約 43億の3乗通り．現実的な時間で全組合せを調べられるはずがないのでは?」

まったくその通りで，本当に全ての組合せを試していたのでは，どれだけ時間を掛けても検証できません．実際は，抽象化 (abstraction) という技術を使ってプログラムを単純化し，それで得られた模型 (model) を使って，エラー状態に到達するかどうかを調べます．抽象化とは，例えば「各変数を 0 または 1 の1ビットに単純化する」といった操作です．

現実的な時間で自動検証を行うためには抽象化が必要ですが，一方，抽象化のために検証結果が不正確になる（すなわち，元のプログラムは安全なのに，模型は「エラー状態に到達する」と判定される）ことがあります（例えばこちらの検証例の例2）．しかも，そのようなズレの起きない100%正確な自動検証を行うことは，理論的に不可能であることがわかっています*1．従って，検証しようと思っている事柄をなるべく正確に扱えてかつ自動検証が可能な，適切な抽象化を施すことが，モデル検査手法の鍵となります．

研究室では「情報ベースアクセス制御(IBAC)のためのモデル検査法」のような「○○のためのモデル検査法の研究」というタイプの研究テーマをこれまでにいくつか扱いました．「○○」に入るもの（例えば「Webアプリケーション」とか「Javaのセキュリティ機構」とか）の特徴をうまく表していてかつ自動的な解析が可能な模型を，有限オートマトン等，計算モデルと呼ばれるものを組み合わせたり変形したりして構築することが，研究の主な内容になります．

ほかにも，モデル検査をもっと手軽に利用できる仕組みの開発や，仕様通りか調べるだけでなく，仕様に合うようにプログラムを自動変更する研究などにも興味があります．

↑

モデル検査以外の検証法†

検証(verification)（または形式的検証(formal verification)）とは，数理的な方法を使って「プログラムが期待通りの動作をする」ことを保証することです．大きく分けて，定理証明型の検証とモデル検査型の検証があります．

↑

定理証明型検証†

定理証明型の検証とは，文字通り「プログラムが期待通りの動作をする」ことの証明を記述する（あるいは生成する）という方法です．

ここで言う証明とは，アルゴリズムの正当性の証明と同じく，

- 実行開始時にこういう性質が成り立っている．

- 従って1文目の直後はこういう性質が成り立っている．

- 従って2文目の直後はこういう性質が成り立っている．

- …

- 従って最終文の直後はこういう性質が成り立っている．

という形式で，最終文の実行後に「プログラムに期待される動作結果」が成り立っていることを示すものです．

ただし，ループのあるプログラムではもう少しややこしく，数学的帰納法のように「n回目の繰り返し実行後に性質 P が成り立っていれば，(n+1)回目の実行後にも P が成り立つ」というような形式で証明する必要があります（このような性質 P をループ不変式(loop invariant)と言います）．

ここまで聞くと，当然以下のような疑問がわくと思います．

そのような証明を実際に行うのは難しすぎるのでは?
記述した証明に誤りがないかどうかはどう確認するのか?

先に後者について述べると，証明を作成することは難しくても，記述された証明が正しい（つまり証明の各ステップに飛躍がない）かどうか確認するのは比較的簡単で，しかも機械的に行えます．実際，ある決まった記述言語で証明を書けば，それが正しいかどうかは定理証明器と呼ばれるソフトウェアツールで調べることができます．

前者の疑問については，実際には証明を完全に記述しなくても，「最初に成り立っている性質（事前条件）」「最終的に成り立ってほしい性質（事後条件）」「ループ不変式」など，証明の一部分のみ記述すれば，あとは定理証明ツールが途中を補完してくれます（ただし，定理証明ツールの能力には限界があるので，ループ不変式やその他の補題を十分与えないと証明に失敗します）．

↑

例†

下図は，ソフトウェア検証支援環境 Why のマニュアルに記述されているプログラム例です．/*@ … @*/ という部分が，Java Modeling Language (JML)という言語で記述された事前条件(requires)，事後条件(ensures)，ループ不変式(loop-invariant)，その他の補題(lemma)です．

ここで証明したいことは，関数sqrtの戻り値(\result)に関して事後条件が成り立つこと，つまり「sqrtの戻り値は引数 x の正の平方根（の整数近似）であること」です．しかし，この例の事前条件と事後条件だけで証明を行うのは定理証明ツールの能力を超えているので，適切なループ不変式も与える必要があります．また，この例では，加算と乗算の分配則を別途補題として与える必要があります（どのようなループ不変式や補題を記述すればよいかは，ある程度試行錯誤して見つける必要があります）．

このような記述を加えたプログラムを Why に入力すると，あとは自動的に事後条件が成り立っていることを証明してくれます（下図）．図の右上部の領域に表示されているのが，その下の領域にオレンジ色で示されている式（事後条件の一部）に対して定理証明ツールが作成した「証明」です．

↑

モデル検査再訪†

モデル検査(model-checking)とは，検査対象であるシステムを有限オートマトン（またはその拡張）に近似し，可能な実行経路を網羅的に調べることで，「望ましくない状態（デッドロックなど）に陥らないか」や「目的の状態に到達することが可能か」等を調べる方法です（近似で得られた有限オートマトンを検査対象のモデルと言います）．

定理証明型検証に比べて検証できる性質が限定されますが，定理証明型検証では人間がループ不変式や補題をよく考えて記述しなければいけないのに対し，モデル検査では最終的に満たしてほしい性質のみ記述するだけで検証が行えます．並行システムや通信プロトコルなど，モジュール間の動作タイミングが重要なシステムの検証には特に向いています．

有限オートマトンへのモデル化や，検証したい性質の記述には，ある程度の知識が必要です．通常，検査対象ソフトウェアの動作を完全に表現した有限オートマトンでは，状態数が莫大になり，現実的な時間では検証ができません．手に負える大きさに近似しないといけませんが，本来の検査対象との差が大きくなり過ぎると検証が無意味になってしまうという問題があります．

↑

補足資料†

2012年度応用ソフトウェア工学論
- モデル検査に関する過去の授業の資料。

↑

例†

下図は，モデル検査支援環境 Uppaal を使って，非常に簡単なエレベータシステムの検証を行おうとしている例です．このシステムは，1～3階を移動するカゴと，各階の呼び出しボタンから構成され，それぞれの動作が有限オートマトンで記述されています（通常の意味の有限オートマトンよりは拡張されていて，floorやarriveといった変数が取り付けられ，変数の値によって状態遷移が可能かどうか変わります）．

下図では，このエレベータシステムに対し，「1階の呼出ボタンが押されたら，いつかは1階に着く」等の性質が成り立つかどうか検証しています．検証したい性質は時相論理(temporal logic)式という独特の記法で記述します．この例では「1階の呼出ボタンが押されたら，いつかは1階に着く」という性質は成り立たず，赤色の印でそのことが示されています．

性質が成り立たない場合，それがどのような動作順序をたどったときに起こるか（この動作順序を反例と言います）を別の画面で確認できるので，それを見てシステムを修正することになります．

（ちなみに上記のシステムモデルではなぜこの性質を満たさないかというと，上記のモデルでは「カゴが2階にあるときに1階からも3階からも呼び出されている場合，カゴはどちらでも好きな方に向かって移動できる」からです．従って，以下の動作順序をたどると「1階のボタンが押されているのにいつまでも1階にはカゴが着かない」ことが起こります（このような動作順序が「反例」です）．