形式手法（Bメソッド） | 技術情報 | 株式会社ヴィッツ形式手法（Bメソッド） 形式手法とは 形式手法は、数学を基盤としたソフトウエアやシステムの仕様記述、検証、開発手法の総称で、数多くの手法が考案されています。 形式仕様記述を用いて厳密に仕様を定義することによる仕様の曖昧性の排除・仕様の前提条件の明確化や、形式検証での数学的解析による開発ソフトウェアの信頼性・頑健性の向上が可能となります。 形式手法の分類 ・形式仕様記述 - モデル規範…集合論・述語論理を用いて仕様を表現 - 性質規範…代数仕様を用いて仕様を表現 ・形式検証 - 定理証明…要求・仕様と設計や実装との間の論理的整合性や一貫性処理の正しさを数学的に証明する - モデル検査…振る舞いについて全状態空間を時相論理式などを用いて自動検査 ・形式プログラム合成 形式手法の分類 機能安全規格IEC 61508や情報セキュリティ評価の為のコモンクライテリアISO/IEC15408といった安全
