This chapter introduces the algorithms and tools to support the design and verification activities of the model driven development process. It describes variability and design space exploration in the design of mixed-criticality systems, and explores the specification of the configuration files and how they are generated by the tools. The chapter provides details of the job-shifting algorithm to admit non-pre-emptive aperiodic tasks in flat and hierarchical scheduling models. Most exploration algorithms are based on generic optimization or constraint solving algorithms, often including custom algorithmic extensions and rarely use distinct search algorithms. Resolution and the associated tools generate the product realization. As with any other software engineering tool, a software product line must provide means to guarantee that any product is verified and validated. A set of software tools can only be applied efficiently if integrated into a tool chain that ensures the seamless flow of design data.