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

m
形式的検証の適用例としては、内部にメモリを持つ暗号回路、組み合わせ回路、デジタル回路などのシステム、ソースコードで表現されるソフトウェアがある。
 
これらのシステムの検証は、システムを抽象化した数学的モデル上で行われ、そのモデルに対応する実際のシステムは一種類とは限らない。使用される数学的モデルとしては、[[有限状態機械]]、labelled transition system[[状態遷移系|ラベル付き遷移系]]、[[ペトリネット]]、timed automata、hybrid automata、[[プロセス代数]]、プログラミング言語の形式意味論(操作的意味論、表示的意味論)、[[ホーア論理]]などがある。
 
== 形式的検証の手法 ==
25,487

回編集