2010 Fiscal Year Annual Research Report
モデル検査技術を活用したソフトウェア設計方法に関する研究
| Project/Area Number |
21500036
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
岡野 浩三 大阪大学, 大学院・情報科学研究科, 准教授 (70252632)
|
|---|
| Keywords | 時間オートマトン / CEGAR LOOP / OCL / JML |
|---|
| Research Abstract |
本研究では以下のことを行い、ソフトウェア設計へのフォーマルアプローチの適用可能性、有用性を調べる
1. 時間オートマトンのCEGARループの抽象化手法を例題に適用し,有用性を示す
2. 提案抽象化手法の並列実行アルゴリズムを提案し,有用性を示す
3. 既存ソフトウェアに対してJML記述を自動で付加する処理系を提案手法をもとに作成する
4. UML/OCL記述からJML記述を自動導出する方法をもとに3.とあわせてソフトウェア開発支援システムのプロトタイプを作成する
5. UML/OCL記述から時間オートマトンへ変換する方法と組み合わせ,それらをもとに総合的な設計開発法への展開をはかる
本年はおおむね2,,3.,4.を行った.まず,2の時間オートマトンのCEGARループアルゴリズムの並列化による効率向上の研究を行い,並列計算機を用いる方法とボトルネックを見極め1つの計算機でも効率よく発見する方法を考案し,国内研究会で発表した.また,1の発展課題として,確率時間オートマトンに対するモデル検査手法に関するアルゴリズムを考案し評価実験を行った結果を国際会議に発表した.3,,4.についてはOCL記述からJML記述への自動変換手法をeclipseプラグインとして実装し,実用例題を用いて評価した結果等を国内研究会で発表した.また,プログラムからのJMLの自動生成についてこれまでの研究成果をまとめ,論文に採録された
|
