コンピュータサイエンスにおいて、形式手法とは、ソフトウェアおよびハードウェアシステムの仕様策定、開発、分析、検証のための数学的に厳密な手法です。 [1]ソフトウェアおよびハードウェア設計における形式手法の使用は、他の工学分野と同様に、適切な数学的分析を行うことで設計の信頼性と堅牢性が向上するという期待に基づいています。[2]

形式手法では、論理計算、形式言語、オートマトン理論、制御理論、プログラム意味論、型システム、型理論など、さまざまな理論計算機科学の基礎が採用されています。[3]

用途

形式手法は、開発プロセスのさまざまなポイントで適用できます。

仕様

形式手法は、開発対象のシステムを、必要な詳細レベルに応じて形式的に記述するために用いられます。さらに、この仕様に基づいて、プログラムを合成したり、システムの正当性を検証したりする形式手法が用いられる場合もあります。

あるいは、仕様策定段階のみが形式手法の適用対象となる場合もあります。仕様を策定することで、非公式な要件における曖昧さを発見し、解決することができます。さらに、エンジニアは形式仕様をリファレンスとして活用し、開発プロセスを導くことができます。[4]

形式仕様システムの必要性は長年指摘されてきました。ALGOL 58報告書[5] において、ジョン・バッカスはプログラミング言語の構文を記述するための形式表記法を提示しました。これは後にバッカス正規形と名付けられ、さらにバッカス・ナウア記法（BNF）と改名されました。[6]バッカスはまた、構文的に有効なALGOLプログラムの意味の形式記述が報告書への掲載に間に合わなかったと述べ、「後続の論文に含める予定」としました。しかし、形式意味論を記述した論文は発表されませんでした。[7]

合成

プログラム合成とは、仕様に準拠したプログラムを自動的に作成するプロセスです。演繹的合成アプローチはプログラムの完全な形式仕様に依存しますが、帰納的アプローチは例から仕様を推論します。合成器は、可能なプログラム空間を探索し、仕様と一致するプログラムを見つけます。この探索空間の広さから、効率的な探索アルゴリズムの開発はプログラム合成における主要な課題の一つです。[8]

検証

形式検証とは、ソフトウェア ツールを使用して形式仕様の特性を証明したり、システム実装の形式モデルがその仕様を満たしていることを証明したりすることです。

正式な仕様が開発されると、その仕様は、仕様の特性を証明するための基礎として、また推論によってシステム実装の特性 を証明するための基礎として使用されることがあります。

サインオフ検証

サインオフ検証とは、信頼性の高い形式検証ツールを用いることです。このようなツールは従来の検証方法に代わるものであり、認証を受けている場合もあります。[要出典]

人間主導の証明

システムの正しさを証明する動機は、システムの正しさを再確認したいという明白な必要性ではなく、システムをより深く理解したいという欲求である場合があります。そのため、正しさの証明の中には、数学的な証明のスタイル、つまり自然言語を用いて手書き（またはタイプセット）で作成され、そのような証明に共通する程度の非形式性も備えています。「良い」証明とは、他の人間が読みやすく理解できる証明のことです。

このようなアプローチに対する批判者は、自然言語に内在する曖昧さにより、証明における誤りが検出されない可能性があると指摘しています。多くの場合、このような証明では通常見落とされる低レベルの詳細に、微妙な誤りが存在する可能性があります。さらに、このような優れた証明を作成するには、高度な数学的洗練と専門知識が必要です。

自動証明

対照的に、自動化された手段によってそのようなシステムの正しさの証明を生成することへの関心が高まっています。自動化された技術は、一般的に以下の3つのカテゴリーに分類されます。

  • 自動定理証明では、システムの説明、一連の論理公理、および一連の推論規則が与えられると、システムが最初から正式な証明を作成しようとします。
  • モデル検査では、システムが実行中に入る可能性のあるすべての状態を徹底的に検索することで、システムが特定のプロパティを検証します。
  • 抽象解釈では、システムは、プログラムの動作特性の過剰近似を、それを表現する（おそらく完全な）格子上の不動点計算を使用して検証します。

