| 研究概要 |
本研究では以下のことを行い、ソフトウェア設計へのフォーマルアプローチの適用可能性、有用性を調べる.
1. 時間オートマトンのCEGARループの抽象化手法を例題に適用し,有用性を示す.
2. 提案抽象化手法の並列実行アルゴリズムを提案し,有用性を示す.
3. 既存ソフトウェアに対してJML記述を自動で付加する処理系を提案手法をもとに作成する.
4. UML/OCL記述からJML記述を自動導出する方法をもとに3.とあわせてソフトウェア開発支援システムのプロトタイプを作成する.
5. UML/OCL記述から時間オートマトンへ変換する方法と組み合わせ,それらをもとに総合的な設計開発法への展開をはかる.
本年はおおむね 1.および3.,4.の一部を行った.まず,時間オートマトンのCEGARループアルゴリズムを論文にまとめ採録された.引き続き,並列化による効率向上の研究を行っていきたい.また,確率時間オートマトンに対するCEGARループアルゴリズムのプロトタイプを実装し,研究会で報告した.これについては,アルゴリズムの正当性を証明した上で,論文にまとめたい.また,確率オートマトンを用いたネットワーク性能解析検証法に関する手法を国際会議,および研究会にて発表した.
3.,4.についてはOCL記述からJML記述への自動変換手法の研究を国内のワークショップで発表し,またそれを整理したものを論文にまとめ採録された.これについては,引き続き,ツールの作成をして,有用性の評価を行っていきたい.
|
