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

Altreonic - 分散RTOS (OpenComRTOS)

ドメイン	電子部品・デバイス
開発対象	組込み機器用リアルタイムOS
国	ベルギー
開発組織	Altreonic
形式手法（言語、ツール）	TLA+/TLC
適用範囲・規模（形式手法）	一部分のみに適用
適用対象のソフト種別	リアルタイム制御系
適用目的・工程	アーキテクチャ設計
実装言語
実装規模
効果	RTOSの性質である安全性とリアルタイム性を実現できた コードサイズが従来と比較して１/10程度になった

（出典:Altreonic社Webサイト ）

詳細情報

検証内容

• 形式モデルに対し、形式モデルエンジニアとソフトウェアエンジニアがミーティングを行い、より詳細なモデルを作成していった。また、モデルが正しいかどうかのチェックを行った。
• モデルが十分実装に近くなったら、PC上の仮想的なターゲット上でシミュレーションモデルを構築した。
• 次にこのコードを実際の16ビットのマイクロプロセッサに移行し、最適化した。

検証規模

期間

判断

形式手法を利用した動機

RTOSは高い安全性と信頼性を要求されるにも関わらず、２００４年時点では、ほとんどのRTOSが検証されていなかった。信頼性の高いRTOSを構築するために形式手法の適用を決めた。

手法・ツール選択理由

C言語に近いSPIN等よりも、より抽象的なタームの重要性を理解することができる。

障害と工夫

• 完全な証明のためにはターゲットとなるハードウェアもモデル化して検証する必要があるが、それは複雑であり状態爆発を起こすため、実施しなかった。
• TLAモデルはパラメータ化ができないため、特定の部分だけをモデル化した。

組織

体制

初期のアーキテクチャを定義した後、2チーム作成し、１チームはアーキテクチャモデルを作成し、もう１チームは、TLA+/TLCを利用して初期の形式モデルを作成した。

教育

その他

情報源

"Bernhard H.C. Sputh, et.al, OpenComRTOS: Reliable performance with a small code sizse Eric Verhulst， Gjalt de Jong, OpenComRTOS - Distributed RTOS development using formal modeling methods"

このページの先頭へ戻る