| Research Abstract |
本年度は,1.リアルタイムオペレーティングシステム(RTOS)の検証ツールの本格的な実装,および,2.RTOS上で動作する実時間ソフトウェアの検証ツールの実装を行った.1のRTOSの検証では,車載システム用のOSであるOSEK/VDXを対象としている.このツールでは,環境モデルと呼ぶOSの外側の挙動と期待する性質を記述し,それに基づいてモデル検査用記述を自動生成する.本年度行った予備実験により,工学的な観点から,環境モデルをシンプルに記述する必要があることが判明した.そこで,そのために必要なモデル構成要素を追加し,ツールの洗練を行った.これにより,現実的なRTOSの設計検証が行えるようになった.このように,モデル検査などの形式的な手法を現実的な問題に適用する際には,工学的な手法と組み合わせることが重要であり,本研究では,それが現実的なセッティングであると考えている.2に関しては,昨年度提案したパラメトリック分析手法を実現するツールの実装を行った.このツールでは,入力となるモデル化言語を定義し,提案した手法に基づいて自動的に分析を行う.また,この手法では,入力のモデルに基づいて到達可能な状態を探索するが,その到達可能な状態はモデルの重要な特徴を表現している.そこで,DOTとよばれるグラフを表現する記述を生成し,到達可能な状態を表示できるようにした
|
