| 研究概要 |
本研究では以下のことを行い、ソフトウェア設計へのフォーマルアプローチの適用可能性、有用性を調べる.
1.時間オートマトンのCEGARループの抽象化手法を例題に適用し,有用性を示す.
2.提案抽象化手法の並列実行アルゴリズムを提案し,有用性を示す.
3.既存ソフトウェアに対してJML記述を自動で付加する処理系を提案手法をもとに作成する.
4.UML/OCL記述からJMLI記述を自動導出する方法をもとに3.とあわせてソフトウェア開発支援システムのプロトタイプを作成する.
5.UML/OCL記述から時間オートマトンへ変換する方法と組み合わせ,それらをもとに総合的な設計開発法への展開をはかる.
本年はおおむね2.,3.,4.を行った.まず,2の時間オートマトンのCEGARループアルゴリズムの並列化による効率向上の研究を行い,並列計算機を用いる方法とボトルネックを見極め1つの計算機でも効率よく発見する方法を考案した.また並列化の論文化をし投稿できる状態にしている,また,ソフトウェア品質をモデル検査とテスト結果両面から評価する手法を考案し,国際会議で発表し論文化した.このテーマを発展させ品質メトリクスの提案まで持って行きたい.またOCLJML変換については相互変換をモデルベースで行う手法を提案し,発表した.またモデル検査技法を使い,表明生成のためのテストケ}ス生成に役立てるツールを実装した.
|
