形式手法はシステム開発において「仕様の曖昧さを無くす」、「設計のミスを防ぐ」、「実装の間違いを見つけ出す」といった利点があることから、鉄道、航空、原子力発電など重要インフラ² 等における制御システムの開発において、高信頼性を担保するために有効な技術です。1990年代後半から欧州では、安心・安全な生活基盤を整備するため、形式手法を適用したシステム構築が進められました。この結果、重要インフラ等、高信頼性を要求される実システムの開発プロジェクトで形式手法の適用が日本に比べ先行しています。
　また、国際規格において、形式手法の適用は一般的な機械を対象とした機能安全規格³（IEC 61508⁴）等で推奨されています。現在策定が進められている自動車分野の機能安全規格（ISO 26262⁵）においても、適用が言及される見通しで、欧州圏などでは、今後、形式手法を適用しないで開発された製品は、通商上の制約を受ける可能性が考えられます。

　一方、国内では、「扱える技術者が少ない」、「技術者の育成に時間が掛かる」、「ツールの導入が必要」、「費用対効果が不明」等の理由から、実システムの開発プロジェクトへの適用は進んでいません。このような背景から、IPA SECでは、国内の開発現場への適用促進に向けた基礎資料作成のため、欧州を中心に海外調査を行い、形式手法を適用した海外のプロジェクト104件の中から、列車制御システム、航空管制システム、防潮堤制御システム等12件の事例および形式手法ツールベンダの調査等をまとめ、公開しました。

◆　調査を実施した12件の事例

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

• 調査事例の要旨
• 2000年以降、形式手法ツールベンダの出現と共に、実システムの開発プロジェクトへの適用件数が増加してきている。
• 当初は航空、鉄道等の大規模な開発プロジェクトへの適用が中心だったが、近年ではスマートカード等の小規模な開発プロジェクトへの適用が拡大している。
• コード自動生成機能を持ったツールが多く使用されている。ツールを利用すれば形式手法を導入しても工数の増加を抑えることが可能である。
• 形式手法の未経験者でも基本的な開発スキルがあれば、形式手法の研修を受けることで、形式手法を適用するプロジェクトへの従事が可能である。
• 欧州では、形式手法を仕様検証や設計検証を目的として使用するケースが多いのに対して、米国では、実装検証を目的として使用するケースが多い。

　IPA SECでは、本調査結果を基に「形式手法導入・プロセス実証評価ワーキンググループ」等を通して、形式手法を扱える技術者育成のための研修教材の提供をはじめ、国内における形式手法の適用を推進していく予定です。

IPA ソフトウェア・エンジニアリング・センター　田丸

Tel： 03-5978-7543　Fax： 03-5978-7517　E-mail：

IPA　戦略企画部広報グループ　横山／白石

Tel： 03-5978-7503　Fax：03-5978-7510　E-mail：