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

この記事は会員登録で続きをご覧いただけます

日経クロステック登録会員になると…

新着が分かるメールマガジンが届く
キーワード登録、連載フォローが便利

さらに、有料会員に申し込むとすべての記事が読み放題に!
春割キャンペーン実施中!
>>詳しくは


日経クロステックからのお薦め

春割キャンペーン実施中!
日経BP総研の問い合わせフォーム

企業価値を高めたいとお悩みなら

日経BP 総合研究所がお話を承ります。ESG/SDGs対応から調査、情報開示まで、お気軽にお問い合わせください。

ブランド強化、認知度向上、エンゲージメント強化、社内啓蒙、新規事業創出…。各種の戦略・施策立案をご支援します。詳細は下のリンクから。

日経BP総研の問い合わせフォームへ行く

日経BPで働きませんか

日経BPで働きませんか

「デジタル&ソリューション」をキーワードに、多様な事業を展開しています。

日経BPは、デジタル部門や編集職、営業職・販売職でキャリア採用を実施しています。デジタル部門では、データ活用、Webシステムの開発・運用、決済システムのエンジニアを募集中。詳細は下のリンクからご覧下さい。

Webシステムの開発・運用(医療事業分野)

システム開発エンジニア(自社データを活用した事業・DX推進)

システム開発エンジニア(契約管理・課金決済システム/ECサイト)