形式手法

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

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

用途

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

仕様

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

あるいは、仕様は形式手法が使用される唯一の段階である可能性があります。仕様を記述することで、非公式な要件の曖昧さを発見して解決することができます。さらに、エンジニアは正式な仕様を参照として使用して、開発プロセスをガイドすることができます。^[4]

正式な仕様体系の必要性は長年指摘されてきた。ALGOL 58レポート^[5] で、ジョン・バッカスはプログラミング言語の構文を記述するための正式な表記法を提示した。これは後にバッカス正規形と名付けられ、さらにバッカス・ナウア記法(BNF)と改名された。 ^[6]バッカスは、構文的に有効な ALGOL プログラムの意味の正式な記述がレポートに間に合わず、「後続の論文に含められる」と述べた。しかし、正式な意味を記述した論文は発表されなかった。^[7]

合成

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

検証

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

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

サインオフ検証

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

人間主導の証明

システムの正しさを証明する動機は、システムの正しさを再確認したいという明らかな必要性ではなく、システムをよりよく理解したいという願望である場合があります。その結果、正しさの証明の一部は、数学的な証明のスタイル、つまり自然言語を使用して手書き（またはタイプセット）で作成され、そのような証明に共通するレベルの非公式性が使用されます。「良い」証明とは、他の人間の読者が読み、理解できる証明です。

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

自動証明

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

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

自動定理証明器の中には、どの特性が追求する価値があるかに関するガイダンスを必要とするものもあれば、人間の介入なしで動作するものもあります。十分に抽象的なモデルが与えられないと、モデルチェッカーはすぐに何百万もの興味のない状態をチェックすることに行き詰まる可能性があります。

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

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

抽象解釈アプローチの主な特徴は、健全な分析を提供すること、つまり偽陰性が返されないことです。さらに、分析対象の特性を表す抽象ドメインを調整し、拡大演算子^[9]を適用して高速収束を実現することで、効率的にスケーラブルです。

テクニック

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

仕様言語

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

二分決定図

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

SAT ソルバー

SATソルバーは、ブール充足可能性問題、つまり与えられた命題式が真と評価される変数の割り当てを見つける問題を解くことができるプログラムです。ブール式がプログラムの特定の実行が仕様に準拠していることを表している場合、それが充足不可能であると判断することは、すべての実行が仕様に準拠していると判断することと同じです。SATソルバーは、境界付きモデル検査でよく使用されますが、境界なしモデル検査でも使用できます。^[13] ${\mathcal {P}}$ $\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とSTマイクロエレクトロニクスによる Common Criteria認証やシステムモデルの開発にも使用されている。

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

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

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

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

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

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

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

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

半形式的手法

セミフォーマルメソッドは、完全に「形式的」とは見なされない形式主義と言語です。セマンティクスを完成させる作業を後の段階に延期し、その後、人間による解釈、またはコードやテストケースジェネレーターなどのソフトウェアによる解釈によって行われます。^[26]

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

形式手法と記法

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

仕様言語

モデルチェッカー

ESBMC ^[32]
MALPAS ソフトウェア静的解析ツールセット– 安全性が重要なシステムの正式な証明に使用される産業用モデルチェッカー
PAT – 並行システムと CSP 拡張 (共有変数、配列、公平性など) 用の無料のモデルチェッカー、シミュレーター、リファインメントチェッカー
スピン
ウパール

解答者と競技

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

SATコンペティションは、SATソルバーを比較する毎年開催されるコンペティションです。^{[34] SATソルバーは、}Alloyなどの形式手法ツールで使用されています。^[35]
CASC は、自動定理証明器の年次コンテストです。
SMT-COMPは形式検証に適用されるSMTソルバーの年次コンテストである。^[36]
CHC-COMPは、形式検証に応用できる制約付きホーン節を解く人の年次コンテストである。 ^[37]
QBFEVALは、モデル検査に応用できる真量化ブール式を解くソルバーの2年ごとのコンテストです。^[38]^[39]
SV-COMPはソフトウェア検証ツールの年次コンテストです。^[40]
SyGuS-COMPはプログラム合成ツールの年次コンテストである。^[41]

