Modellgetriebene Softwareentwicklung (MGSE) umfasst die traditionellen Gebiete des Sprachentwurfs, der Werkzeugentwicklung, und der Systemvalidierung in einem einheitlichen konzeptuellen und technischen Rahmen (Meta-Modellierung, deklarative Modell-Transformation, und modellbasierte Analyse). Diese Arbeit untersucht Entwurfsfälle für Methodologien und Werkzeuge im Rahmen der MGSE, wobei der Stand der Kunst durch die Anwendung formaler Techniken erhöht wird. Die Forschungsbeiträge dieser Arbeit umfassen (a) die Anwendung von Techniken der Meta-Modellierung auf industriell relevante Programmiersprachen; (b) die Formulierung einer methodischen Vorgehensweise zur Zertifizierung von Transformations - Algorithmen zur Entwurfszeit, (c) der Entwurf von Algorithmen zur effizienten Evaluierung von in der Object Constraint Language (OCL) formulierten Invarianten im Sekundär- und im Hauptspeicher und (d) diverse Beiträge zur Generierung von Integrierten Entwicklungsumgebungen (Integrated Development Environments, IDEs) aus Sprachspezifikationen für domänenspezifische Sprachen (Domain Specific Languages, DSLs). Ebenso wird ein Ausblick für zukünftige Forschungsarbeiten gegeben, und der Einfluss unserer Forschungsarbeiten auf industrielle Praxis diskutiert.