The following technical report is available from http://aib.informatik.rwth-aachen.de: Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten Hans Grönniger AIB 2010-17 Eine Voraussetzung für den Erfolg einer modellbasierten Methode zur Softwareentwicklung ist eine variable und dennoch präzise Definition der verwendeten Modellierungssprachen. Hierzu gehört insbesondere auch die explizite Definition der Bedeutung der Sprachen -- ihrer Semantik. Formale Semantik leistet einen wichtigen Beitrag zur unmissverständlichen Kommunikation zwischen den Beteiligten und kann einen hohen Grad der Automatisierung über interoperable Werkzeuge ermöglichen. Diese Arbeit beschäftigt sich mit der vollständigen, formalen Definition objektbasierter Modellierungssprachen und legt den Fokus auf die flexible Definition problemadäquater Semantik. Zur Definition der Semantik objektbasierter Modellierungssprachen wird das Systemmodell als von allen Sprachen gemeinsam genutzte semantische Domäne definiert. Das Systemmodell charakterisiert abstrakt die Struktur, das Verhalten und die Interaktion von Objekten objektbasierter Systeme. Die prädikative semantische Abbildung von Elementen der Syntax einer Sprache in das Systemmodell definiert für ein Modell eine Menge von objektbasierten Systemen und erzeugt damit eine präzise Bedeutung auch für unvollständige bzw. unterspezifizierte Modelle. Die Semantik von Modellkomposition und -verfeinerung kann auf Basis des Systemmodells durch einfache mathematische Operationen erklärt werden. Gemäß einer allgemeinen Klassifikation der möglichen Variabilität einer Modellierungssprache können die verschiedenen Sprachbestandteile wie Syntax, semantische Domäne und semantische Abbildung mit Varianten ausgestattet werden. Dies ermöglicht die Anpassung einer Sprache zum Beispiel an einen projektspezifischen Kontext. Varianten und ihre Abhängigkeiten werden in Feature-Diagrammen dokumentiert. Eine Konfiguration, also die Auswahl von Sprachvarianten gemäß der Feature-Diagramme, legt dann die Menge der gültigen Definitionen fest. Die eingeführte Werkzeugunterstützung basiert auf MontiCore, einem Framework zur modularen Erstellung von textuellen Modellierungssprachen und dem Theorembeweiser Isabelle/HOL. Hierdurch wird eine flexible und gleichzeitig maschinenlesbare Syntax und Semantik gewonnen. Auch die Definition und Konfiguration von Semantikvarianten wird unterstützt. Die Definition der Semantik der UML-Teilmenge UML/P dient der Erprobung des werkzeugunterstützten Vorgehens. Betrachtet werden Klassendiagrammen, Objektdiagramme, Statecharts und Sequenzdiagramme. Zudem werden als Aktions- bzw. Constraint-Sprache vereinfachte Versionen von Java und OCL verwendet. Die angegebenen Semantikvarianten können direkt zur maschinenunterstützten Verifikation im Theorembeweiser verwendet werden, da sich zusätzlich auch konkrete Modelle automatisch in Isabelle übersetzen lassen. Die Verifikation wird an Beispielen unter Verwendung integrierter Semantiken verschiedener Modellierungssprachen der UML/P demonstriert. Dies zeigt die praktische Verwendbarkeit des Ansatzes.