「形式手法適用調査」報告書 : 情報処理推進機構：ソフトウェアエンジニアリング形式手法は高信頼性を担保するための有効な技術です。1990年代後半から欧州では、形式手法を適用したシステム構築が進められました。一方、国内では、「扱える技術者が少ない」等の理由から、形式手法の適用は進んでいません。このような背景から、国内の開発現場への適用促進に向けた基礎資料作成のため、本調査を実施しました。 本報告書は、欧州を中心に海外調査を行い、形式手法を適用した海外のプロジェクト104件の中から12件の事例、および形式手法ツールベンダの調査結果等について、とりまとめました。 調査した事例は、下記の通りです。 ・防潮可動堤開閉意志決定システム／オランダ ・航空管制システム（iFACT）／イギリス ・無人地下鉄車両の制御（パリ地下鉄14号線）／フランス ・パリ地下鉄プラットフォームドアの制御／フランス ・シャルルドゴール空港の無人シャトル制御／フランス ・北京地下鉄の自動列車停止システム
