我々は、大規模で複雑な組込みネットワークシステ ムを対象として「信頼性向上」と「開発検証コストの圧 縮」の両方を実現するための形式手法に基づくテスト 環境の開発を目指している。提案するテスト環境では、 FMBT(Formal Model-based Testing) 技術による「仕 様の形式記述と分析」と「形式仕様からのテストケー ス自動生成」と CILS(Cluster in the Loop Simulation) 技術による「高速クラスタシミュレーション環境上で のテスト実行」を可能にする。本報告では、組込みネッ トワークシステムのテストの現状の問題、その問題を 解決するために我々が提案する FMBT と CILS による テスト環境の構想、FMBT における形式仕様に基づく テストケース自動生成に関する研究進捗、今後の研究 計画について述べる。