ディペンダブル・システムのための形式手法の実践ポータル

Intertechnique - 航空機の燃料管理システム

ドメイン	航空運輸
開発対象	Airbus A380の燃料管理システム
国	フランス
開発組織	Intertechnique, Esterel Technologies
形式手法（言語、ツール）	SCADE
適用範囲・規模（形式手法）
適用対象のソフト種別	リアルタイム制御系
適用目的・工程	設計、自動コード生成
実装言語
実装規模
効果	開発工程の早い段階でシミュレーションによる検証を行うことができたため、機能の不具合が改善されたことにより、ハードウェアとの統合にかかる時間を60%程度削減することができた。

（出典: A. Jean-Louis Camus, Pierre Vincent, Olivier Graff, Sebastien Poussard, A verifiable architecture for multi-task, multi-rate synchronous software, 2008）

詳細情報

検証内容

サブシステム間のデータ交換が正しく行われることを検証した。

検証規模

期間

判断

形式手法を利用した動機

• 安全を保証した設計とその検証を早い段階で行い、組込みソフトウェアのコードを生成する必要があった。
• DO-178B標準の要求を満たす必要があった。

手法・ツール選択理由

• 以前のA340電子ロード管理システムの実装に成功し、その後2年間、Esterel Technologiesの協力を得て、SCADEの利用を社内標準とした。
• SCADEはDO-178B標準を満たすCコード生成機能を有している。
• SCADEは並列動作や機能の依存性の簡潔で明確な表現が可能である。

障害と工夫

SCADEは単一スレッドのコードを生成するように設計されているため、当初考案したモデル（図参照）に対応する正しいコードを生成することができなかった。そこで、自動コード生成可能な意味的に同一なモデルを作成した。

組織

体制

教育

その他

情報源

• Intertechnique :: Success Stories, Esterel Technologies, http://www.esterel-technologies.com/technology/success-stories/intertechnique
• A. Jean-Louis Camus, Pierre Vincent, Olivier Graff, Sebastien Poussard, A verifiable architecture for multi-task, multi-rate synchronous software, 2008

このページの先頭へ戻る