Paramètres
En savoir plus sur le livre
Die Korrektheit von Modelltransformationen ist entscheidend für die modellgetriebene Softwareentwicklung, insbesondere zur Vermeidung semantischer Fehler durch Verhaltensbewahrung. Diese Eigenschaft gewährleistet, dass spezifische Merkmale während des Entwicklungsprozesses erhalten bleiben. Verifikationstechniken zeigen, dass entweder bestimmte Eigenschaften bewahrt werden oder eine Form von Verhaltensäquivalenz zwischen Quell- und Zielmodellen besteht. Automatisierte Werkzeuge existieren für die Verifikation auf der Instanzebene, um konkrete Modellpaare zu überprüfen. Ein automatisierter Ansatz für die Transformationsebene, der Aussagen zu allen Quell- und Zielmodellen treffen kann, fehlt jedoch. Dieser Bericht erweitert frühere Arbeiten und präsentiert einen neuen Ansatz zur automatischen Verifikation von Verhaltensbewahrung, der auf Bisimulation und Simulation basiert. Modelltransformationen werden durch Triple-Graph-Grammatiken und Verhaltensdefinitionen mittels Graphtransformationsregeln beschrieben. Wir zeigen, dass das Verhaltensbewahrungsproblem durch Bisimulation auf Invariant-Checking für Graphtransformationssysteme reduziert werden kann. Zudem wird demonstriert, dass unser Werkzeug zur Verifikation induktiver Invarianten das Invariant-Checking-Problem für ein komplexes Beispiel, die Transformation von Sequenzdiagrammen in Systeme kommunizierender Automaten, lösen kann. Abschließend werden Einschränkungen von Invaria
Achat du livre
Automatic verification of behavior preservation at the transformation level for relational model transformation, Johannes Dyck
- Langue
- Année de publication
- 2017
Modes de paiement
Personne n'a encore évalué .