2010年7月29日
独立行政法人 情報処理推進機構
ソフトウェア・エンジニアリング・センター
概要
形式手法は高信頼性を担保するための有効な技術です。1990年代後半から欧州では、形式手法を適用したシステム構築が進められました。一方、国内では、「扱える技術者が少ない」等の理由から、形式手法の適用は進んでいません。このような背景から、国内の開発現場への適用促進に向けた基礎資料作成のため、本調査を実施しました。
本報告書は、欧州を中心に海外調査を行い、形式手法を適用した海外のプロジェクト104件の中から12件の事例、および形式手法ツールベンダの調査結果等について、とりまとめました。
調査した事例は、下記の通りです。
・防潮可動堤開閉意志決定システム／オランダ
・航空管制システム（iFACT）／イギリス
・無人地下鉄車両の制御（パリ地下鉄14号線）／フランス
・パリ地下鉄プラットフォームドアの制御／フランス
・シャルルドゴール空港の無人シャトル制御／フランス
・北京地下鉄の自動列車停止システム／中国
・サンパウロ地下鉄プラットフォームドア／ブラジル
・ニューヨーク地下鉄カナーシ線列車制御システム（CBTC）の最新化／アメリカ
・航空機のシステム（エアバス）／フランス・ドイツ・スペイン・イギリス
・艦載ヘリコプタ運行限界計装システム（SHOLIS）／イギリス
・コンポーネント仕様のモデル化／フランス
・バイオメトリクスID認証ツールのアクセス管理セキュリティソフトウェア（TIS）／アメリカ
