| Research Abstract |
本年度は,昨年度までに提案した手法とツールを,現実的なシステムに適用し,評価を行った.適用対象はリアルタイムオペレーティングシステム(RTOS)である.主に,1.モデル検査のための環境生成ツール,2.モデル検査に基づいたテストケース生成ツールの適用を行った,1のツールは,RTOSの設計の正しさを検証するためのものであり,2のツールは,RTOSの実装をチェックするために,1で検証済みの設計モデルからテストケースを生成するものである.1に関しては,本研究で提案した環境モデルを作成し,ツールを用いてモデル検査用のスクリプトを自動生成した.環境モデルは,複数の側面から検証要件のモデル化を行い,アスペクト指向の考え方を用いて,それらを整理した.また,検証結果が膨大になったため,関係データベースに検証データを格納し,SQLでクエリを発行することにより,その分析を行った,その結果,効果的,かつ,効果的に設計検証を行うことができた.2に関しては,1を適用した設計モデルから,モデル検査のアルゴリズムに基づいて,網羅的にテストケースを生成した.生成したテストケースは75万弱である。さらに,これらのテストケースから,テスト用のアプリケーションを自動生成し,RTOSの実装のテストも行った.テストケースの数が膨大なため,テストに3ヶ月を要したが,すべてについて実行することができた.これらのことから,本研究で提案した手法とツールは,現実問題に適用できることがわかった.モデル検査に基づいた手法を,このように大規模に適用した事例は見たことが無く,非常に大きな成果が得られたと考えている.
|
