Loading article…
ハードウェアおよびソフトウェアシステムの文脈において、形式検証とは、数学の形式的手法を用いて、特定の形式仕様または特性に関してシステムの正しさを証明または反証する行為である。[ 1 ] 形式検証は、システムの形式仕様の重要な動機であり、形式手法の中核をなすものである。これは、電子設計自動化における分析および検証の重要な側面を表し、ソフトウェア検証のアプローチの1つである。形式検証の使用により、コンピュータセキュリティ認証の共通基準の枠組みにおいて、最高レベルの評価保証レベル（EAL7 ）が可能になる。[ 2 ]
形式検証は、暗号プロトコル、組み合わせ回路、内部メモリを備えたデジタル回路、プログラミング言語でソースコードとして表現されたソフトウェアなど、システムの正当性を証明するのに役立ちます。検証済みのソフトウェアシステムの代表的な例としては、 CompCert検証済みCコンパイラやseL4高信頼性オペレーティングシステムカーネルなどが挙げられます。
これらのシステムの検証は、システムの数学モデルの形式的証明の存在を保証することによって行われます。 [ 3 ]システムをモデル化するために使用される数学的オブジェクトの例としては、有限状態機械、ラベル付き遷移システム、ホーン節、ペトリネット、ベクトル加算システム、時間付きオートマトン、ハイブリッドオートマトン、プロセス代数、操作的意味論、表示的意味論、公理的意味論、ホーア論理などのプログラミング言語の形式的意味論などがあります。[ 4 ]
モデル検査は、数学モデルを体系的かつ徹底的に調査するものです。このような調査は有限モデルで可能ですが、無限の状態集合を抽象化や対称性を利用して有限に効果的に表現できる一部の無限モデルでも可能です。通常、これはモデル内のすべての状態と遷移を調査することから成り、スマートでドメイン固有の抽象化技術を使用して、単一の操作で状態のグループ全体を考慮し、計算時間を短縮します。実装技術には、状態空間列挙、記号状態空間列挙、抽象解釈、記号シミュレーション、抽象化の洗練などがあります。検証される特性は、線形時相論理(LTL)、プロパティ仕様言語(PSL)、SystemVerilogアサーション (SVA)、計算ツリー論理(CTL)などの時相論理で記述されることがよくあります。モデル検査の大きな利点は、多くの場合完全に自動化されていることです。主な欠点は、一般的に大規模システムには拡張できないことです。記号モデルは通常、数百ビット程度の状態に限定されるのに対し、明示的な状態列挙では、探索対象となる状態空間が比較的小さい必要がある。
もう1つのアプローチは演繹的検証です。[ 5 ] [ 6 ]これは、システムとその仕様（および場合によっては他の注釈）から、システムが仕様に適合していることを意味する数学的証明義務の集合を生成し、証明支援（対話型定理証明器）（HOL、ACL2、Isabelle、Rocq（以前はCoqとして知られていた）、PVSなど）または自動定理証明器（特に充足可能性法理論（SMT）ソルバーを含む）を使用してこれらの義務を履行することから成ります。このアプローチの欠点は、ユーザーがシステムが正しく動作する理由を詳細に理解し、証明すべき定理のシーケンスの形式、またはシステムコンポーネント（関数や手続きなど）および場合によってはサブコンポーネント（ループやデータ構造など）の仕様（不変条件、事前条件、事後条件）の形式でこの情報を検証システムに伝える必要がある場合があることです。
ソフトウェアプログラムの形式検証とは、プログラムがその動作に関する形式仕様を満たしていることを証明することです。形式検証のサブ分野には、演繹的検証（上記参照）、抽象解釈、自動定理証明、型システム、軽量形式手法などがあります。有望な型ベースの検証手法の一つに、依存型プログラミングがあります。これは、関数の型に（少なくとも一部）関数の仕様が含まれ、コードの型チェックによってその仕様に対する正当性が証明されるものです。機能豊富な依存型言語は、演繹的検証を特殊なケースとしてサポートしています。
もう一つの補完的なアプローチはプログラム導出であり、これは一連の正当性を維持する手順によって機能仕様から効率的なコードを生成するものである。このアプローチの一例としてバード・メーテンス形式があり、これはプログラム合成の別の形態と見なすことができる。
これらの手法は、検証された特性が意味論から論理的に推論できる健全なものと、そのような保証がない健全でないものに分けられます。健全な手法は、可能性の空間全体を網羅した後にのみ結果を生成します。健全でない手法の例としては、可能性のサブセットのみを網羅し、例えば特定の数までの整数のみを網羅して「十分な」結果を与える手法が挙げられます。手法は、アルゴリズムの実装が必ず答えで終了することが保証されている決定可能なものと、決して終了しない可能性がある決定不可能なものに分けられます。決定可能な健全な手法が存在しない場合でも、可能性の範囲を制限することで、決定可能な不健全な手法を構築できる可能性があります。
検証は、製品の目的適合性をテストする一側面です。妥当性確認は、それを補完する側面です。多くの場合、この全体的なチェックプロセスはV&Vと呼ばれます。
検証プロセスは、静的/構造的側面と動的/動作的側面から構成されます。例えば、ソフトウェア製品の場合、ソースコードを検査（静的）し、特定のテストケースに対して実行（動的）することができます。検証は通常、動的にのみ行うことができます。つまり、製品を典型的な使用状況と非典型的な使用状況の両方でテストします（「すべての使用状況を十分に満たしているか？」）。
プログラムの修復は、生成された修正の検証に使用されるプログラムの望ましい機能を包含するオラクルに関して実行されます。簡単な例としてはテストスイートがあり、入力/出力ペアがプログラムの機能を指定します。さまざまな手法が採用されており、最もよく知られているのは充足可能性モジュロ理論(SMT) ソルバーと遺伝的プログラミング[ 7 ]の使用です。遺伝的プログラミングは進化的計算を使用して、修正の候補を生成および評価します。前者の方法は決定論的であり、後者はランダム化されています。たとえば、Nopol ツールは、バグのある条件文の修復を SMT インスタンスとしてエンコードし、if 条件と欠落した前提条件のパッチを決定論的に生成します。[ 8 ]
プログラム修復は、形式検証とプログラム合成の技術を組み合わせたものです。形式検証における欠陥位置特定技術は、合成モジュールが対象とする可能性のあるバグ箇所を特定するためにプログラム上のポイントを計算するために使用されます。修復システムは、探索範囲を縮小するために、事前に定義された少数のバグクラスに焦点を当てることがよくあります。既存の技術は計算コストが高いため、産業界での利用は限られています。
設計の複雑化に伴い、ハードウェア業界における形式検証技術の重要性が高まっている。[ 9 ] [ 10 ]現在、形式検証は主要ハードウェア企業のほとんどすべてで使用されているが、[ 11 ]ソフトウェア業界での使用は依然として停滞している。これは、エラーが商業的に大きな意味を持つハードウェア業界において、形式検証の必要性がより大きいことに起因する可能性がある。コンポーネント間の微妙な相互作用の可能性から、シミュレーションによって現実的な可能性のセットを検証することはますます困難になっている。ハードウェア設計の重要な側面は自動化された証明方法に適しており、形式検証の導入が容易になり、生産性も向上する。[ 12 ]
2011年現在これまで、いくつかのオペレーティングシステムが正式に検証されてきました。NICTA の Secure Embedded L4 マイクロカーネル( OK Labs がseL4として商用販売)、 [ 13 ]東華師範大学の OSEK/VDX ベースのリアルタイムオペレーティングシステム ORIENTAIS 、Green Hills Software のIntegrity オペレーティングシステム、SYSGOのPikeOSなどです。[ 14 ] [ 15 ] 2016 年に、イェール大学の Zhong Shao が率いるチームが、CertiKOS と呼ばれる正式に検証されたオペレーティングシステムカーネルを開発しました。[ 16 ] [ 17 ]
2017年現在、形式検証は、ネットワークの数学的モデルを通じて大規模コンピュータネットワークの設計に適用されており[ 18 ]、新しいネットワーク技術カテゴリであるインテントベースネットワーキングの一部としても適用されています[ 19 ]。形式検証ソリューションを提供するネットワークソフトウェアベンダーには、 Cisco [ 20 ]、 Forward Networks [ 21 ] [ 22 ]、Veriflow Systems [ 23 ]などがあります。
SPARKプログラミング言語は、形式検証を伴うソフトウェア開発を可能にするツールセットを提供し、いくつかの高信頼性システムで使用されています。
CompCert Cコンパイラは、ISO Cの大部分を実装した形式的に検証されたCコンパイラです。[ 24 ] [ 25 ]