EU

Logica Nederland B.V. - オランダ運河のマエスラント防潮可動橋(水門)

ドメイン
    その他(水門)
開発対象
    水門開閉の意思決定システム
    オランダ
開発組織
    Logica Nederland B.V. (旧CMC Den Haag B.V.) - Rijkswaterstaat (Dutch Ministry of Transport, Public Works and Water managementの一部門) の委託を受けて開発
形式手法(言語、ツール)
    Z (ZTC type checking tool)、SPIN、PVS
適用範囲・規模(形式手法)
    コアとなる部分のみ。Zの仕様記述 - 29プログラム/20KLOC
適用対象のソフト種別
    制御系
適用目的・工程
    アーキテクチャ設計(SPIN)、詳細設計(Z)
実装言語
    C++
実装規模
    Cの運用システム - 250KLOC
効果
  • 費用対効果の面で有利であった。
  • モデル検査により、プロトコルレベルで大きな変更を実施する必要性が判明した
  • Zの仕様記述により、テストケース作成やコード/設計レビューを有効に行うことができた。また、設計者、プログラマ、テスタ、コードレビュー者間の意思疎通を曖昧さを排除して行うことができた

(出典: Rijkswaterstaatウェブサイト)


詳細情報

検証内容

    [Promela/SPINによる検証]
  • コアアーキテクチャにおいてライブロック及びデッドロックが存在しないこと
  • [Zによる検証]
  • 仕様の妥当性を検証した
  • Ward & Mellor手法に基づいてモデル化を行った
  • 各プロセス、store、flowにおける機能やデータをモデル化した

検証規模

期間

    1期: 1995-1996年、2期: 2007-2009年

判断

形式手法を利用した動機

    IEC 61508ではsafety-criticalシステムの開発には形式手法の利用を推奨しており、本プロジェクトではIEC 61508の遵守を決定した

手法・ツール選択理由

障害と工夫

組織

体制

    [1期の開発]
  • 3名の形式手法の専門家の支援を受け、5名が中心となって開発を行った
  • 7名が主にコーディングを行った
  • [2期の開発]
  • 7名が開発を行った

教育

  • Promela/SPINによるモデリングは習得が容易であった
  • Zによるモデリングは難しく、習得に時間がかかった

その他

情報源

  • Ken Madlener, et al., A Formal Verification Study on the Rotterdam Storm Surge Barrier, ICFEM 2010
  • Klaas Wijbrans, et al., Software Engineering with Formal Methods: The storm surge barrier revisited, ACISION, 2008
  • 形式手法適用調査 調査報告書、情報処理推進機構、2010

このページの先頭へ戻る