組織

参照

参考文献

^ Butler, RW (2001-08-06). 「形式手法とは何か?」 . 2006-11-16閲覧。
^ Holloway, C. Michael. 「エンジニアが形式手法を検討すべき理由」(PDF) 。第 16 回デジタルアビオニクスシステムカンファレンス (1997 年 10 月 27 ～ 30 日)。2006 年 11 月 16 日時点のオリジナル(PDF)からアーカイブ。2006年11 月 16 日閲覧。 {{cite journal}}:ジャーナルを引用するには|journal=(ヘルプ)が必要です
^ モナン、pp.3-4
^ Utting, Mark ; Reeves, Steve (2001 年 8 月 31 日)。「テストによる形式手法の軽量版の指導」。ソフトウェアのテスト、検証、信頼性。11 (3): 181–195。doi :10.1002/stvr.223。
^ Backus, JW (1959)。「チューリッヒ ACM-GAMM 会議で提案された国際代数言語の構文と意味論」。国際情報処理会議の議事録。ユネスコ。
^ Knuth, Donald E. (1964)、Backus Normal Form と Backus Naur Form。Communications of the ACM、7(12):735–736。
^ O'Hearn, Peter W.; Tennent, Robert D. (1997). Algol のような言語。
^ Gulwani, Sumit; Polozov, Oleksandr; Singh, Rishabh ( 2017). 「プログラム合成」。プログラミング言語の基礎と動向。4 (1–2): 1–119. doi :10.1561/2500000010.
^ A. CortesiとM. Zanioli、「抽象解釈のための拡張演算子と縮小演算子」。コンピュータ言語、システム、構造。第37巻（1）、pp.24-42、Elsevier、ISSN 1477-8424（2011）。
^ Bjørner, Dines; Henson, Martin C. (2008).仕様言語のロジック. pp. VII–XI.
^ Bryant, Randal E. (2018). 「二分決定図」。Clarke, Edmund M.、Henzinger, Thomas A.、Veith, Helmut、Bloem, Roderick (編)。モデル検査ハンドブック。p. 191。
^ Chaki, Sagar; Gurfinkel, Arie (2018). 「BDD ベースのシンボリックモデル検査」。Clarke, Edmund M.、Henzinger, Thomas A.、Veith, Helmut、Bloem, Roderick (編)。モデル検査ハンドブック。p. 191。
^ Prasad, Mukul R; Biere, Armin; Gupta, Aarti (2005 年 1 月 25 日)。「SAT ベースの形式検証における最近の進歩の調査」。技術移転のためのソフトウェアツールに関する国際ジャーナル。7 (2): 156–173。doi : 10.1007 /s10009-004-0183-4。
^ ビョルナー、ダインズ;グラム、クリスチャン。オエスト、オーレ・N.リストローム、レイフ (2011)。「ダンスク・データマティック・センター」。インパリアッツォでは、ジョン。ルンディン、パー;ベングラー、ベンクト編（編）。北欧コンピューティングの歴史 3: 情報通信技術における IFIP の進歩。スプリンガー。 350–359ページ。
^ Bjørner, Dines; Havelund, Klaus. 「形式手法の 40 年: いくつかの障害といくつかの可能性?」 FM 2014: 形式手法: 第 19 回国際シンポジウム、シンガポール、2014 年 5 月 12 ～ 16 日。議事録(PDF)。Springer。pp. 42 ～ 61。
^ Gheorghe, AV、Ancel, E. (2008 年 11 月)。無人航空システムの国家航空システムへの統合。インフラストラクチャシステムとサービス: より明るい未来のためのネットワークの構築 (INFRA)、2008 年第 1 回国際会議 (pp. 1-5)。IEEE。
^ 空中協調紛争解決および検出、http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ 2016-03-05 にWayback Machineでアーカイブ
^ 「アトリエB」。www.atelierb.eu。
^ CT Chou、PK Mannava、S. Park、「キャッシュコヒーレンスプロトコルのパラメータ化された検証のための簡単な方法」、コンピュータ支援設計における形式手法、pp. 382–398、2004年。
^ Intel Core i7 プロセッサ実行エンジン検証における形式検証、http://cps-vo.org/node/1371、Wayback Machineで 2015 年 5 月 3 日にアーカイブ、2013 年 9 月 13 日にアクセス。
^ J. Grundy、「Intel IA-64 アーキテクチャの検証済み最適化」、Theorem Proving in Higher Order Logics、Springer Berlin Heidelberg、2004 年、215 ～ 232 ページ。
^ E. Seligman、I. Yarom、「Cadence Conformal LEC を使用するための最もよく知られた方法」、Intel。
^ C. Eisner、A. Nahir、K. Yorav、「構成的推論による電力ゲート設計の機能検証^{[ permanent dead link ]}」、Computer Aided Verification、Springer Berlin Heidelberg、pp. 433–445。
^ PC Attie、H. Chockler、「フォールトトレラントレジスタエミュレーションの自動検証」、Electronic Notes in Theoretical Computer Science、vol. 149、no. 1、pp. 49–60。
^ 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。
^ X2R-2、成果物D5.1。
^ ダニエル・ジャクソンとジャネット・ウィング、「軽量形式手法」、IEEE Computer、1996年4月
^ Vinu George と Rayford Vaughn、「要件エンジニアリングにおける軽量形式手法の適用」、Wayback Machineに 2006-03-01 にアーカイブ、Crosstalk: The Journal of Defense Software Engineering、2003 年 1 月
^ ダニエル・ジャクソン、「Alloy: 軽量オブジェクトモデリング表記法」、ACM Transactions on Software Engineering and Methodology (TOSEM)、第 11 巻、第 2 号 (2002 年 4 月)、256-290 ページ
^ Richard Denney、「ユースケースで成功する：スマートに作業して品質を実現する」、Addison-Wesley Professional Publishing、2005 年、ISBN 0-321-31643-6。
^ Sten Agerholm と Peter G. Larsen、「形式手法への軽量アプローチ」、Wayback Machineで 2006-03-09 にアーカイブ、応用形式手法の最新動向に関する国際ワークショップの議事録、ドイツ、ボッパルト、Springer-Verlag、1998 年 10 月
^ "ESBMC". esbmc.org .
^ 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: 形式手法のコンペティションの概要」。Beyer, Dirk; Huisman, Marieke; Kordon, Fabrice; Steffen, Bernhard (編)。システムの構築と分析のためのツールとアルゴリズム。コンピュータサイエンスの講義ノート。Cham: Springer International Publishing。pp. 3–24。土井: 10.1007/978-3-030-17502-3_1。ISBN 978-3-030-17502-3。
^ フロレイクス、ニルス;ヘーレ、マリジン。イゼル、マルクス。ヤルビサロ、マッティ。須田、マーティン（2021-12-01）。「SATコンペティション2020」。人工知能。301 : 103572.土井: 10.1016/j.artint.2021.103572。ISSN 0004-3702。
^ Cornejo, César (2021-01-27). 「Alloy の SAT ベースの算術サポート」。第 35 回 IEEE/ACM 国際自動ソフトウェアエンジニアリング会議の議事録。ASE '20。米国ニューヨーク州ニューヨーク: Association for Computing Machinery。pp. 1161–1163。doi : 10.1145/ 3324884.3415285。ISBN 978-1-4503-6768-4。
^ 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.
^ 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.
^ 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。
^ Pulina, Luca; Seidl, Martina (2019-09-01). 「2016 年と 2017 年の QBF ソルバーの評価 (QBFEVAL'16 と QBFEVAL'17)」。人工知能。274 : 224–248。doi : 10.1016/ j.artint.2019.04.002。ISSN 0004-3702。
^ Beyer, Dirk (2022). 「ソフトウェア検証の進歩: SV-COMP 2022」。Fisman, Dana、Rosu, Grigore (編)。システムの構築と分析のためのツールとアルゴリズム。コンピュータサイエンスの講義ノート。第13244巻。Cham: Springer International Publishing。pp. 375–402。doi : 10.1007 / 978-3-030-99527-0_20。ISBN 978-3-030-99527-0。
^ Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). 「SyGuS-Comp 2017: 結果と分析」.理論計算機科学電子会議. 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 年。
ヒューバート・ガラベル（編集者）とスザンヌ・グラフ。安全でセキュアなコンピュータシステムのための形式的手法^{[永久デッドリンク]}。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 の形式手法

アーカイブ資料

Archive.org経由のMicrosoft Academic Searchの形式手法キーワード
DEPLOY がサポートする形式手法の使用と業界への影響に関する証拠。2012 年 6 月 8 日にArchive.orgのWayback Machineプロジェクト (EU FP7)にアーカイブされました。

[butler-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] モナン、pp.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 会議で提案された国際代数言語の構文と意味論」。国際情報処理会議の議事録。ユネスコ。

[6] Knuth, Donald E. (1964)、Backus Normal Form と Backus Naur Form。Communications of the ACM、7(12):735–736。

[7] O'Hearn, Peter W.; Tennent, Robert D. (1997). Algol のような言語。

[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-03-05 に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、「構成的推論による電力ゲート設計の機能検証^{[ permanent dead link ]}」、Computer Aided Verification、Springer Berlin Heidelberg、pp. 433–445。

[24] PC Attie、H. Chockler、「フォールトトレラントレジスタエミュレーションの自動検証」、Electronic Notes in Theoretical Computer Science、vol. 149、no. 1、pp. 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-03-01 にアーカイブ、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] Richard Denney、「ユースケースで成功する：スマートに作業して品質を実現する」、Addison-Wesley Professional Publishing、2005 年、ISBN 0-321-31643-6。

[31] Sten Agerholm と Peter G. Larsen、「形式手法への軽量アプローチ」、Wayback Machineで 2006-03-09 にアーカイブ、応用形式手法の最新動向に関する国際ワークショップの議事録、ドイツ、ボッパルト、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: 形式手法のコンペティションの概要」。Beyer, Dirk; Huisman, Marieke; Kordon, Fabrice; Steffen, Bernhard (編)。システムの構築と分析のためのツールとアルゴリズム。コンピュータサイエンスの講義ノート。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 ベースの算術サポート」。第 35 回 IEEE/ACM 国際自動ソフトウェアエンジニアリング会議の議事録。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] Pulina, Luca; Seidl, Martina (2019-09-01). 「2016 年と 2017 年の QBF ソルバーの評価 (QBFEVAL'16 と QBFEVAL'17)」。人工知能。274 : 224–248。doi : 10.1016/ j.artint.2019.04.002。ISSN 0004-3702。

[40] Beyer, Dirk (2022). 「ソフトウェア検証の進歩: SV-COMP 2022」。Fisman, Dana、Rosu, Grigore (編)。システムの構築と分析のためのツールとアルゴリズム。コンピュータサイエンスの講義ノート。第13244巻。Cham: 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: 結果と分析」.理論計算機科学電子会議. 260 : 97–115. arXiv : 1611.07627 . doi : 10.4204/EPTCS.260.9 . ISSN 2075-2180.

用途

仕様

合成

検証

サインオフ検証

人間主導の証明

自動証明

テクニック

仕様言語

二分決定図

SAT ソルバー

アプリケーション

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

半形式的手法

形式手法と記法

仕様言語

モデルチェッカー

解答者と競技

組織

参照

参考文献

さらに読む

外部リンク

関連するトピック

コンピュータサイエンス

ソフトウェア

ハードウェア

仕様