| 研究概要 |
前年度までに,ソフトウェア仕様記述モデルUML-MARTEシーケンス図で記述されたマルチタスク実時間組込みソフトウェアの動作仕様,および各タスクへのリソース割り当ておよびスケジューリング方式が与えられたとき,その時間的な動作を表現する検証モデル,優先権付き時間ペトリネットに変換し,実時間制約検証を行う手法を提案した.本年度はこの手法に対して,次のような問題点の修正および拡張を行った.まず,タスク動作仕様記述モデルとして当初採用していたUML-MARTEシーケンス図について、その動作意味が正確に与えられていないために検証モデルへの変換の正しさが証明できなかったため,古くから慣用的に用いられ,より動作意味が明確である,タスクグラフモデルで動作仕様を記述するように変更した.次に,従来研究では現実のシステムでよく用いられるタスクのプリエンプションに対応していなかったため,検証モデルを時間の計測を任意に停止・再開できるストップウォッチを持つモデルである,優先権付きストップウォッチペトリネットに拡張し,プリエンプティブ固定優先度スケジューリングの動作を検証モデルに変換する手法を考案した.さらに,仕様モデルからの自動変換を容易にし,検証モデルにおけるエラーに対応する元の仕様の誤りをトレースしやすくするため,仕様モデルを構成するタスク・リソース・スケジューラ等の構成要素毎に検証モデルに変換し,それらを機械的に結合することにより全体の検証モデルを構成する手法に改良した.これらの成果は査読付きの国内会議「組込みシステムシンポジウム2010」に採択され,論文集に掲載されている.提案手法を用いることにより,マルチタスク実時間ソフトウェアに対してどの程度のリソースを割り当てれば実時間制約を満たすか,あるいは、どの程度の性能が達成されるか,といった検証を,設計初期段階の設計モデルの段階で行うことが可能となる.また,リソース数やスケジューリング方式の変更および再検証も容易であるため,設計者によるアーキテクチャ検討の手段としても有用であると考えられる.
|
