Parametric timed systems are systems whose behavior depends on timing constrained by time parameters. These systems often operate in a safety critical environment, hence their provably correct behavior has to be guaranteed by the application of formal methods. This thesis summarizes the basics of model checking, one of the most successful formal approaches. Moreover, it presents the principles of the theory of timed, respectively parametric timed automata, which are formalisms that are suitable for modeling of such systems. Furthermore, a model based language framework is introduced, with a syntax that enables direct modeling of parametric timed behavior; together with a semantics based on a series of model transformations and mapping to a logical representation that allows the symbolic analysis of the model. The usability of the approach is demonstrated on two examples: the first one is a canonical example, Fischer's well known Mutual Exclusion Protocol, and the second one is an industrial case study, the connection handling of Prolan's SCAN protocol.