ディペンダブル・システムのための形式手法の実践ポータル
文字サイズ
小
中
大
ホーム
サイトの主旨
形式手法の概要
トピックス
応用事例DB
導入方法
情報源
文献
手法・ツール
会議
公的プロジェクト情報
ホーム
>
応用事例DB
>
地域
>
EU
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"
このページの先頭へ戻る
地域
形式手法の分類
手法・ツール
適用分野