2010年6月7日
2010年7月～2013年6月（36ヶ月）
IBM Research(Haifa Lab.)、オックスフォード大学他。EU FP7からの予算。
IBM Research、EU、企業パートナーなどが共同で、電力グリッド、原子力発電所、水パイプライン等の大規模インフラシステムに関して、ソフトウェア更新時の信頼性確保のための技術開発を行う3年間の共同プロジェクトを開始する（実施期間：2010.7～2013.6）。形式手法に基づくテストとシミュレーションを組合わせて用いることにより、多数の運用条件の下でシステムが設計通りに動作することを検証することを目的とする。
機能要求に関わる不具合を70%程度低減することでシステムの信頼性を高めることを目標としている。
Eclipse上に、ソフトウェア更新の影響に関する静的解析、動的解析のためのツールを開発する。
ソフトウェアが設計通りに動作することを検証する技術は従来より存在するが、システムのアップグレードに特化した形式手法に基づく新しい技術を開発する。
適用する手法はプロジェクトのホームページからは不明であるが、システムが設計通りに動作することを証明するための形式手法を導入することが記載されていることからBメソッドであることが予想される。
ソフトウェア更新に関する新しい分野の検証ツールがEclipse上で開発されることが予定されているため、先行ツールとして欧州の関連システムでの利用が予想される。
自動検証技術を用いてソフトウェア更新の影響解析を行うことで、検証コストを低減する。システムライフサイクルコストの40%～70%を占めるソフトウェアの検証部分のコスト低減効果が期待できる。また、機能仕様の不具合の70%を低減による信頼性の向上を実現する。