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

編集の要約なし
m (ロボットによる 追加: pt:Verificação formal)
形式的検証の手法は大きく2つに分類される。
 
第一の手法は[[モデル検査]]と呼ばれる。これは数学的モデルの体系的かつ徹底的な検証を意味する(有限なモデルでのみ可能)。一般にモデル内の全状態と全遷移の検証を含み、演算時間を減らすために領域固有の抽象化技法などを駆使して効率化を図る。実装技法には[[状態空間列挙法]]、抽象状態空間列挙法、[[抽象インタプリタ解釈]]、abstraction refinment などがある。
 
第二の手法は論理的推論である。一般に HOL theorem prover や Isabelle theorem prover などの定理証明ソフトウェアを使って、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。
検証される特性(プロパティ)は[[時相論理]]で記述され、[[線形時相論理]]や[[計算木論理]]が使われる。
 
== Validation と Verification ==
検証(Verification)は製品が目的に適合しているかどうかをテストする観点の1つである。妥当性検証(Validation)はそれを補完する観点と言える。この両者を合わせて検証プロセス全体を V & V と呼ぶこともある。
 
検証プロセスには静的部分と動的部分がある。例えばソフトウェア製品なら、ソースコードの検査ができるし(静的)、特定のテスト条件で実行させることもできる(動的)。妥当性検証(Validation)は動的にしかできない。すなわち、製品を典型的局面で利用してみたり、一般的でない局面で利用してみたりする。
 
== プログラム検証 ==
'''プログラム検証'''とは、仕様書通りに[[プログラム (コンピュータ)|プログラム]]が書かれているかを検証するプロセスである。この場合、数学的モデルに還元せずにソースコード自体に一種の形式的検証を行う。
 
[[関数型言語]]では、一部のプログラムは[[数学的帰納法]]によって検証可能である。命令型言語のコードは[[ホーア論理]]を使って検証可能である。
 
== 関連項目 ==
* [[形式等価判定]]
* [[Property Specification Language]]
* [[静的コード解析]]
* [[自動定理証明]]
 
[[Category:デジタル回路|けいしきてきけんしよう]]
804

回編集