自動定理証明器の中には、どの特性が「興味深い」のかを検証するための指示を必要とするものもあれば、人間の介入なしに動作するものもあります。モデルチェッカーは、十分に抽象的なモデルが与えられなければ、何百万もの興味のない状態の検証にすぐに行き詰まってしまう可能性があります。

このようなシステムの支持者は、面倒な詳細がすべてアルゴリズムによって検証されているため、その結果は人間が作成した証明よりも数学的な確実性が高いと主張しています。また、このようなシステムを使用するために必要な訓練は、手作業で優れた数学的証明を作成するために必要な訓練よりも少ないため、より幅広い専門家がこれらの技術を利用できるようになります。

批評家は、これらのシステムの一部は神託のようなものだと指摘しています。つまり、真実を宣言しながらも、その真実性についての説明を一切与えないのです。また、「検証者の検証」という問題もあります。検証を支援するプログラム自体が証明されていない場合、生成された結果の妥当性に疑問を抱く理由が生じる可能性があります。一部の最新のモデル検証ツールは、証明の各ステップを詳細に記述した「証明ログ」を生成し、適切なツールがあれば独立した検証を実行できるようにしています。

抽象解釈アプローチの主な特徴は、健全な分析、すなわち偽陰性がないことです。さらに、分析対象となる特性を表す抽象領域を調整し、拡張演算子[9]を適用して高速収束を実現することで、効率的にスケーラブルです。

テクニック

形式手法にはさまざまな手法が含まれます。

仕様言語

コンピューティングシステムの設計は、証明システムを含む形式言語である仕様言語を用いて表現することができます。この証明システムを用いることで、形式検証ツールは仕様を推論し、システムが仕様に準拠していることを検証することができます。[10]

二分決定図

二分決定図は、ブール関数を表すデータ構造です。[11]ブール式がプログラムの実行が仕様に準拠していることを表す場合、二分決定図を用いて、それがトートロジーであるかどうか、つまり常にTRUEと評価されるかどうかを判断できます。この場合、プログラムは常に仕様に準拠しています。[12]

SATソルバー

SATソルバーは、ブール充足可能性問題を解くことができるプログラムです。充足可能性問題は、与えられた命題式が真となるような変数の割り当てを見つける問題です。ブール式がプログラムの特定の実行が仕様に準拠していることを表している場合、それが充足不可能であると判断することは、すべての実行が仕様に準拠していると判断することと同等です。SA​​Tソルバーは、境界付きモデル検査でよく使用されますが、非境界付きモデル検査でも使用できます。[13]

アプリケーション

形式手法は、ルータ、イーサネットスイッチ、ルーティングプロトコル、セキュリティアプリケーション、seL4などのオペレーティングシステムの マイクロカーネルなど、ハードウェアとソフトウェアのさまざまな領域に適用されています。データセンターで使用されるハードウェアとソフトウェアの機能検証に使用された例がいくつかあります。IBMは、 AMD x86プロセッサの開発プロセスで定理証明器であるACL2を使用しました。 [引用が必要] Intelは、ハードウェアとファームウェア（読み取り専用メモリにプログラムされた永続的なソフトウェア）の検証にこのような方法を使用しています[引用が必要]。Dansk Datamatik Centerは、 1980年代に形式手法を使用して、後に長寿商用製品となるAdaプログラミング言語のコンパイラシステムを開発しました。 [14] [15]

NASAのプロジェクトには、次世代航空輸送システム[要出典]、国家空域システムへの無人航空機システムの統合[16]、空中協調紛争解決・検知(ACCoRD) [17 ]など、形式手法が適用されているものがいくつかあります。Atelier BによるB法[ 18]は、アルストムとシーメンスが世界中に設置したさまざまな地下鉄の安全自動化の開発に使用されているほか、 ATMELとSTマイクロエレクトロニクスによるCommon Criteria認証とシステムモデルの開発にも使用されています。

