「形式的検証」の版間の差分

出典: フリー百科事典『ウィキペディア（Wikipedia）』
履歴の双方向閲覧
← 古い編集新しい編集 →
削除された内容 追加された内容
ビジュアルウィキテキスト
Luckas-bot (会話 | 投稿記録)
384,485 回編集
m r2.5.2) (ロボットによる 追加: el:Τυπική επαλήθευση
Melan (会話 | 投稿記録)
25,487 回編集
en:Formal verification（2012年5月3日 15:35:38(UTC)）の翻訳（一部省略）をマージ
1行目: 1行目:
'''形式的検証'''（けいしきてきけんしょう）とは、[[ハードウェア]]および[[ソフトウェア]]のシステムにおいて[[形式手法]]や[[数学]]を利用し、何らかの[[形式仕様]]やプロパティに照らしてシステムが正しいことを[[証明]]したり、逆に正しくないことを証明することである。
'''形式的検証'''（けいしきてきけんしょう）とは、[[ハードウェア]]および[[ソフトウェア]]のシステムにおいて[[形式手法]]や[[数学]]を利用し、何らかの[[形式仕様記述]]やプロパティに照らしてシステムが正しいことを[[証明]]したり、逆に正しくないことを証明することである{{要出典|date=2009年6月}}。


{{Quote box|width=30em |quoted=true |bgcolor=#FFFFF0 |salign=center|完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。|[[Association for Computing Machinery|ACM]]シンポジウムで発表された論文の要約から<ref>{{Cite web |url= http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf |title= seL4: Formal Verification of an OS Kernel (paper submitted to 22nd ACM Symposium on Operating Systems Principles, October 2009) |author= Gerwin Klein |coauthors= 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 |accessdate= 2011-11-07}}</ref>}}
⚫
== 説明 ==
[[ソフトウェアテスト]]のみでは、システムが特定の欠陥を持っていないことを証明できない。また、システムが必要な特性（プロパティ）を持っていることも証明できない。「形式的」な検証をすることで、特定の欠陥がなく必要な特性を持っていることを証明できる。システムが「全く」欠陥を持たないことを証明したり、テストしたりすることはできない。というのも、「欠陥がない」ということの形式的定義が不可能だからである。従って我々ができるのは、システムに想定される欠陥がなく、使用するに当たって必要とされる機能が全て備わっていることを証明することだけである。


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


これらのシステムの検証は、システムを抽象化した数学的モデル上で行われ、そのモデルに対応する実際のシステムは一種類とは限らない。使用される数学的モデルとしては、[[有限状態機械]]、[[状態遷移系|ラベル付き遷移系]]、[[ペトリネット]]、timed automata、hybrid automata、[[プロセス代数]]、[[プログラム意味論|プログラミング言語の形式意味論]]（[[操作的意味論]]、[[表示的意味論]]）、[[ホーア論理]]などがある。
これらのシステムの検証は、システムを抽象化した[[数理モデル]]上で行われ、その数理モデルと実際のシステムの性質は一致している。使用される数理モデルとしては、[[有限状態機械]]、[[状態遷移系|ラベル付き遷移系]]、[[ペトリネット]]、[[:en:timed automaton|timed automata]]、[[:en:hybrid automata|hybrid automata]]、[[プロセス計算]]、[[プログラム意味論|プログラミング言語の形式意味論]]（[[操作的意味論]]、[[表示的意味論]]、[[公理的意味論]]）、[[ホーア論理]]などがある{{要出典|date=2009年9月}}。


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


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


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


検証される特性（プロパティ）は[[時相論理]]で記述され、[[線形時相論理]]や[[計算木論理]]が使われる。
[[線形論理]]や[[時相論理]]などの[[非古典論理学|非古典論理]]は、モデル検査だけでなく論理的推論でも使われる。

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

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

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


== Validation と Verification ==
== Validation と Verification ==
24行目: 31行目:
* '''Verification''': 「我々は製品を正しく作っているか？」すなわち、その製品は仕様通りに作られているか？
* '''Verification''': 「我々は製品を正しく作っているか？」すなわち、その製品は仕様通りに作られているか？


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

== 産業での応用 ==
設計の複雑さが増すにつれ、形式的検証技法の重要性は特にハードウェア業界で増している<ref>{{Cite journal|doi=10.1109/LICS.2003.1210044|title=Formal verification at Intel|year=2003|last1=Harrison|first1=J.|pages=45–54}}</ref><ref>[http://portal.acm.org/citation.cfm?id=800667 Formal verification of a real-time hardware design]. Portal.acm.org (1983-06-27). Retrieved on 2011-04-30.</ref>。コンポーネント間の潜在的な微妙な相互作用により、シミュレーションだけで考えられる組合せをすべて調べるのは難しくなってきている。ハードウェア設計の重要な面は自動化証明技法に適しており、形式的検証の導入が容易で生産的である<ref>[http://www.cl.cam.ac.uk/~jrh13/slides/types-04sep99/slides1.pdf Formal Verification in Industry]</ref>。


2011年現在、いくつかの[[オペレーティングシステム]]が形式的検証を採用している。
== プログラム検証 ==
* [[L4|Embedded L4 microkernel]]（[[:en:NICTA|NICTA]]）<ref name="Ganssle">[http://www.embedded.com/columns/breakpoint/220900551 "A new OS has been proven to be correct using mathematical proofs. The cost: astronomical."] by Jack Ganssle</ref>
'''プログラム検証'''とは、仕様書通りに[[プログラム (コンピュータ)|プログラム]]が書かれているかを検証するプロセスである。この場合、数学的モデルに還元せずにソースコード自体に一種の形式的検証を行う。
* [[:en:Integrity (operating system)|Integrity]]（[[:en:Green Hills Software|Green Hills Software]]）<ref name="Ganssle"/>
* [[PikeOS]]（[[:en:SYSGO|SYSGO]]）<ref>Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer [http://www-wjp.cs.uni-saarland.de/publikationen/Ba10EW.pdf Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS]</ref>


⚫
== 脚注 ==
[[関数型言語]]では、一部のプログラムは[[数学的帰納法]]によって検証可能である。命令型言語のコードは[[ホーア論理]]を使って検証可能である。
{{Reflist}}


== 関連項目 ==
== 関連項目 ==
37行目: 50行目:
* [[自動定理証明]]
* [[自動定理証明]]


[[Category:デジタル回路|けいしきてきけんしよう]]
{{DEFAULTSORT:けいしきてきけんしよう}}
[[Category:ソフトウェア工学|けいしきてきけんしよう]]
[[Category:理論計算機科学]]
[[Category:形式手法|けいしきてきけんしよう]]
[[Category:デジタル回路]]
[[Category:ソフトウェア工学]]
⚫
[[Category:数学に関する記事|けいしきてきけんしよう]]
[[Category:形式手法]]
⚫
[[Category:数学に関する記事]]


[[cs:Formální verifikace]]
[[cs:Formální verifikace]]

2012年9月7日 (金) 03:30時点における版

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

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

使い方

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

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

形式的検証の手法

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

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

第二の手法は論理的推論である。一般に HOL、ACL2、Isabelle、Coq といった定理証明ソフトウェアを使い、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。最近では、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

関連項目

「https://ja.wikipedia.org/w/index.php?title=形式的検証&oldid=44077688」から取得