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

m
wikify
m (robot Adding: cs:Formální verifikace)
m (wikify)
'''形式的検証'''(けいしきてきけんしょう)とは、[[ハードウェア]]および[[ソフトウェア]]のシステムにおいて[[形式手法]]や[[数学]]を利用し、何らかの[[形式仕様]]やプロパティに照らしてシステムが正しいことを[[証明]]したり、逆に正しくないことを証明することである。
 
== 説明 ==
形式的検証の適用例としては、内部にメモリを持つ暗号回路、組み合わせ回路、デジタル回路などのシステム、ソースコードで表現されるソフトウェアがある。
 
これらのシステムの検証は、システムを抽象化した数学的モデル上で行われ、そのモデルに対応する実際のシステムは一種類とは限らない。使用される数学的モデルとしては、[[有限状態機械]]、[[状態遷移系|ラベル付き遷移系]]、[[ペトリネット]]、timed automata、hybrid automata、[[プロセス代数]]、[[プログラム意味論|プログラミング言語の形式意味論]][[操作的意味論]][[表示的意味論]])、[[ホーア論理]]などがある。
 
== 形式的検証の手法 ==