Formalizing interactive staged feature model configuration