形式検証：ハードウェアとソフトウェアの正しさを証明する

主要な手法

実務者は、問題の種類に応じて適した、相互補完的な複数の技法を用いる。

• モデル検査：有限状態モデルを網羅的に探索し、安全性や活性などの時相的性質を検証する。
• 定理証明：多くの場合、対話型または自動化された証明支援系を用いて、プログラムや回路が形式仕様を満たすことを機械検査可能な証明として構築する。
• 抽象解釈と静的解析：プログラムを実行せずに、その性質を推論する保守的な近似手法である。
• 型システムと精密化型：構成段階から、ある種の誤り全体を防ぐプログラミング言語レベルの仕組みである。

起源と発展

形式検証は、20世紀半ばの数理論理学、プログラム意味論、オートマトン理論の進展を背景として発展した。初期の研究ではプログラムの正しさやアルゴリズムに関する推論が形式化され、その後の数十年間にはモデル検査と自動推論のための実用的なアルゴリズムやツールが登場した。計算システムが複雑化し、安全性への要求が高まるにつれて、この分野は成熟していった。

応用と例

形式手法は、信頼性が不可欠な分野で最も多く使われる。具体例には、航空電子機器、医療機器、産業用コントローラ、重要なネットワークプロトコルがある。技術者は、ロボットなどの自律システム向け制御ソフトウェアを検証し、航空機で用いられる制御・誘導サブシステムを証明する。また、暗号プロトコル、コンパイラ、オペレーティングシステムのカーネルの検証や、製造後の修正に多大な費用がかかる一部のシリコン設計にも用いられる。

限界と実務上の考慮事項

形式検証は強力だが、あらゆる場面に適用できるわけではない。正しい形式仕様を作成すること自体が難しい場合があり、多くの性質は一般には決定不能である。また、網羅的な手法は、複雑性の増大に伴う状態空間爆発に直面する。そのためチームは、コスト、労力、網羅性を管理するため、形式的証明をテスト、コードレビュー、実行時監視と組み合わせることが多い。

関連概念との違いと注目すべき事項

形式検証は妥当性確認やテストとは異なる。検証が問うのは「実装は形式仕様を満たしているか」であるのに対し、妥当性確認が問うのは「仕様は現実世界で意図された目的に合致しているか」である。ツールには、完全自動の検査器から対話型証明支援系まである。導入を成功させるには通常、厳密なツールと、仕様およびモデルを注意深く設計するエンジニアリングとを組み合わせる。入門資料やツールの参照先については、ソフトウェアおよび数学的手法のガイドにある一般的な資料とツール文書を参照のこと。