2011 Fiscal Year Annual Research Report
モデル検査技術を活用したソフトウェア設計方法に関する研究
| Project/Area Number |
21500036
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
岡野 浩三 大阪大学, 大学院・情報科学研究科, 准教授 (70252632)
|
|---|
| Keywords | 時間オートマトン / CEGAR LOOP / OCL |
|---|
| Research Abstract |
本研究では以下のことを行い、ソフトウェア設計へのフォーマルアプローチの適用可能性、有用性を調べる.
1.時間オートマトンのCEGARループの抽象化手法を例題に適用し,有用性を示す.
2.提案抽象化手法の並列実行アルゴリズムを提案し,有用性を示す.
3.既存ソフトウェアに対してJML記述を自動で付加する処理系を提案手法をもとに作成する.
4.UML/OCL記述からJMLI記述を自動導出する方法をもとに3.とあわせてソフトウェア開発支援システムのプロトタイプを作成する.
5.UML/OCL記述から時間オートマトンへ変換する方法と組み合わせ,それらをもとに総合的な設計開発法への展開をはかる.
本年はおおむね2.,3.,4.を行った.まず,2の時間オートマトンのCEGARループアルゴリズムの並列化による効率向上の研究を行い,並列計算機を用いる方法とボトルネックを見極め1つの計算機でも効率よく発見する方法を考案した.また並列化の論文化をし投稿できる状態にしている,また,ソフトウェア品質をモデル検査とテスト結果両面から評価する手法を考案し,国際会議で発表し論文化した.このテーマを発展させ品質メトリクスの提案まで持って行きたい.またOCLJML変換については相互変換をモデルベースで行う手法を提案し,発表した.またモデル検査技法を使い,表明生成のためのテストケ}ス生成に役立てるツールを実装した.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
時間オートマトンのCEGAR並列化の論文化が予定通りに進まなかったがソフトウェア工学への応用としてのメトリクスの可視化をはじめとしてソフトウェア工学への応用で進展が視られた.
|
| Strategy for Future Research Activity |
時間オートマトンのCEGAR並列化の論文化を至急取り組みたい.また,進展のあったテーマについて国際会議での発表をいくつか計画している.
|
Research Products
(16 results)
