研究概要 |
マルチタスク実時間組込みソフトウェアの資源制約およびスケジューリング方式を考慮した実時間制約検証手法を考案した.考案した手法では,既存の組込みソフトウェアのモデリング言語であるUML MARTEの振る舞い仕様,振る舞いを構成する各単位動作が必要とする資源の割り当て情報,および,各資源のスケジューリング方式が与えられたとき,これらの仕様が表現する動きを正確に表現する優先権付き時間ペトリネット(以下,PrTPN)記述へ変換する。従来研究では待ち行列ネットワークなどの確率的なモデル化により実時間性に関する性能評価を行っていたが,提案手法は確定的な実時間モデルであるPrTPNを用いることにより,特に高信頼性を要求される組込みソフトウェアの設計において重要な,最悪時における実時間制約の保証を行うことができる.また,PrTPNを用いることにより,通常の時間ペトリネット(TPN)では表現できなかった固定優先度スケジューリングのモデル化を行うことができる.一方,従来優先権付き時間ペトリネットでは動的優先度スケジューリングの記述はできないとされてきたが,本研究では動的優先度スケジューリングの一つであるEDFスケジューリング方式の動作を離散的に近似することにより,PrTPNによるモデル化を可能とした.さらに本研究では,UML MARTEからPrTPNへの変換において,冗長ではあるが機械的な変換がしやすいように変換ルールを工夫した.また,変換したモデルを用いてスループットの検証を行うため,既存のPrTPN検証ツールを用いて,デッドロック検証問題へと帰着させた.提案手法は組込みソフトウェアなどの設計初期段階における最悪時の性能検証に有用であり,設計の手戻りを防ぎ効率化に寄与すると考えられる.
|