|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。 ・ 形 ： [けい, かたち, ぎょう] 1. (suf) shape 2. form 3. type ・ 形式 ： [けいしき] 【名詞】 1. (1) form 2. formality 3. format 4. (2) appearance 5. mode 6. (3) math expression ・ 形式的 ： [けいしきてき] 1. (adj-na) formal ・ 式 ： [しき] 1. (n,n-suf) (1) equation 2. formula 3. expression 4. (2) ceremony 5. (3) style ・ 的 ： [まと, てき] 【名詞】 1. mark 2. target ・ 検証 ： [けんしょう] 1. (n,vs) verification 2. inspection ・ 証 ： [あかし, しょう] (n) 1. proof 2. evidence
形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 == 使い方 == 形式的検証の適用例としては、内部にメモリを持つ暗号回路、組み合わせ回路、デジタル回路などのシステム、ソースコードで表現されるソフトウェアがある。 これらのシステムの検証は、システムを抽象化した数理モデル上で行われ、その数理モデルと実際のシステムの性質は一致している。使用される数理モデルとしては、有限状態機械、ラベル付き遷移系、ペトリネット、timed automata、hybrid automata、プロセス計算、プログラミング言語の形式意味論（操作的意味論、表示的意味論、公理的意味論）、ホーア論理などがある。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「形式的検証」の詳細全文を読む スポンサード リンク
|