形式手法

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

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

用途

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

仕様

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

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

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

合成

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

検証

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

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

サインオフ検証

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

人間主導の証明

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

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

自動証明

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

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

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

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

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

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

テクニック

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

仕様言語

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

二分決定図

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

SATソルバー

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

アプリケーション

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

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

形式検証は、IBM、 Intel、AMDなどのほとんどの有名なハードウェアベンダーによってハードウェアで頻繁に使用されています。Intelが製品の動作を検証するために形式手法を使用しているハードウェア領域は多数あります。たとえば、キャッシュコヒーレントプロトコルのパラメーター化検証、 [ 19 ] Intel Core i7プロセッサ実行エンジンの検証[ 20 ]（定理証明、BDD、記号評価を使用）、HOL light定理証明器を使用したIntel IA-64アーキテクチャの最適化[ 21 ] 、Cadenceを使用したPCI expressプロトコルとIntel advanced management technologyをサポートする高性能デュアルポートギガビットイーサネットコントローラーの検証[ 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、「抽象解釈のためのワイドニング演算子とナローイング演算子」（Wayback Machineで2015年9月23日にアーカイブ）. コンピュータ言語、システム、構造. 第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月）、pp. 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」 .電子論文集, 理論計算機科学. 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 . 

さらに読む

アーカイブ資料
「 https://en.wikipedia.org/w/index.php?title=Formal_methods&oldid=1326266969」より取得