アーカイブ

「形式手法適用調査」報告書

2010年7月29日
独立行政法人 情報処理推進機構
ソフトウェア・エンジニアリング・センター

概要

 形式手法は高信頼性を担保するための有効な技術です。1990年代後半から欧州では、形式手法を適用したシステム構築が進められました。一方、国内では、「扱える技術者が少ない」等の理由から、形式手法の適用は進んでいません。このような背景から、国内の開発現場への適用促進に向けた基礎資料作成のため、本調査を実施しました。
 本報告書は、欧州を中心に海外調査を行い、形式手法を適用した海外のプロジェクト104件の中から12件の事例、および形式手法ツールベンダの調査結果等について、とりまとめました。
 調査した事例は、下記の通りです。

・防潮可動堤開閉意志決定システム/オランダ
・航空管制システム(iFACT)/イギリス
・無人地下鉄車両の制御(パリ地下鉄14号線)/フランス
・パリ地下鉄プラットフォームドアの制御/フランス
・シャルルドゴール空港の無人シャトル制御/フランス
・北京地下鉄の自動列車停止システム/中国
・サンパウロ地下鉄プラットフォームドア/ブラジル
・ニューヨーク地下鉄カナーシ線列車制御システム(CBTC)の最新化/アメリカ
・航空機のシステム(エアバス)/フランス・ドイツ・スペイン・イギリス
・艦載ヘリコプタ運行限界計装システム(SHOLIS)/イギリス
・コンポーネント仕様のモデル化/フランス
・バイオメトリクスID認証ツールのアクセス管理セキュリティソフトウェア(TIS)/アメリカ

ダウンロード

注:コンテンツは2つあります。それぞれPDF形式での提供となっております。
調査概要資料[1.30MB]PDF文書   
調査報告書[1.81MB]PDF文書