本発表では、組み込みシステムの要求仕様を分析するための、半形式的なドキュメント「説明基盤」の概念を新たに導入する。その上で、日本語の要求仕様から自然言語処理技術を介して説明基盤を求め、形式手法の技術を使って解析することにより、元の要求仕様の妥当性を検証する方法論、および、その機械的支援手法を提案する。今回は解析に仕様記述言語Alloyとその解析器Alloy Analyzerを援用し、専用のイディオムも併せて提案する。