ソフトウェアシステムは,サービスを提供するアプリケーションとアプリケーションを実行する環境から構成される.これらソフトウェアシステムを構成する要素は,アプリケーションの発展や環境の移植などの要求に応じて変更される.このとき,アプリケーションや実行環境に競合などの問題が起きないことを保証するために,変更に際しては整合性を保つことが重要となる.しかし,人手による作業にも限界があるため,要求に応じた構成の変更と整合性の判定について計算機による支援が求められる.本稿ではこれらを体系的かつ形式的に行うため,構成要素の変更管理を目的としたフレームワークを提案し,Alloyを用いた形式化の方針を示す.本フレームワークはFODAのフィーチャモデルを基に,ソフトウェアシステムのアプリケーションと実行環境の構成要素,それらの対応関係に着目して抽象化したモデルを用いる手法である.また,構成を選択し変更する際の整合性を判定し,不整合が生じる場合には原因の特定と修正を適用する.