Consistency-by-Construction Techniques for Software Models and Model Transformations
A model is consistent with given specifications (specs) if and only if all the specifications are held on the model, i.e., all the specs are true (correct) for the model. Constructing consistent models (e.g., programs or artifacts) is vital during software development, especially in Model-Driven...
Main Author: | |
---|---|
Contributors: | |
Format: | Doctoral Thesis |
Language: | English |
Published: |
Philipps-Universität Marburg
2020
|
Subjects: | |
Online Access: | PDF Full Text |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Ein Softwaremodell ist mit gegebenen Spezifikationen (Specs) genau dann konsistent, wenn alle Spezifikationen von dem Softwaremodell eingehalten werden, d.h. alle Spezifikationen für das Softwaremodell wahr (korrekt) sind. Während der Softwareentwicklung ist die Konstruktion von konsistenten Softwaremodellen (z.B. Programmen oder Artefakten) essentiell. Dies gilt besonders im Bereich des Model-Driven Engineering (MDE), in welchem die Softwaremodelle in allen Phasen des Softwareentwicklungsprozesses (Analyse, Design, Implementierung und Test) verwendet werden. Softwaremodelle werden üblicherweise in domänenspezifischen Modellierungssprachen (DSMLs) verfasst und dienen der Beschreibung eines Domänenproblems oder eines Systems aus unterschiedlichen Perspektiven und auf unterschiedlichen Abstraktionsebenen. Wenn das Softwaremodell mit der Definition seiner DSML (gewöhnlich durch ein Meta-Modell und Integritätsbedingungen definiert) konform ist, gilt das Softwaremodell als konsistent. Modelltransformationen sind eine essentielle Technologie zur (semi)-automatisierten Manipulation von Softwaremodellen, inkl. z.B. des Refactorings und der Codegenerierung. Dabei wird oftmals ein wohldefiniertes Transformationsverhalten vorausgesetzt in dem Sinne, dass die resultierenden Softwaremodelle in Hinblick auf die Bedingungen konsistent sind. Inkonsistente Softwaremodelle beeinflussen die Anwendbarkeit von Modelltransformationen, wodurch die automatische Ausführung unzuverlässig und fehleranfällig werden kann. Die Konsistenz von Softwaremodellen und den Ergebnissen von Modelltransformationen trägt zur Qualität des gesamten modellierten Systems bei. Obwohl MDE bemerkenswerte Fortschritte gemacht hat und ein akzeptiertes Verfahren in vielen Anwendungsbereichen wie der Automobilindustrie sowie der Luft- und Raumfahrt darstellt, so gilt es immer noch deutliche Herausforderungen zu bewältigen, um die MDE-Vision in der Industrie umzusetzen. Die Herausforderungen bestehen dabei in dem Umgang und der Auflösung von Inkonsistenzen in Softwaremodellen (z.B. unvollständigen Softwaremodellen), der Sicherstellung und Erhaltung von Modellkonsistenz und Korrektheit während der Modellkonstruktion, der Erhöhung der Zuverlässigkeit von Modelltransformationen (z.B. durch die Sicherstellung der Modellkonsistenz nach Modelltransformationen), der Entwicklung von effizienten (automatisierten, standardisierten und zuverlässigen) domänenspezifischen Modellierungswerkzeugen und dem Umgang mit großen Softwaremodellen, was insgesamt die Notwendigkeit weiterer Forschung zeigt. In dieser Arbeit werden vier automatisierte und interaktive Techniken zur Sicherstellung der Konsistenz von Softwaremodellen und Modelltransformationsergebnissen innerhalb des Softwareentwicklungsprozesses vorgestellt. Die ersten beiden Beiträge erlauben die Konstruktion von konsistenten Softwaremodellen einer gegebenen DSML in einer automatisierten und interaktiven Weise. Die Konstruktion kann dabei mit einem potentiell inkonsistenten Softwaremodell beginnen. Da die Erweiterung von Transformationen zur Erfüllung von Bedingungen eine langwierige und fehleranfällige Aufgabe darstellt, welche hohe Fähigkeiten in Bezug auf die theoretischen Grundlagen voraussetzt, ergeben sich die weiteren Beiträge: Die vorgestellten Techniken stellen die Modellkonsistenz nach einer automatischen Erweiterung der Modelltransformation durch zusätzliche Anwendungsbedingungen (engl. Application Conditions - ACs) sicher. Diese resultierenden Anwendungsbedingungen steuern die Anwendbarkeit der Transformationen in Bezug auf eine Menge von Konsistenzbedingungen. Darüber hinaus werden zusätzlich Optimierungsstrategien bereitgestellt. Im Einzelnen wird folgendes präsentiert: Als Erstes wird eine automatische und interaktive Technik zur Reparatur von Softwaremodellen präsentiert. Dieser Ansatz leitet Modellierer beim Reparieren des gesamten Modells, indem alle Kardinalitätsverletzungen aufgelöst werden, und führt somit zu dem gewünschten konsistenten Softwaremodell. Zweitens wird eine Technik zur effizienten Generierung von großen, konsistenten und heterogenen Softwaremodellen eingeführt. Beide Techniken sind DSML-unabhängig, d.h. sie können für beliebige Meta-Modelle eingesetzt werden. Es werden Meta-Techniken für die Anwendung beider Ansätze auf einer gegebenen DSML präsentiert, da mittels Meta-Tools entsprechende DSML-Werkzeuge (Modellreparatur und Modellgeneration) auf Basis eines gegebenen Meta-Modells automatisch generierbar sind. Es wird die Korrektheit dieser Techniken sowie die Auswertung und Diskussion der Eigenschaften (z.B. Skalierbarkeit) gezeigt. Drittens ist ein Werkzeug entwickelt worden, basierend auf einem konstruktiven Ansatz zur Übersetzung von OCL Bedingungen in semantisch äquivalente Graphbedingungen, welches diese als gewährleistende Anwendungsbedingungen vollautomatisch in Transformationsregeln integriert. Eine bedingungsgewährleistende Anwendungsbedingung stellt sicher, dass eine Transformationsregel nur genau dann auf einem beliebigen Softwaremodell ausgeführt werden kann, wenn das resultierende Softwaremodell nach der Regelanwendung die Bedingung erfüllt. Viertens wurde ein konstruktiver Ansatz zur Optimierung von Anwendungsbedingungen für bedingungserhaltende Transformationsregeln entwickelt. Eine bedingungserhaltende Anwendungsbedingung stellt sicher, dass eine Regel erfolgreich auf ein konsistentes Softwaremodell, welches die Bedingung erfüllt, angewandt werden kann, genau dann, wenn das resultierende Softwaremodell nach der Regelanwendung immer noch konsistent mit der Bedingung ist. Es wird die Korrektheit der Techniken, die Einsatzfertigkeit der Werkzeuge, die Evaluation der Effizienz (Komplexität und Leistungsfähigkeit) beider Ansätze sowie die Bewertung des gesamten Ansatzes gezeigt. Die vier Techniken sind kompatibel zu dem Eclipse Modeling Framework (EMF), welches die Realisierung der OMG-Standard-Spezifikation in der Praxis darstellt. Daher sind die Interoperabilität und die Austauschbarkeit der Techniken sichergestellt. Die vorgestellten Techniken verbessern nicht nur die Qualität des modellierten Systems, sondern erhöhen auch die Produktivität durch die Bereitstellung von Meta-Tools zur Generierung von DSML-Werkzeugen, welche die Aufgabenbearbeitung durch Automatisierung beschleunigen.