形式検証は、IBM、 Intel 、AMDなどのほとんどの有名なハードウェアベンダーによってハードウェアで頻繁に使用されています。Intelが形式手法を使用して製品の動作を検証したハードウェア領域は多数あります。たとえば、キャッシュ コヒーレント プロトコルのパラメーター化検証、[19] Intel Core i7 プロセッサー実行エンジンの検証[20] (定理証明、BDD、記号評価を使用)、HOL light 定理証明器を使用した Intel IA-64 アーキテクチャの最適化[21] 、Cadence を使用した、 PCI expressプロトコルと Intel 高度管理技術をサポートする高性能デュアルポートギガビット イーサネット コントローラーの検証[22]などです。同様に、IBMは、パワー ゲートの検証、 [23]レジスタの検証、[24]および IBM Power7 マイクロプロセッサーの機能検証に形式手法を使用しています。[25]

ソフトウェア開発において

ソフトウェア開発において、形式手法とは、要件、仕様、設計の各レベルでソフトウェア（およびハードウェア）の問題を解決するための数学的なアプローチです。形式手法は、航空電子機器ソフトウェアなど、安全性やセキュリティが極めて重要なソフトウェアやシステムに最も多く適用されます。DO -178Cなどのソフトウェア安全性保証規格では、補足的な形式手法の使用が認められており、コモンクライテリアでは、分類の最高レベルで形式手法の使用が義務付けられています。

順次ソフトウェアの場合、形式手法の例には、 B メソッド、自動定理証明で使用される仕様言語、RAISE、Z 表記法などがあります。

関数型プログラミングでは、プロパティベースのテストにより、個々の関数の予想される動作の数学的仕様とテスト（徹底的なテストではないにしても）が可能になりました。

オブジェクト制約言語(およびJava モデリング言語などの特殊化) により、必ずしも正式に検証されなくても、オブジェクト指向システムを正式に指定できるようになりました。

並行ソフトウェアおよびシステムの場合、ペトリ ネット、プロセス代数、有限状態マシン(オートマトン理論に基づく。仮想有限状態マシンまたはイベント駆動型有限状態マシンも参照) を使用すると、実行可能なソフトウェア仕様が可能になり、アプリケーションの動作を構築および検証するために使用できます。

ソフトウェア開発における形式手法へのもう一つのアプローチは、何らかの形式のロジック（通常は一階述語論理のバリエーション）で仕様を記述し、そのロジックをプログラムであるかのように直接実行するというものである。記述論理に基づくOWL言語はその一例である。また、英語（または他の自然言語）の何らかのバージョンとロジックを自動的にマッピングしたり、ロジックを直接実行したりする研究もある。その例としては、語彙や構文の制御を目的としないAttempto Controlled EnglishやInternet Business Logicなどがある。双方向の英語とロジックのマッピングとロジックの直接実行をサポートするシステムの特徴は、ビジネスレベルまたは科学レベルで結果を英語で説明できることである。[要出典]

半形式手法

準形式的手法とは、完全に「形式的」とはみなされない形式主義と言語である。意味論の完成は後段階に委ねられ、人間による解釈、あるいはコードジェネレータやテストケースジェネレータなどのソフトウェアによる解釈によって行われる。[26]

一部の実務家は、形式手法コミュニティが仕様や設計の完全な形式化を過度に重視していると考えている。[27] [28]彼らは、関連する言語の表現力とモデル化対象となるシステムの複雑さが、完全な形式化を困難で費用のかかる作業にしていると主張する。代替案として、部分的な仕様記述と集中的な適用を重視する様々な軽量形式手法が提案されている。こうした軽量形式手法の例として、Alloyオブジェクトモデリング記法[29] 、DenneyによるZ記法のいくつかの側面とユースケース駆動開発の統合[30]、CSK VDMツール[31]などが挙げられる。

形式手法と記法

さまざまな形式手法と表​​記法が利用可能です。

仕様言語

モデルチェッカー

解答者と競技

形式手法における多くの問題はNP困難ですが、実際に発生する事例では解決可能です。例えば、ブール充足可能性問題はクック・レビン定理によりNP完全ですが、SATソルバーは様々な大規模事例を解くことができます。形式手法で発生する様々な問題には「ソルバー」が存在し、そのような問題解決における最先端技術を評価するための定期的なコンペティションが数多く開催されています。[33]

