形式的手法は,主に2つに大別される。1つは,ソフトウエアの仕様を「形式的な仕様記述言語」を使って論理的に記述したり,検査したりすることで,少しでも早い段階でバグを洗い出す「仕様記述」。もう1つは,形式的な仕様記述言語とは別の専用言語で記述したシステムの状態遷移をコンピュータに入力することで,振る舞いにバグがないかどうかを高速かつ自動的に探索する「形式検証(モデル検査)」である。いずれも形式的手法の一種ではあるものの,使いこなしの観点や利点はかなり趣を異にしている。

この先は会員の登録が必要です。有料会員(月額プラン)は初月無料!