ホーム > 応用事例DB > 適用分野 > 航空運輸

航空運輸

National Air Traffic Services (NATS) Praxis - iFACTS、航空管制システム

ドメイン
    航空運輸
開発対象
    航空管制システムの拡張機能。iFACTS (Interim Future Area Control Tools Support)は、NATSに従来からある航空管制システムNERC (New En-Route Centre)の拡張であり、管制官を支援するツールを提供する。
国
    イギリス
開発組織
    Praxis
形式手法（言語、ツール）
    Z (Microsoft Word Add-ins, Fuzz: 型チェッカー)
適用範囲・規模（形式手法）
  • 機能仕様記述
  • ATSシステムソフトウェアの開発
  • 既存のNERCシステムに付加し、仕様記述と実装 4250ページ
適用対象のソフト種別
    エンタプライズ系
適用目的・工程
    仕様記述、コーディング、テスト、検証
実装言語
    SPARK Ada
実装規模
    150,000SLOC (Ada SPARK)
効果
    [バグ排除]
  • ソフトウェアに重大な欠陥は発見されず、ソフトウェア品質に問題がないことが確認された。
    • [形式手法の経験]
  • Zを用いたモデリングを経験：　テスト実施者やレビュー実施者はテスト・ケース作成やコード・設計のレビューを効率的に行える　 ようになった。
  • 各工程間のコミュニケーション促進・曖昧さを解消に役立った。 （設計者、プログラマ、テスト実施者・コードレビュー実施者、保守作業における人的要素を過小評価しないこと）
    • [規格、認証準拠]
  • IEC61508、SIL4対応に対応できた。

詳細情報

検証内容

検証規模

期間

判断

形式手法を利用した動機

    英国政府は、空港の年間フライト数の急増に備えて、信頼性の高い航空管制システムを導入する必要があった。

手法・ツール選択理由

障害と工夫

    Zの記述にはWordを用いた。言語とツールと同時に新しいことを教えるのは困難という判断があった。ZのフォントとFuZZタイプチェカーの起動ボタン、仕様と構造の対応を確認するGUIツールへのリンクなどを備える。

組織

体制

教育

    [Zの読み]
  • 3日間のコースを実施。1週間の業務ですらすらと読めるようになった。 75名をトレーニングした。
    • [Zの書き]
  • 3日間のコースを実施。3ヶ月の業務ですらすらと書けるようになった。 11名をトレーニングした。
    • [SPARK]
  • 57名をトレーニングした。

その他

情報源

  • Open-DO, The Use of Formal Methods on the iFACTS ATC Project (Neil White), http://www.open-do.org/2010/04/20/the-use-of-formal-methods-on-the-ifacts-air-traffic-control-project/

カテゴリ

, , ,

このページの先頭へ戻る