Loading article…
コンピュータサイエンスにおいて、形式手法は、ソフトウェアおよびハードウェアシステムの仕様、開発、分析、検証のための数学的に厳密な技術である。 [ 1 ]ソフトウェアおよびハードウェア設計に形式手法を用いる動機は、他の工学分野と同様に、適切な数学的分析を行うことで設計の信頼性と堅牢性に貢献できるという期待に基づいている。[ 2 ]
形式手法は、論理計算、形式言語、オートマトン理論、制御理論、プログラム意味論、型システム、型理論など、さまざまな理論計算機科学の基礎を採用しています。[ 3 ]
形式手法は、開発プロセスのさまざまな段階で適用できる。
形式手法を用いることで、開発対象システムの形式的な記述を、必要な詳細レベルで作成することができる。さらに、この仕様に基づいてプログラムを合成したり、システムの正当性を検証したりするために、他の形式手法を用いることも可能である。
あるいは、仕様策定段階のみが形式手法を用いる場合もある。仕様書を作成することで、非公式な要件の曖昧さを発見し、解決することができる。さらに、エンジニアは形式仕様書をリファレンスとして開発プロセスを導くことができる。[ 4 ]
形式仕様システムの必要性は何年も前から指摘されてきた。ALGOL 58レポートでは、[ 5 ]ジョン・バッカスがプログラミング言語の構文を記述するための形式表記法を発表し、後にバッカス正規形、さらにバッカス・ナウア記法(BNF) と改名された。[ 6 ]バッカスはまた、構文的に有効な ALGOL プログラムの意味の形式的な記述はレポートに含めるのに間に合わなかったと述べ、「後続の論文に含める」と記した。しかし、形式意味論を記述した論文は結局発表されなかった。[ 7 ]
プログラム合成とは、仕様に準拠したプログラムを自動的に作成するプロセスです。演繹的合成手法はプログラムの完全な形式仕様に依存しますが、帰納的手法は例から仕様を推論します。シンセサイザは、可能なプログラムの空間を探索して、仕様に合致するプログラムを見つけます。この探索空間の大きさから、効率的な探索アルゴリズムの開発は、プログラム合成における主要な課題の1つです。[ 8 ]
形式検証とは、ソフトウェアツールを使用して形式仕様の特性を証明したり、システム実装の形式モデルがその仕様を満たしていることを証明したりすることである。
正式な仕様が策定されると、その仕様は仕様自体の特性を証明するための基礎として使用され、ひいてはシステム実装の特性を推論するためにも使用される。
サインオフ検証とは、信頼性の高い正式な検証ツールを使用することです。このようなツールは、従来の検証方法に取って代わることができます（ツール自体が認証されている場合もあります）。[ 9 ]
システムの正しさを証明する動機は、必ずしもシステムの正しさを確証したいという明白な必要性からではなく、システムをより深く理解したいという欲求から生じる場合がある。そのため、正しさの証明の中には、数学的証明のスタイルで作成されるものもある。つまり、自然言語を用いて手書き（または活字印刷）で記述され、こうした証明に共通する非公式な表現が用いられる。「良い」証明とは、他の人間が読みやすく理解しやすいものである。
こうした手法に対する批判者は、自然言語に内在する曖昧さによって、証明における誤りが見過ごされがちであると指摘する。多くの場合、こうした証明では見落とされがちな低レベルの詳細部分に、微妙な誤りが存在する可能性がある。さらに、このような優れた証明を作成するには、高度な数学的知識と専門性が必要となる。
対照的に、こうしたシステムの正当性を証明するための自動化された手段への関心が高まっている。自動化された技術は、大きく3つのカテゴリーに分類される。
自動定理証明器の中には、どの性質が「興味深い」かを判断するための指示を必要とするものもあれば、人間の介入なしに動作するものもある。モデルチェッカーは、十分に抽象的なモデルが与えられないと、何百万もの興味のない状態をチェックすることにすぐに行き詰まってしまう可能性がある。
こうしたシステムの支持者たちは、煩雑な詳細事項がすべてアルゴリズムによって検証されているため、人間が作成した証明よりも数学的な確実性が高いと主張する。また、こうしたシステムを使用するために必要な訓練は、手作業で質の高い数学的証明を作成するために必要な訓練よりも少なく、より幅広い分野の実務家がこれらの技術を利用できるという利点もある。
批評家たちは、そうしたシステムの中には、まるで神託のようなものがあると指摘している。つまり、真実を宣言するものの、その真実の根拠を一切説明しないのだ。また、「検証者の検証」という問題もある。検証を支援するプログラム自体が未検証であれば、生成された結果の妥当性に疑問が生じる可能性がある。現代のモデル検査ツールの中には、証明の各ステップを詳細に記した「証明ログ」を生成するものもあり、適切なツールがあれば、独立した検証が可能となる。
抽象解釈アプローチの主な特徴は、健全な分析を提供すること、つまり偽陰性が返されないことです。さらに、分析対象の特性を表す抽象ドメインを調整し、高速な収束を実現するために拡大演算子[ 10 ]を適用することにより、効率的にスケーラブルです。
形式手法には、さまざまな技術が含まれる。
コンピュータシステムの設計は、証明システムを含む形式言語である仕様言語を使用して表現できます。この証明システムを使用すると、形式検証ツールは仕様について推論し、システムが仕様に準拠していることを確立できます。[ 11 ]
二分決定図は、ブール関数を表すデータ構造です。[ 12 ]ブール式がプログラムの実行が仕様に準拠しているかどうかを表す場合、バイナリ決定図を使用して、これはトートロジーです。つまり、常にTRUEと評価されます。この場合、プログラムは常に仕様に準拠します。[ 13 ]
SATソルバーは、ブール充足可能性問題、つまり与えられた命題式が真となるような変数の割り当てを見つける問題を解くことができるプログラムです。ブール式がプログラムの特定の実行が仕様に準拠していることを表し、次に充足不可能であることは、すべての実行が仕様に準拠していることを判定することと同等です。SATソルバーは、境界付きモデル検査でよく使用されますが、境界なしモデル検査でも使用できます。[ 14 ]
形式手法は、ルーター、イーサネットスイッチ、ルーティングプロトコル、セキュリティアプリケーション、seL4などのオペレーティングシステムマイクロカーネルなど、ハードウェアとソフトウェアのさまざまな分野で適用されています。データセンターで使用されるハードウェアとソフトウェアの機能を検証するために使用された例がいくつかあります。IBMは、 AMD x86 プロセッサの開発プロセスで定理証明器であるACL2 を使用しました。Intel は、ハードウェアとファームウェア(読み取り専用メモリにプログラムされた永続的なソフトウェア)を検証するためにこのような手法を使用しています。Dansk Datamatik Center は、 1980 年代に形式手法を使用して、 Ada プログラミング言語用のコンパイラ システムを開発し、それが長期間商用製品となりました。[ 15 ] [ 16 ]
NASAには、次世代航空輸送システム、国家空域システムにおける無人航空機システムの統合[ 17 ]、空中協調衝突解決および検出（ACCoRD）[ 18 ]など、形式手法を適用した他のプロジェクトがいくつかあります。Atelier Bを使用したBメソッド[ 19 ]は、AlstomとSiemensが世界中に設置したさまざまな地下鉄の安全自動化の開発、およびATMELとSTMicroelectronicsによる共通基準認証とシステムモデルの開発にも使用されています。
形式検証は、IBM、 Intel 、AMDなどの有名なハードウェアベンダーのほとんどによってハードウェアで頻繁に使用されています。Intel は、キャッシュコヒーレント プロトコルのパラメータ検証[ 20 ] 、 Intel Core i7 プロセッサ実行エンジンの検証 [ 21 ] (定理証明、BDD、および記号評価を使用)、HOL ライト定理証明器を使用した Intel IA-64 アーキテクチャの最適化[ 22 ]、Cadence を使用したPCI Expressプロトコルと Intel アドバンス マネジメント テクノロジーをサポートする高性能デュアルポートギガビット イーサネットコントローラの検証[ 23 ]など、ハードウェアの多くの分野で形式手法を使用して製品の動作を検証しています。同様に、IBM は、パワー ゲート[ 24 ]、レジスタ[ 25 ] 、および IBM Power7 マイクロプロセッサの機能検証[ 26 ]の検証に形式手法を使用しています。
ソフトウェア開発において、形式手法とは、要件、仕様、設計の各レベルでソフトウェア（およびハードウェア）の問題を解決するための数学的手法です。形式手法は、航空電子機器ソフトウェアなど、安全性やセキュリティが極めて重要なソフトウェアやシステムに適用されることが多いです。DO -178Cなどのソフトウェア安全性保証規格では、形式手法を補足的に使用することが認められており、Common Criteriaでは、最高レベルの分類において形式手法の使用が義務付けられています。
逐次ソフトウェアの場合、形式手法の例としては、 Bメソッド、自動定理証明で使用される仕様言語、RAISE、Z記法などが挙げられる。
関数型プログラミングにおいては、プロパティベーステストによって、個々の関数の期待される動作を数学的に規定し、（網羅的なテストではないにしても）テストすることが可能になった。
オブジェクト制約言語（およびJavaモデリング言語などの特殊化）により、オブジェクト指向システムは、必ずしも形式的に検証されるわけではないものの、形式的に仕様化することが可能になった。
並行ソフトウェアおよびシステムの場合、ペトリネット、プロセス代数、および有限状態機械（オートマトン理論に基づく。仮想有限状態機械またはイベント駆動型有限状態機械も参照）は、実行可能なソフトウェア仕様を可能にし、アプリケーションの動作を構築および検証するために使用できます。
ソフトウェア開発における形式手法のもう一つのアプローチは、仕様を何らかの論理形式（通常は一階述語論理の変形）で記述し、それをプログラムであるかのように直接実行することです。記述論理に基づくOWL言語はその一例です。また、英語（または他の自然言語）の何らかのバージョンを論理形式に自動的にマッピングし、論理形式を直接実行する研究も行われています。例としては、語彙や構文を制御しようとしないAttempto Controlled EnglishやInternet Business Logicなどがあります。双方向の英語-論理マッピングと論理形式の直接実行をサポートするシステムの特徴は、ビジネスレベルまたは科学レベルで、結果を英語で説明できることです。
半形式的手法は、完全に「形式的」とはみなされない形式体系や言語です。意味論を完成させる作業を後の段階に延期し、その作業は人間の解釈、またはコードジェネレータやテストケースジェネレータなどのソフトウェアによる解釈によって行われます。[ 27 ]
形式手法コミュニティは仕様や設計の完全な形式化を過度に重視してきたと考える実務家もいる。[ 28 ] [ 29 ]彼らは、関係する言語の表現力とモデル化されるシステムの複雑さから、完全な形式化は困難でコストのかかる作業になると主張している。代替案として、部分的な仕様と集中的な適用を重視するさまざまな軽量形式手法が提案されている。形式手法に対するこの軽量アプローチの例としては、Alloyオブジェクトモデリング表記法[ 30 ] 、Denney によるZ 表記法のいくつかの側面とユースケース駆動開発の統合[ 31 ] 、および CSK VDMツール[ 32 ]などがある。
様々な形式手法と表記法が利用可能である。
形式手法における多くの問題はNP困難ですが、実際に発生するケースでは解決可能です。たとえば、ブール充足可能性問題はクック・レヴィンの定理によりNP完全ですが、SATソルバーはさまざまな大規模なインスタンスを解くことができます。形式手法で発生するさまざまな問題に対する「ソルバー」があり、そのような問題を解決する最先端技術を評価するための定期的なコンペティションが多数開催されています。[ 35 ]
{{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）