ソフトウェアのデザインを確認する方法としてモデル検査検証技術が有効である．実用的な対象では，通常処理に加えて多くの例外事象がある．場合分けが増え，対象の仕様記述だけではなく検証性質の表現も複雑になる．また，状態空間が大きくなり実行効率にも影響する．本稿では，多値遷移システムに基づくモデル検査技法を用いて，系統的に複雑さを軽減する方法を報告する．EJBコンポーネントフレームワークの振舞い解析を対象とし定量的な観点を含めて議論する．