| Research Abstract |
今年度は,1. シングルCPU上で動作するリアルタイムオペレーティングシステム(RTOS)の検証ツールのプロトタイプ作成,2. RTOS上で動作する実時間ソフトウェアのモデル化及びモデル検査手法の提案を行った.1のRTOSの検証では,車載システム用のOSであるOSEK/VDXを対象とした.OSは様々な使われ方をするため,それぞれの使われ方に関して検証する必要がある.そこで,昨年度,UMLにより整理して記述し,その記述からモデル検査のための記述を複数自動生成するアルゴリズムを提案した.今年度は,そのアルゴリズムに基づいて,モデル検査用の記述を自動生成するツールのプロトタイプを作成した.このツールでは,個々の使われ方毎に1つのモデル検査用記述を生成する.そのため,検査するバリエーションが多くなると,大量のモデル検査用記述が生成される.そこで,それらの記述を計算機クラスタにより検証を行う実験も行った.現在,実験結果の分析を行っている.2に関しては,実時間ソフトウェアの設計を対象としたパラメトリック分析手法を提案した.この手法では,動作の実行時間を変数として表現した設計モデルを対象として,デッドラインなどの実時間性を満たす変数に関する条件を求める.今年度は,そのアルゴリズムと停止性,健全性,完全性などの基本的な性質,および,ツールのプロトタイプを作成した.
|