組織

参照

参考文献

  1. ^ Butler, RW (2001-08-06). 「形式手法とは何か？」 . 2006年11月16日閲覧。
  2. ^ Holloway, C. Michael. 「エンジニアが形式手法を検討すべき理由」(PDF) . 第16回デジタル航空電子工学システム会議 (1997年10月27～30日). 2006年11月16日時点のオリジナル(PDF)からアーカイブ。 2006年11月16日閲覧。 {{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）が必要です
  3. ^ モナン、3-4ページ
  4. ^ Utting, Mark; Reeves, Steve (2001年8月31日). 「テストによる形式手法の軽量版の指導」 .ソフトウェアテスト、検証、信頼性. 11 (3): 181– 195. doi :10.1002/stvr.223.
  5. ^ Backus, JW (1959). 「チューリッヒACM-GAMM会議で提案された国際代数言語の構文と意味論」国際情報処理会議議事録. UNESCO.
  6. ^ Knuth, Donald E. (1964), バッカス正規形とバッカスナウア形. Communications of the ACM , 7(12):735–736.
  7. ^ O'Hearn, Peter W.; Tennent, Robert D. (1997). Algol-like Languages .
  8. ^ Gulwani, Sumit; Polozov, Oleksandr; Singh, Rishabh (2017). 「プログラム合成」 .プログラミング言語の基礎と動向. 4 ( 1–2 ): 1– 119. doi :10.1561/2500000010.
  9. ^ A. CortesiとM. Zanioli、「抽象解釈のための拡張演算子と縮小演算子」、コンピュータ言語、システム、構造、第37巻（1）、pp.24–42、Elsevier、ISSN  1477-8424（2011年）。
  10. ^ Bjørner, Dines; Henson, Martin C. (2008).仕様記述言語のロジック. pp.  VII– XI.
  11. ^ Bryant, Randal E. (2018). 「二分決定図」. Clarke, Edmund M.、Henzinger, Thomas A.、Veith, Helmut、Bloem, Roderick (編). 『モデル検査ハンドブック』p. 191.
  12. ^ Chaki, Sagar; Gurfinkel, Arie (2018). 「BDDベースのシンボリックモデル検査」. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (編). 『モデル検査ハンドブック』 p. 191.
  13. ^ Prasad, Mukul R; Biere, Armin; Gupta, Aarti (2005年1月25日). 「SATベースの形式検証における最近の進歩の概観」.国際技術移転ソフトウェアツールジャーナル. 7 (2): 156– 173. doi :10.1007/s10009-004-0183-4.
  14. ^ ビョルナー、ダインズ;グラム、クリスチャン。オエスト、オーレ・N.リストローム、レイフ (2011)。 「ダンスク・データマティック・センター」。インパリアッツォでは、ジョン。ルンディン、パー;ベングラー、ベンクト編（編）。北欧コンピューティングの歴史 3: 情報通信技術における IFIP の進歩。スプリンガー。350～ 359ページ 。
  15. ^ Bjørner, Dines; Havelund, Klaus. 「形式手法の40年：いくつかの障害といくつかの可能性？」 FM 2014: 形式手法：第19回国際シンポジウム、シンガポール、2014年5月12日～16日。議事録(PDF)。Springer。pp.  42– 61。
  16. ^ Gheorghe, AV, & Ancel, E. (2008年11月). 無人航空システムの国家空域システムへの統合. インフラシステムとサービス：より明るい未来のためのネットワーク構築 (INFRA)、2008年第1回国際会議 (pp. 1-5). IEEE.
  17. ^ 空中協調紛争解決および検知、http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ 2016年3月5日アーカイブ、Wayback Machine
  18. ^ 「アトリエB」. www.atelierb.eu .
  19. ^ CT Chou、PK Mannava、S. Park、「キャッシュコヒーレンスプロトコルのパラメータ化検証のための簡単な方法」、コンピュータ支援設計における形式手法、pp. 382–398、2004年。
  20. ^ Intel Core i7 プロセッサー実行エンジン検証における形式検証、http://cps-vo.org/node/1371、Wayback Machineに 2015 年 5 月 3 日にアーカイブ、2013 年 9 月 13 日にアクセス。
  21. ^ J. Grundy、「Intel IA-64 アーキテクチャの検証済み最適化」、Theorem Proving in Higher Order Logics、Springer Berlin Heidelberg、2004 年、215 ～ 232 ページ。
  22. ^ E. Seligman、I. Yarom、「Cadence Conformal LEC を使用するための最もよく知られた方法」、Intel。
  23. ^ C. Eisner、A. Nahir、K. Yorav、「構成的推論による電力ゲート設計の機能検証[リンク切れ]」、Computer Aided Verification、Springer Berlin Heidelberg、pp. 433–445。
  24. ^ PC Attie、H. Chockler、「フォールトトレラントレジスタエミュレーションの自動検証」、電子理論計算機科学ノート、第149巻、第1号、49～60頁。
  25. ^ KD Schubert、W. Roesner、JM Ludden、J. Jackson、J. Buchert、V. Paruthi、B. Brock、「IBM POWER7 マイクロプロセッサおよび POWER7 マルチプロセッサ システムの機能検証」、IBM Journal of Research and Development、vol. 55、no 3。
  26. ^ X2R-2、成果物D5.1。
  27. ^ ダニエル・ジャクソンとジャネット・ウィング、「軽量形式手法」、IEEE Computer、1996年4月
  28. ^ Vinu GeorgeとRayford Vaughn、「要件エンジニアリングにおける軽量形式手法の適用」、Wayback Machineで2006年3月1日にアーカイブ、Crosstalk: The Journal of Defense Software Engineering、2003年1月
  29. ^ ダニエル・ジャクソン、「Alloy: 軽量オブジェクトモデリング表記法」、ACM Transactions on Software Engineering and Methodology (TOSEM)、第11巻、第2号（2002年4月）、256-290頁
  30. ^ リチャード・デニー著『ユースケースで成功する：スマートな働き方で品質を実現』Addison-Wesley Professional Publishing、2005年、ISBN 0-321-31643-6。
  31. ^ Sten AgerholmとPeter G. Larsen、「形式手法への軽量アプローチ」、Wayback Machineで2006年3月9日にアーカイブ、応用形式手法の最新動向に関する国際ワークショップの議事録、ドイツ、ボッパルト、Springer-Verlag、1998年10月
  32. ^ "ESBMC". esbmc.org .
  33. ^ Bartocci, Ezio; Beyer, Dirk; Black, Paul E.; Fedyukovich, Grigory; Garavel, Hubert; Hartmanns, Arnd; Huisman, Marieke; Kordon, Fabrice; Nagele, Julian; Sighireanu, Mihaela; Steffen, Bernhard; Suda, Martin; Sutcliffe, Geoff; Weber, Tjark; Yamada, Akihisa (2019). "TOOLympics 2019: An Overview of Competitions in Formal Methods". In Beyer, Dirk; Huisman, Marieke; Kordon, Fabrice; Steffen, Bernhard (eds.). Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp.  3–24 .土井: 10.1007/978-3-030-17502-3_1。ISBN 978-3-030-17502-3。
  34. ^ フロレイクス、ニルス;ヘーレ、マリジン。イゼル、マルクス。ヤルビサロ、マッティ。須田、マーティン（2021-12-01）。 「SATコンペティション2020」。人工知能。301 103572.土井: 10.1016/j.artint.2021.103572。ISSN  0004-3702。
  35. ^ Cornejo, César (2021-01-27). 「Alloy 向け SAT ベース算術サポート」. Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering . ASE '20. ニューヨーク、ニューヨーク州、米国: Association for Computing Machinery. pp.  1161– 1163. doi :10.1145/3324884.3415285. ISBN 978-1-4503-6768-4。
  36. ^ Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron (2013-03-01). 「SMT-COMPの6年間」 . Journal of Automated Reasoning . 50 (3): 243– 277. doi :10.1007/s10817-012-9246-5. ISSN  1573-0670.
  37. ^ Fedyukovich, Grigory; Rümmer, Philipp (2021-09-13). 「コンペティションレポート: CHC-COMP-21」. Electronic Proceedings in Theoretical Computer Science . 344 : 91–108 . arXiv : 2008.02939 . doi : 10.4204/EPTCS.344.7 . ISSN  2075-2180.
  38. ^ Shukla, Ankit; Biere, Armin; Pulina, Luca; Seidl, Martina (2019年11月). 「定量化ブール式の応用に関する調査」. 2019 IEEE 第31回人工知能ツール国際会議 (ICTAI) . IEEE. pp.  78– 84. doi :10.1109/ICTAI.2019.00020. ISBN 978-1-7281-3798-8。
  39. ^ ピュリナ、ルカ;ザイドル、マルティナ (2019-09-01)。 「2016 年および 2017 年の QBF ソルバー評価 (QBFEVAL'16 および QBFEVAL'17)」。人工知能。274 : 224–248 .土井: 10.1016/j.artint.2019.04.002。ISSN  0004-3702。
  40. ^ Beyer, Dirk (2022). 「ソフトウェア検証の進歩：SV-COMP 2022」. Fisman, Dana; Rosu, Grigore (編).システムの構築と分析のためのツールとアルゴリズム. コンピュータサイエンス講義ノート. 第13244巻. 出版社: Springer International Publishing. pp.  375– 402. doi : 10.1007/978-3-030-99527-0_20 . ISBN 978-3-030-99527-0。
  41. ^ Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). 「SyGuS-Comp 2017: 結果と分析」. Electronic Proceedings in Theoretical Computer Science . 260 : 97–115 . arXiv : 1611.07627 . doi : 10.4204/EPTCS.260.9 . ISSN  2075-2180.

さらに読む

  • Jonathan P. BowenとMichael G. Hinchey、「形式手法」。Allen B. Tucker, Jr.編、『コンピュータサイエンスハンドブック』第2版、第XI章「ソフトウェアエンジニアリング」、第106章、106-1～106-25ページ、Chapman & Hall / CRC Press、Association for Computing Machinery、2004年。
  • Hubert Garavel (編集者) と Susanne Graf。安全でセキュアなコンピュータ システムのための形式的手法[永久デッドリンク]。Bundesamt für Sicherheit in der Informationstechnik、BSI 研究 875、ドイツ、ボン、2013 年 12 月。
  • ガラベル, ヒューバート; テル・ビーク, モーリス・H.; ヴァン・デ・ポル, ヤコ (2020年8月29日). 「2020年形式手法に関する専門家調査」. 産業用クリティカルシステムのための形式手法：第25回国際会議, FMICS 2020 (PDF) .コンピュータサイエンス講義ノート(LNCS). 第12327巻.シュプリンガー. pp.  3– 69. doi :10.1007/978-3-030-58298-2_1. ISBN 978-3-030-58297-5. S2CID  221381022。* Michael G. Hinchey、Jonathan P. Bowen、Emil Vassev著『形式手法』。Philip A. Laplante編『Encyclopedia of Software Engineering』、Taylor & Francis、2010年、308～320ページ。
  • Marieke Huisman、Dilian Gurov、Alexander Malkis、「形式手法：学術界から産業実践へ – 旅行ガイド」、arXiv:2002.07279、2020年。
  • Gleirscher, Mario; Marmsoler, Diego (2020年9月9日). 「ディペンダブルシステムエンジニアリングにおける形式手法：欧州と北米の専門家への調査」. Empirical Software Engineering . 25 (6). Springer Nature : 4473–4546 . arXiv : 1812.08815 . doi : 10.1007/s10664-020-09836-5 .
  • Jean François MoninとMichael G. Hinchey著、『Understanding formal methods』、Springer、2003年、ISBN 1-85233-247-6。
  • 形式手法ヨーロッパ（FME）
  • 形式手法ウィキ
  • Foldocの形式手法
アーカイブ資料