Variability modelling with feature models is one key technique for specifying the problem space of software product lines (SPLs). To allow for the automatic derivation of a concrete product based on a given variant configuration, a mapping between features in the problem space and their realisations in the solution space is required. Ensuring the correctness of all participating models of an SPL (i.e., feature models, mapping models, and solution-space models) is a crucial task to create correct products of an SPL. In this paper we discuss different possibilities for checking wellformedness of SPLs and relate them to their implementation in the FeatureMapper SPL tool. Categories and Subject Descriptors D.2.2 [Software Engineering]: Design Tools and Techniques—Computer-aided software engineering, Object-oriented design methods; D.2.2 [Software Engineering]: Software/Program Verification—Validation; D.2.13 [Software Engineering]: Reusable Software General Terms Design, Languages ...