独立行政法人情報処理推進機構のソフトウェア・エンジニアリング・センター(以下、SEC)は7月29日、形式手法に関する調査結果をまとめた『「形式手法適用調査」報告書』を公開した。
形式手法は、高信頼性を担保するプログラム開発手法の1つ。独自の仕様記述言語を用いて仕様を記述し、ツールを使ってそれを自動検証することで、仕様の曖昧さを無くし、設計/実装のミスを見つけ出す仕組みになっている。一般的な機械を対象とした機能安全規格「IEC 61508」等で推奨されているほか、現在策定が進められている自動車分野の機能安全規格「ISO 26262」でも適用が言及される見通しで、「欧州圏などでは、今後、形式手法を適用しないで開発された製品は、通商上の制約を受ける可能性が考えられる」という。
IPAでは、欧州を中心に海外調査を実施。形式手法を適用した海外のプロジェクト104件の中から、「列車制御システム」、「航空管制システム」、「防潮堤制御システム」等12件の事例および形式手法ツールベンダの調査等をまとめ、レポートとして公開している。
掲載されている事例は以下のとおり。
- 防潮可動堤開閉意志決定システム - オランダ
- 航空管制システム(iFACT) - イギリス
- 無人地下鉄車両の制御(パリ地下鉄14号線) - フランス
- パリ地下鉄プラットフォームドアの制御 - フランス
- シャルルドゴール空港の無人シャトル制御 - フランス
- 北京地下鉄の自動列車停止システム - 中国
- サンパウロ地下鉄プラットフォームドア - ブラジル
- ニューヨーク地下鉄カナーシ線列車制御システム(CBTC)の最新化 - アメリカ
- 航空機のシステム(エアバス) - フランス・ドイツ・スペイン・イギリス
- 艦載ヘリコプタ運行限界計装システム(SHOLIS) - イギリス
- コンポーネント仕様のモデル化 - フランス
- バイオメトリクスID認証ツールのアクセス管理セキュリティソフトウェア(TIS) - アメリカ
レポートはSECのWebサイトから無償でダウンロードできる。