独立行政法人情報処理推進機構のソフトウェア・エンジニアリング・センター(以下、SEC)は7月29日、形式手法に関する調査結果をまとめた『「形式手法適用調査」報告書』を公開した。

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

形式手法は、高信頼性を担保するプログラム開発手法の1つ。独自の仕様記述言語を用いて仕様を記述し、ツールを使ってそれを自動検証することで、仕様の曖昧さを無くし、設計/実装のミスを見つけ出す仕組みになっている。一般的な機械を対象とした機能安全規格「IEC 61508」等で推奨されているほか、現在策定が進められている自動車分野の機能安全規格「ISO 26262」でも適用が言及される見通しで、「欧州圏などでは、今後、形式手法を適用しないで開発された製品は、通商上の制約を受ける可能性が考えられる」という。

IPAでは、欧州を中心に海外調査を実施。形式手法を適用した海外のプロジェクト104件の中から、「列車制御システム」、「航空管制システム」、「防潮堤制御システム」等12件の事例および形式手法ツールベンダの調査等をまとめ、レポートとして公開している。

掲載されている事例は以下のとおり。

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

レポートはSECのWebサイトから無償でダウンロードできる。