Blick ins Buch

Automatic verification of behavior preservation at the transformation level for relational model transformation

Buch | Softcover

VIII, 112 Seiten

2017
Universitätsverlag Potsdam
9783869563916 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)

Titel ist leider vergriffen;
keine Neuauflage

Artikel merken

Die Korrektheit von Modelltransformationen ist von zentraler Wichtigkeit bei der Anwendung modellgetriebener Softwareentwicklung für die Entwicklung hochqualitativer Software. Insbesondere verhindert Verhaltensbewahrung als wichtigste Korrektheitseigenschaft die Entstehung semantischer Fehler während des modellgetriebenen Entwicklungsprozesses. Techniken zur Verifikation von Verhaltensbewahrung zeigen, dass bestimmte spezifische Eigenschaften bewahrt bleiben oder, im allgemeineren und komplexeren Fall, dass eine Form von Verhaltensäquivalenz oder Verhaltensverfeinerung zwischen Quell- und Zielmodell der Transformation besteht. Für beide Ansätze existieren automatisierte Werkzeuge für die Verifikation auf der Instanzebene, also zur Überprüfung konkreter Paare aus Quell- und Zielmodellen der Transformation. Allerdings existiert kein automatischer Verifikationsansatz, der auf der Transformationsebene arbeitet, also Aussagen zu allen Quell- und Zielmodellen einer Modelltransformation treffen kann.Dieser Bericht erweitert unsere Vorarbeit und Ergebnisse aus [27] und stellt einen neuen Ansatz zur automatischen Verifikation von Verhaltensbewahrung vor, der auf Bisimulation bzw. Simulation basiert. Dabei werden Modelltransformationen durch Triple-Graph-Grammatiken und Verhaltensdefinitionen mittels Graphtransformationsregeln beschrieben. Insbesondere weisen wir nach, dass das Problem der Verhaltensbewahrung durch Bisimulation auf Invariant-Checking für Graphtransformationssysteme reduziert werden kann und dass das entstehende Invariant-Checking-Problem für ein komplexes Beispiel durch unser Werkzeug zur Verifikation induktiver Invarianten gelöst werden kann. Das Beispiel beschreibt die Transformation von Sequenzdiagrammen in Systeme kommunizierender Automaten. Darüber hinaus diskutieren wir bestehende Einschränkungen von Invariant-Checking für Graphtransformationssysteme und Ansätze für zukünftige Arbeiten in diesem Bereich.

Erscheinungsdatum	27.04.2017
Reihe/Serie	Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam ; 112
Verlagsort	Potsdam
Sprache	englisch
Maße	210 x 297 mm
Einbandart	Paperback
Themenwelt	Mathematik / Informatik ► Informatik
Schlagworte	Abstraction • Behavior • behavioral abstraction • behavioral equivalenc • behavioral refinement • behavior preservation • bisimulation • Checking • constraints • equivalenc • Grammars • Graph • graph constraints • Graph-Constraints • Graphtransformationssysteme • graph transformation systems • Invariant • invariant checking • Invariant-Checking • Level • Model • Modelltransformationen • model transformation • Preservation • Refinement • Relational • relationale • relationale Modelltransformationen • relational model transformation • Semantics • semantics preservation • Simulation • Systems • Transformation • transformation level • Transformationsebene • Triple • triple graph grammars • Triple-Graph-Grammatiken • Verhaltensabstraktion • Verhaltensäquivalenz • Verhaltensbewahrung • Verhaltensverfeinerung
ISBN-13	9783869563916 / 9783869563916
Zustand	Neuware