提供: miniwiki

← 形式的検証

あなたには「このページの編集」を行う権限がありません。理由は以下の通りです:

---

このページのソースの閲覧やコピーができます。

'''形式的検証'''（けいしきてきけんしょう）とは、[[ハードウェア]]および[[ソフトウェア]]のシステムにおいて[[形式手法]]や[[数学]]を利用し、何らかの[[形式仕様記述]]やプロパティに照らしてシステムが正しいことを[[証明]]したり、逆に正しくないことを証明することである{{要出典|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 (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 == 検証(Verification)は製品が目的に適合しているかどうかをテストする観点の1つである。妥当性検証(Validation)はそれを補完する観点と言える。この両者を合わせて検証プロセス全体を V & V と呼ぶこともある。 * '''Validation''': 「我々は正しい製品を作っているか？」すなわち、その製品はユーザーが本当に必要とすることを行っているか？ * '''Verification''': 「我々は製品を正しく作っているか？」すなわち、その製品は仕様通りに作られているか？ 検証プロセスには静的部分と動的部分がある。例えばソフトウェア製品なら、ソースコードの検査ができるし（静的）、特定のテスト条件で実行させることもできる（動的）。妥当性検証(Validation)は動的にしかできない。すなわち、製品を典型的局面で利用してみたり、一般的でない局面で利用してみたりする（すなわち、それはあらゆる[[ユースケース]]に対して満足できる動作をするか、である）。 == 脚注 == {{Reflist}} == 関連項目 == * [[形式等価判定]] * [[Property Specification Language]] * [[静的コード解析]] * [[自動定理証明]] {{DEFAULTSORT:けいしきてきけんしよう}} [[Category:理論計算機科学]] [[Category:デジタル回路]] [[Category:ソフトウェア工学]] [[Category:形式手法]] [[Category:数学に関する記事]]

形式的検証 に戻る。