組み込みシステムの開発において、Simulinkモデルのカバレッジテストが重要である。
しかしモデルが大規模や非線形になると、条件を満たす入力信号を手動生成することは難しい。
そこで本研究では、Simulinkのテストケースを自動生成することを目的とする。
手法として、SMTソルバによる静的解析を提案する。
まず、モデルの単位時間ごとの振る舞いやカバレッジ条件を制約として記述する。
また、求解の効率化のために、振る舞いを限定するパス制約を記述することも検討する。
次に、上記の制約充足問題をSMTソルバーで解くことにより、テストケースを得る。
提案手法で、中規模モデルで高カバレッジが達成できることを確認した。