モデル検査はソフトウェアの設計品質向上に有効な技術だが，モデル記述言語と時相論理を習得して検査モデルと制約条件を記述しなければならないことが，産業界への普及の妨げとなっている．そこで，状態遷移表と付加的な表から制約条件まで含む検査モデルを自動生成するモデル検査支援環境を作成し，複数の組込みソフトウェア開発プロジェクトへの適用によって評価した．Model Checking is effective to improve quality of software design. But, it requires knowledge of model description language and temporal logic to describe models and properties by hand, which make it difficult to be widely practiced in the industry. We developed Model Checking Support Environment to automatically generate models including properties to be checked, from State Transition Matrix and some additional tables. We also applied it to some embedded software development projects and evaluated.