研究課題
本研究では以下のことを行い、ソフトウェア設計へのフォーマルアプローチの適用可能性、有用性を調べる．1.時間オートマトンのCEGARループの抽象化手法を例題に適用し，有用性を示す．2.提案抽象化手法の並列実行アルゴリズムを提案し，有用性を示す．3.既存ソフトウェアに対してJML記述を自動で付加する処理系を提案手法をもとに作成する.4.UML/OCL記述からJML記述を自動導出する方法をもとに 3.とあわせてソフトウェア開発支援システムのプロトタイプを作成する．5.UML/OCL記述から時間オートマトンへ変換する方法と組み合わせ，それらをもとに総合的な設計開発法への展開をはかる．本年はおおむね4.を行った．OCLJML変換については相互変換をモデルベースで行う手法nituについて効率化を目指した改善をいくつか行い，国際会議等にて発表した．またモデル検査技法を使い，表明生成のためのテストケース生成に役立てるツールについて発表・投稿を行った．
2: おおむね順調に進展している
あとは時間オートマトンを用いた設計総合開発システムへの展開であり概ね1年でできると考える．
時間オートマトンのモデル検査の研究を進め，またＯＣＬ／ＪＭＬ双方向変換を活用したシステムの有効性評価を進めてきたい．
すべて 2013 2012
すべて 雑誌論文 (3件) (うち査読あり 3件) 学会発表 (10件)
International Journal of Informatics Society (IJIS)
巻: vol.4, No.3 ページ: to appear
巻: vol.5, No.1 ページ: to appear
