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

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

回編集