プログラム中に表明を記述することで,プログラムの保守性,信頼性を高めることができる.そのため,表明の自動生成手法が注目されている.表明の自動生成手法の1つに動的生成手法がある.動的生成手法は比較的少ないコストで表明を生成できる.しかし表明の妥当性がテストケースに依存するという問題がある.そこで著者らは,表明の妥当性向上のためにインバリアントカバレッジとモデル検査の技術を用いたテストケース自動生成手法を提案している.本論文では,提案手法および評価実験について報告する.提案手法を実装したツールは対象Javaプログラムに対しテストケース依存問題を改善したテストケースを自動生成する.評価実験の結果,生成されたテストケースによる表明の妥当性向上を確認した.