EU

Altreonic - 分散RTOS (OpenComRTOS)

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

(出典:Altreonic社Webサイト )


詳細情報

検証内容

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

検証規模

期間

判断

形式手法を利用した動機

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

手法・ツール選択理由

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

障害と工夫

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

組織

体制

    初期のアーキテクチャを定義した後、2チーム作成し、1チームはアーキテクチャモデルを作成し、もう1チームは、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"

このページの先頭へ戻る