2010 Fiscal Year Annual Research Report
高度な並行・並列組込みソフトウェアの検証法に関する研究
| Project/Area Number |
20680001
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
|
|---|
| Keywords | ソフトウェア工学 / ソフトウェア開発効率化・安定化 / ディペンダブル・コンピューティング |
|---|
| Research Abstract |
本年度は,1.リアルタイムオペレーティングシステム(RTOS)の検証ツールの本格的な実装,および,2.RTOS上で動作する実時間ソフトウェアの検証ツールの実装を行った.1のRTOSの検証では,車載システム用のOSであるOSEK/VDXを対象としている.このツールでは,環境モデルと呼ぶOSの外側の挙動と期待する性質を記述し,それに基づいてモデル検査用記述を自動生成する.本年度行った予備実験により,工学的な観点から,環境モデルをシンプルに記述する必要があることが判明した.そこで,そのために必要なモデル構成要素を追加し,ツールの洗練を行った.これにより,現実的なRTOSの設計検証が行えるようになった.このように,モデル検査などの形式的な手法を現実的な問題に適用する際には,工学的な手法と組み合わせることが重要であり,本研究では,それが現実的なセッティングであると考えている.2に関しては,昨年度提案したパラメトリック分析手法を実現するツールの実装を行った.このツールでは,入力となるモデル化言語を定義し,提案した手法に基づいて自動的に分析を行う.また,この手法では,入力のモデルに基づいて到達可能な状態を探索するが,その到達可能な状態はモデルの重要な特徴を表現している.そこで,DOTとよばれるグラフを表現する記述を生成し,到達可能な状態を表示できるようにした
|
Research Products
(8 results)
