Logica Nederland B.V. - オランダ運河のマエスラント防潮可動橋（水門） - 応用事例DB

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ウェブサイト）

詳細情報

検証内容

コアアーキテクチャにおいてライブロック及びデッドロックが存在しないこと

仕様の妥当性を検証した
Ward & Mellor手法に基づいてモデル化を行った
各プロセス、store、flowにおける機能やデータをモデル化した

検証規模

期間

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

判断

形式手法を利用した動機

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

手法・ツール選択理由

障害と工夫

組織

体制

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

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

このページの先頭へ戻る