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

en:Formal verification(2012年5月3日 15:35:38(UTC))の翻訳(一部省略)をマージ
m (r2.5.2) (ロボットによる 追加: el:Τυπική επαλήθευση)
(en:Formal verification(2012年5月3日 15:35:38(UTC))の翻訳(一部省略)をマージ)
'''形式的検証'''(けいしきてきけんしょう)とは、[[ハードウェア]]および[[ソフトウェア]]のシステムにおいて[[形式手法]]や[[数学]]を利用し、何らかの[[形式仕様記述]]やプロパティに照らしてシステムが正しいことを[[証明]]したり、逆に正しくないことを証明することである{{要出典|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>}}
== 説明 ==
[[ソフトウェアテスト]]のみでは、システムが特定の欠陥を持っていないことを証明できない。また、システムが必要な特性(プロパティ)を持っていることも証明できない。「形式的」な検証をすることで、特定の欠陥がなく必要な特性を持っていることを証明できる。システムが「全く」欠陥を持たないことを証明したり、テストしたりすることはできない。というのも、「欠陥がない」ということの形式的定義が不可能だからである。従って我々ができるのは、システムに想定される欠陥がなく、使用するに当たって必要とされる機能が全て備わっていることを証明することだけである。
 
== 使い方 ==
形式的検証の適用例としては、内部にメモリを持つ暗号回路、組み合わせ回路、[[デジタル回路]]などのシステム、[[ソースコード]]で表現される[[ソフトウェア]]がある。
 
これらのシステムの検証は、システムを抽象化した[[学的モデル]]上で行われ、その数理モデルに対応する実際のシステムの性質は一種類とは限らな致して。使用される数学的モデルとしては、[[有限状態機械]]、[[状態遷移系|ラベル付き遷移系]]、[[ペトリネット]]、[[:en:timed automaton|timed automata]][[:en:hybrid automata|hybrid automata]]、[[プロセス代数計算]]、[[プログラム意味論|プログラミング言語の形式意味論]]([[操作的意味論]]、[[表示的意味論]]、[[公理的意味論]])、[[ホーア論理]]などがある{{要出典|date=2009年9月}}
 
== 形式的検証の手法 ==
形式的検証の手法は大きく2つに分類される。
 
第一の手法は[[モデル検査]]と呼ばれる。これは数学的モデルの体系的かつ徹底的な検証を意味する([[有限モデル理論|有限なモデル]]でのみ可能だが、無限の状態を持つモデルであっても抽象化によって有限な表現が可能であれば検証可能である)。一般にモデル内の全状態と全遷移の検証を含み、演算時間を減らすために領域固有の抽象化技法などを駆使して効率化を図る。実装技法には[[{{仮リンク|状態空間列挙法]]|en|state space enumeration}}、抽象状態空間列挙法、[[抽象解釈]]、{{仮リンク|記号シミュレーション|en|symbolic simulation}}、abstraction refinment などがある。検証される特性(プロパティ)は[[時相論理]]で記述され、[[線形時相論理]] (LTL) や[[計算木論理]] (CTL) が使われる。
 
第二の手法は論理的推論である。一般に [[:en:HOL theorem(proof proverassistant)|HOL]]、[[:en:ACL2|ACL2]]、[[:en:Isabelle (proof assistant)|Isabelle]]、[[:en:Coq|Coq]] theorem prover などのといった[[自動定理証明|定理証明]]ソフトウェアを使って、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。最近では、[[: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 ==
* '''Verification''': 「我々は製品を正しく作っているか?」すなわち、その製品は仕様通りに作られているか?
 
検証プロセスには静的部分と動的部分がある。例えばソフトウェア製品なら、ソースコードの検査ができるし(静的)、特定のテスト条件で実行させることもできる(動的)。妥当性検証(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}}
 
== 関連項目 ==
* [[自動定理証明]]
 
[[Category{{DEFAULTSORT:デジタル回路|けいしきてきけんしよう]]}}
[[Category:ソフトウェア工理論計算機科|けいしきてきけんしよう]]
[[Category:形式手法|けいしきてきけんしようデジタル回路]]
[[Category:ソフトウェア工学]]
[[Category:数学に関する記事|けいしきてきけんしよう]]
[[Category:形式手法]]
[[Category:数学に関する記事|けいしきてきけんしよう]]
 
[[cs:Formální verifikace]]
25,487

回編集