可変性を持つシステムはソフトウェア開発において多くの分野で存在する。特にソフトウェアプロダクトライン（以下SPL）開発では、類似する製品群の共通性と可変性を分析し、それに基づいて体系的な再利用開発を行うものである。可変性を持つシステムは潜在的に多くの製品構成を持つが、その数は可変性に対して指数関数的に増えるためその検証は困難である。本研究では特にモデル検査技術に注目し、可変性を持つシステムの検証手法について検討する。
可変性を持つシステムを効率的にモデル検査を行うためのモデル化手法が研究されている。その一つにfeatured transition systems（FTS）がある。本研究では、可能性を持つシステムに対して、FTSを拡張し確率を考慮したモデル検査手法を提案する。