形式仕様開発支援環境の研究

点击翻译按钮获取中文摘要

本年度は,これまでに提案したツールの発展として,証明譜に基づくテスト生成手法について,提案した(学会発表)。本研究では統合開発環境Eclipseを用いて,ソフトウェアの仕様を記述し,その仕様が望ましい性質を持つことを証明するための支援環境を開発・提案している。しかし,その仕様から実際のソフトウェア開発には距離がある。そこで,仕様記述,証明,ソフトウェア開発をEclipse上で一貫して行うことを目的とし,テスト駆動開発のためのテスト生成手法を提案した。テスト駆動開発とは,ソフトウェアが正しく動作することを確認するためのテスト群を先に開発し,そのテストをパスするようにソフトウェアの開発を進める手法であり,Eclipseはこの手法をサポートするツールとしても有名である。本研究において提案したテスト生成手法は,既に提案した手法で作成した証明を用いて,テスト群を自動で生成できる。この手法では,生成されたテストにパスしないソフトウェアが開発されると,証明済みの性質を満たさないことが保証される。このため,ソフトウェア開発を形式仕様に基づいて行うことができ,本研究の成果は科学的アプローチに基づく開発手法として,ソフトウェア開発の効率化・安定化につながると期待でぎる。本年度は,引き続き提案したツールの実装および改良を行った。より,実装を洗練するために多くの改良を行った。これによって証明譜のモデルが整理されたため,同種のソフトウェア開発が容易になると期待される。なお,本補助金による支援終了後も,引き続きツールの改良・保守を行っていく予定である。