DSF、東証のシステムで「形式手法」の有用性を確認

要求定義や設計段階でエラーやミスの混入を防ぐには、どうすればいいか。有力な解の一つが形式手法(Formal Method）である。自動車や電子機器など他の工業製品（ハードウェア）と違って、ソフトウェアには融通無碍という特徴があり、だからこそ様々なハードをソフトで置き換える試みが進む。だがこの特徴がシステムの信頼性や安全性を損なう要因でもある。そこで数理論理学に基づく仕様記述によってこの問題を解決するのが形式手法、という因果関係だ（本誌2011年11月号「ソフトウェアの信頼性を根本的に高める「形式手法（Formal Method）」の本質」参照）。