Static analysis and family-based model checking of featured transition systems with VMC