形式的検証（けいしきてきけんしょう、英: formal verification）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである[要出典]。
使い方
形式的検証の適用例としては、内部にメモリを持つ暗号回路、組み合わせ回路、デジタル回路などのシステム、ソースコードで表現されるソフトウェアがある。
これらのシステムの検証は、システムを抽象化した数理モデル上で行われ、その数理モデルと実際のシステムの性質は一致している。使用される数理モデルとしては、有限状態機械、ラベル付き遷移系、ペトリネット、timed automata、hybrid automata、プロセス計算、プログラミング言語の形式意味論（操作的意味論、表示的意味論、公理的意味論）、ホーア論理などがある[要出典]。
形式的検証の手法
形式的検証の手法は大きく2つに分類される。
第一の手法はモデル検査と呼ばれる。これは数理モデルの体系的かつ徹底的な検証を意味する（有限なモデルでのみ可能だが、無限の状態を持つモデルであっても抽象化によって有限な表現が可能であれば検証可能である）。一般にモデル内の全状態と全遷移の検証を含み、演算時間を減らすために領域固有の抽象化技法などを駆使して効率化を図る。実装技法には(状態空間列挙法)、抽象状態空間列挙法、抽象解釈、(記号シミュレーション)、abstraction refinment などがある。検証される特性（プロパティ）は時相論理で記述され、線形時相論理 (LTL) や計算木論理 (CTL) が使われる。
第二の手法は論理的推論である。一般に HOL、ACL2、Isabelle、Coq といった定理証明ソフトウェアを使い、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。最近では、Perfect Developer や Escher C Verifier といったツールが証明の完全自動化を試みている。
線形論理や時相論理などの非古典論理は、モデル検査だけでなく論理的推論でも使われる。
ソフトウェアの形式的検証
ソフトウェアの形式的検証のための論理推論はさらに以下のように分類される。
- 1970年代のより古典的手法では、まずコードを普通に書き、続いてのステップで正しいことを検証する。
- (依存型プログラミング)では、関数の型がその関数の仕様（の一部）を含み、コードの型チェックによって仕様に対する正しさが保証される。完全な依存型プログラミング言語は第一の手法を特殊ケースとしてサポートする。
それとは相補的な若干異なる手法としてプログラム導出がある。その場合、正しさを保持したステップを踏んで関数仕様から効率的コードを生成する。例として Bird-Meertens Formalism (BMF) があり、"correctness by construction" の別の形態と見ることもできる。
Validation と Verification
検証(Verification)は製品が目的に適合しているかどうかをテストする観点の1つである。妥当性検証(Validation)はそれを補完する観点と言える。この両者を合わせて検証プロセス全体を V & V と呼ぶこともある。
- Validation: 「我々は正しい製品を作っているか？」すなわち、その製品はユーザーが本当に必要とすることを行っているか？
- Verification: 「我々は製品を正しく作っているか？」すなわち、その製品は仕様通りに作られているか？
検証プロセスには静的部分と動的部分がある。例えばソフトウェア製品なら、ソースコードの検査ができるし（静的）、特定のテスト条件で実行させることもできる（動的）。妥当性検証(Validation)は動的にしかできない。すなわち、製品を典型的局面で利用してみたり、一般的でない局面で利用してみたりする（すなわち、それはあらゆるユースケースに対して満足できる動作をするか、である）。
産業での応用
設計の複雑さが増すにつれ、形式的検証技法の重要性は特にハードウェア業界で増している[2][3]。コンポーネント間の潜在的な微妙な相互作用により、シミュレーションだけで考えられる組合せをすべて調べるのは難しくなってきている。ハードウェア設計の重要な面は自動化証明技法に適しており、形式的検証の導入が容易で生産的である[4]。
2011年現在、いくつかのオペレーティングシステムが形式的検証を採用している。
- Embedded L4 microkernel（NICTA）[5]
- Integrity（Green Hills Software）[5]
- PikeOS（SYSGO）[6]
脚注
- ^ Gerwin Klein; Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood et al. “seL4: Formal Verification of an OS Kernel (paper submitted to 22nd ACM Symposium on Operating Systems Principles, October 2009)”. 2011年11月7日閲覧。
- ^ Harrison, J. (2003). Formal verification at Intel. pp. 45–54. doi:10.1109/LICS.2003.1210044.
- ^ Formal verification of a real-time hardware design. Portal.acm.org (1983-06-27). Retrieved on 2011-04-30.
- ^ Formal Verification in Industry
- ^ a b "A new OS has been proven to be correct using mathematical proofs. The cost: astronomical." by Jack Ganssle
- ^ Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS