プログラム検証とは? わかりやすく解説

Weblio 辞書 > 辞書・百科事典 > ウィキペディア小見出し辞書 > プログラム検証の意味・解説 

形式的検証

(プログラム検証 から転送)

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2023/04/19 13:48 UTC 版)

形式的検証(けいしきてきけんしょう、: formal verification)とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである[要出典]

完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。
ACMシンポジウムで発表された論文の要約から[1]

使い方

形式的検証の適用例としては、内部にメモリを持つ暗号回路、組み合わせ回路、デジタル回路などのシステム、ソースコードで表現されるソフトウェアがある。

これらのシステムの検証は、システムを抽象化した数理モデル上で行われ、その数理モデルと実際のシステムの性質は一致している。使用される数理モデルとしては、有限状態機械ラベル付き遷移系ペトリネットtimed automatahybrid automataプロセス計算プログラミング言語の形式意味論操作的意味論表示的意味論公理的意味論)、ホーア論理などがある[要出典]

形式的検証の手法

形式的検証の手法は大きく2つに分類される。

第一の手法はモデル検査と呼ばれる。これは数理モデルの体系的かつ徹底的な検証を意味する(有限なモデルでのみ可能だが、無限の状態を持つモデルであっても抽象化によって有限な表現が可能であれば検証可能である)。一般にモデル内の全状態と全遷移の検証を含み、演算時間を減らすために領域固有の抽象化技法などを駆使して効率化を図る。実装技法には状態空間列挙法英語版、抽象状態空間列挙法、抽象解釈記号シミュレーション英語版、abstraction refinment などがある。検証される特性(プロパティ)は時相論理で記述され、線形時相論理 (LTL) や計算木論理 (CTL) が使われる。

第二の手法は論理的推論である。一般に HOLACL2IsabelleCoq といった定理証明ソフトウェアを使い、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。最近では、Perfect Developer や Escher C Verifier といったツールが証明の完全自動化を試みている。

線形論理時相論理などの非古典論理は、モデル検査だけでなく論理的推論でも使われる。

ソフトウェアの形式的検証

ソフトウェアの形式的検証のための論理推論はさらに以下のように分類される。

  • 1970年代のより古典的手法では、まずコードを普通に書き、続いてのステップで正しいことを検証する。
  • 依存型プログラミング英語版では、関数の型がその関数の仕様(の一部)を含み、コードの型チェックによって仕様に対する正しさが保証される。完全な依存型プログラミング言語は第一の手法を特殊ケースとしてサポートする。

それとは相補的な若干異なる手法としてプログラム導出がある。その場合、正しさを保持したステップを踏んで関数仕様から効率的コードを生成する。例として Bird-Meertens Formalism (BMF) があり、"correctness by construction" の別の形態と見ることもできる。

Validation と Verification

検証(Verification)は製品が目的に適合しているかどうかをテストする観点の1つである。妥当性検証(Validation)はそれを補完する観点と言える。この両者を合わせて検証プロセス全体を V & V と呼ぶこともある。

  • Validation: 「我々は正しい製品を作っているか?」すなわち、その製品はユーザーが本当に必要とすることを行っているか?
  • Verification: 「我々は製品を正しく作っているか?」すなわち、その製品は仕様通りに作られているか?

検証プロセスには静的部分と動的部分がある。例えばソフトウェア製品なら、ソースコードの検査ができるし(静的)、特定のテスト条件で実行させることもできる(動的)。妥当性検証(Validation)は動的にしかできない。すなわち、製品を典型的局面で利用してみたり、一般的でない局面で利用してみたりする(すなわち、それはあらゆるユースケースに対して満足できる動作をするか、である)。

産業での応用

設計の複雑さが増すにつれ、形式的検証技法の重要性は特にハードウェア業界で増している[2][3]。コンポーネント間の潜在的な微妙な相互作用により、シミュレーションだけで考えられる組合せをすべて調べるのは難しくなってきている。ハードウェア設計の重要な面は自動化証明技法に適しており、形式的検証の導入が容易で生産的である[4]

2011年現在、いくつかのオペレーティングシステムが形式的検証を採用している。

脚注

  1. ^ Gerwin Klein; Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood et al. “seL4: Formal Verification of an OS Kernel (paper submitted to 22nd ACM Symposium on Operating Systems Principles, October 2009)”. 2011年11月7日閲覧。
  2. ^ Harrison, J. (2003). Formal verification at Intel. pp. 45–54. doi:10.1109/LICS.2003.1210044. 
  3. ^ Formal verification of a real-time hardware design. Portal.acm.org (1983-06-27). Retrieved on 2011-04-30.
  4. ^ Formal Verification in Industry
  5. ^ a b "A new OS has been proven to be correct using mathematical proofs. The cost: astronomical." by Jack Ganssle
  6. ^ Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS

関連項目


プログラム検証

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/07 01:59 UTC 版)

銀の弾などない」の記事における「プログラム検証」の解説

プログラム検証には労力がかかる。そのため、全ての開発対象検証することはできず、一部重要なプログラム検証することしかできないまた、たとえプログラム検証したとしても、それは、プログラム仕様書通り実装されていることを証明するだけであり、仕様書バグがないことを証明するわけではないプログラム開発本質多く部分は、仕様書デバッグである。 完全で一貫した仕様書到達することは、非常に難し作業である。

※この「プログラム検証」の解説は、「銀の弾などない」の解説の一部です。
「プログラム検証」を含む「銀の弾などない」の記事については、「銀の弾などない」の概要を参照ください。

ウィキペディア小見出し辞書の「プログラム検証」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ


英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

すべての辞書の索引

「プログラム検証」の関連用語

プログラム検証のお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



プログラム検証のページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアの形式的検証 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。
ウィキペディアウィキペディア
Text is available under GNU Free Documentation License (GFDL).
Weblio辞書に掲載されている「ウィキペディア小見出し辞書」の記事は、Wikipediaの銀の弾などない (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。

©2025 GRAS Group, Inc.RSS