形式的検証の手法
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/11/10 06:15 UTC 版)
形式的検証の手法は大きく2つに分類される。 第一の手法はモデル検査と呼ばれる。これは数理モデルの体系的かつ徹底的な検証を意味する（有限なモデルでのみ可能だが、無限の状態を持つモデルであっても抽象化によって有限な表現が可能であれば検証可能である）。一般にモデル内の全状態と全遷移の検証を含み、演算時間を減らすために領域固有の抽象化技法などを駆使して効率化を図る。実装技法には状態空間列挙法（英語版）、抽象状態空間列挙法、抽象解釈、記号シミュレーション（英語版）、abstraction refinment などがある。検証される特性（プロパティ）は時相論理で記述され、線形時相論理 (LTL) や計算木論理 (CTL) が使われる。 第二の手法は論理的推論である。一般に HOL、ACL2、Isabelle、Coq といった定理証明ソフトウェアを使い、システムに関して形式的な推論を行う。この手法は完全自動化されていないのが一般的で、ユーザーの対象システムについての理解に応じて行われる。最近では、Perfect Developer や Escher C Verifier といったツールが証明の完全自動化を試みている。 線形論理や時相論理などの非古典論理は、モデル検査だけでなく論理的推論でも使われる。
※この「形式的検証の手法」の解説は、「形式的検証」の解説の一部です。
「形式的検証の手法」を含む「形式的検証」の記事については、「形式的検証」の概要を参照ください。
ウィキペディア小見出し辞書の「形式的検証の手法」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ。
- 形式的検証の手法のページへのリンク
