形式的検証
出典: フリー百科事典『ウィキペディア（Wikipedia）』
形式的検証とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。
目次 |
[編集] 説明
ソフトウェアテストのみでは、システムが特定の欠陥を持っていないことを証明できない。また、システムが必要な特性（プロパティ）を持っていることも証明できない。「形式的」な検証をすることで、特定の欠陥がなく必要な特性を持っていることを証明できる。システムが「全く」欠陥を持たないことを証明したり、テストしたりすることはできない。というのも、「欠陥がない」ということの形式的定義が不可能だからである。従って我々ができるのは、システムに想定される欠陥がなく、使用するに当たって必要とされる機能が全て備わっていることを証明することだけである。
[編集] 使い方
形式的検証の適用例としては、内部にメモリを持つ暗号回路、組み合わせ回路、デジタル回路などのシステム、ソースコードで表現されるソフトウェアがある。
これらのシステムの検証は、システムを抽象化した数学的モデル上で行われ、そのモデルに対応する実際のシステムは一種類とは限らない。使用される数学的モデルとしては、有限状態機械、ラベル付き遷移系、ペトリネット、timed automata、hybrid automata、プロセス代数、プログラミング言語の形式意味論（操作的意味論、表示的意味論）、ホーア論理などがある。
[編集] 形式的検証の手法
形式的検証の手法は大きく2つに分類される。
第一の手法はモデル検査と呼ばれる。これは数学的モデルの体系的かつ徹底的な検証を意味する（有限なモデルでのみ可能）。一般にモデル内の全状態と全遷移の検証を含み、演算時間を減らすために領域固有の抽象化技法などを駆使して効率化を図る。実装技法には状態空間列挙法、抽象状態空間列挙法、抽象インタプリタ、abstraction refinment などがある。
第二の手法は論理的推論である。一般に HOL theorem prover や Isabelle theorem prover などの定理証明ソフトウェアを使って、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。
検証される特性（プロパティ）は時相論理で記述され、線形時相論理や計算木論理が使われる。
[編集] Validation と Verification
検証(Verification)は製品が目的に適合しているかどうかをテストする観点の1つである。妥当性検証(Validation)はそれを補完する観点と言える。この両者を合わせて検証プロセス全体を V & V と呼ぶこともある。
- Validation: 「我々は正しい製品を作っているか？」すなわち、その製品はユーザーが本当に必要とすることを行っているか？
- Verification: 「我々は製品を正しく作っているか？」すなわち、その製品は仕様通りに作られているか？
検証プロセスには静的部分と動的部分がある。例えばソフトウェア製品なら、ソースコードの検査ができるし（静的）、特定のテスト条件で実行させることもできる（動的）。妥当性検証(Validation)は動的にしかできない。すなわち、製品を典型的局面で利用してみたり、一般的でない局面で利用してみたりする。
[編集] プログラム検証
プログラム検証とは、仕様書通りにプログラムが書かれているかを検証するプロセスである。この場合、数学的モデルに還元せずにソースコード自体に一種の形式的検証を行う。
関数型言語では、一部のプログラムは数学的帰納法によって検証可能である。命令型言語のコードはホーア論理を使って検証可能である。
[編集] 関連項目
- 形式等価判定
- プロパティ記述言語
- 静的コード解析
- 自動定理証明
