A Formal Model for Multi SPLs