Detailansicht

Supporting automated containment checking of software behavioural models

Muram Faiz Ul

Art der Arbeit

Dissertation

Universität

Universität Wien

Fakultät

Fakultät für Informatik

Studiumsbezeichnung bzw. Universitätlehrgang (ULG)

Dr.-Studium der technischen Wissenschaften (Dissertationsgebiet: Informatik)

Betreuer*in

Uwe Zdun

Volltext herunterladen
Volltext in Browser öffnen

DOI

10.25365/thesis.47558

URN

urn:nbn:at:at-ubw:1-28781.87360.592273-3

Link zu u:search

(Print-Exemplar eventuell in Bibliothek verfügbar)

Abstracts

Abstract

(Deutsch)

Während des Softwareentwicklungsprozesses ist es eine große Herausforderung, bereits in den frühen Phasen auf verschiedenen Abstraktionsebenen festzustellen, ob ein System von beabsichtigtem Verhalten abweicht und etwaige Abweichungen zu korrigieren. Werden Inkonsistenzen erst in späteren Phasen entdeckt, nachdem das System bereits implementiert oder getestet worden ist, führt dies zu enormem Aufwand für Korrektur, Überarbeitung und Verifikation. Es ist daher von großer Bedeutung, diese Inkonsistenzen bereits in einer frühen Phase des Softwareentwicklungsprozesses zu erkennen und zu beheben. Dies gilt vor allem, sobald verfeinerte Modelle von ihren abstrakten Gegenstücken abweichen. Diese Dissertation konzentriert sich auf eine spezielle Art von vertikaler Konsistenz, insbesondere Containment Checking. Dabei wird überprüft, ob das vom Low-Level-Modell beschriebene Verhalten auch das im High-Level Gegenstück beschriebene erfasst. Die Containment-Beziehung von Verhaltensmodellen wurde in bereits existierenden Forschungsarbeiten bisher nicht untersucht. Nach einer systematischen Überprüfung der vorhandenen Forschung zur Konsistenzprüfung von Software-Verhaltensmodellen konnten wir eine Reihe an Lücken und offenen Problemen ermitteln, die als Basis für diese Dissertation dienen. Der hauptsächliche Beitrag dieser Dissertation besteht aus neuen Konzepten und Techniken zum automatischen Containment Checking von Software-Verhaltensmodellen. Mittels Modelltransformationen und Modellprüfung (Model Checking) wird Containment Checking von Software-Verhaltensmodellen, insbesondere Activity Models, Sequence Models und Service Choreography unterstützt. Genauer gesagt wird eine automatische Transformation von Verhaltensmodellen in formale Spezifikationen und Konsistenzbeschränkungen durchgeführt. Diese werden beim Model Checking für das Erkennen von Abweichungen zwischen den Eingabemodellen und daraus folgende Gegenbeispiele benötigt. Das Feedback von Model Checkern ist jedoch für Benutzer mit eingeschränktem Wissen über die zugrundeliegenden formalen Methoden zur Analyse von beziehungsweise dem Verständnis für Konsistenzverstöße meist wenig hilfreich. Wir schlagen daher einen Ansatz vor, der die Analyse von Gegenbeispielen verwendet, um den Grund von Konsistenzverstößen zu finden und den jeweiligen Akteuren passende Lösungsvorschläge zu präsentieren. Endlosschleifen und parallel ausgeführte Programmteile stellen Techniken, die auf Model Checking basieren, vor große Herausforderungen. Wir haben daher zusätzlich einen Ansatz entwickelt, der basierend auf Graphen fehlende Knoten, fehlende transitive Verbindungen und fehlende Abläufe überprüft. Zunächst wurde Containment Checking allgemein nach benannten Designmodellen untersucht und die Anwendung in realistischen Use-Case-Szenarien geprüft, wobei letztere überwiegend aus Enterprise Informationssystemen entnommen wurden. Als einen zweiten Anwendungsbereich untersuchten wir die Anwendung von Containment Checking im Kontext von Architekturmustern. Diese legen verschiedene Arten von Designbedingungen für den Detailentwurf und für die Implementierung fest, die nicht verletzt werden dürfen. Wir untersuchten außerdem die Anwendung von Containment Checking für das Prüfen von Designbedingungen bei drei beliebten Architekturmustern: Model-View-Controller, Layers und Pipe and Filter, sowie deren Varianten. Die quantitative Evaluierung der realistischen Anwendungsszenarien zeigt, dass die vorgeschlagenen Ansätze in typischen Arbeitsumgebungen für Softwareentwickler ziemlich gut funktionieren und gut genug für übliche Größen von Softwaredesign-Modellen skalieren.

Abstract

(Englisch)

A major challenge in software development processes is to detect and fix the deviations of system's intended behaviours at different abstraction levels in early phases. Inconsistencies that are detected at later phases, when the system is already implemented or tested, require huge amounts of time and effort for correction, revision, and verification. Therefore, it is crucial to detect and fix the inconsistencies at early phases of software development, and especially as soon as refined models deviate from their abstract counterparts. This dissertation focuses on a special type of vertical consistency, in particularly containment checking that verifies whether the behaviour described by the low-level model encompasses those specified in the high-level counterpart. Previous research has not investigated the containment relationship for behavioural models. We have performed a systematic review of software behavioural model consistency checking research, and identified a number of gaps and open problems that serve as a foundation for this dissertation. The major contributions of this dissertation are novel concepts and techniques for automatic containment checking of software behaviour models. Containment checking of software behaviour models, in particularly activity models, sequence models and service choreographies, is supported using model transformations and model checking. Specifically, the automated transformation of behaviour models into formal specifications and consistency constraints is performed; they are required by model checkers for detecting any discrepancies between the input models and yielding corresponding counterexamples. However, the feedback of model checkers is rather not helpful for users with limited background on the underlying formal methods to analyse and understand the causes of consistency violations. A counterexample analysis approach is therefore proposed for locating the cause(s) of containment violations and presenting appropriate suggestions to stakeholders for their resolution. Dealing with unconditional loops and parallel execution branches are challenging issues in model checking based techniques. Therefore, we introduced, in addition to the model checking based techniques, a lightweight graph-based approach that verifies missing nodes, missing transitive links, and missing cycles. We have investigated containment checking first generically for the named design models and studied the application in realistic use case scenarios, taken mainly from enterprise information systems. As a second application domain, we have studied applying containment checking in the context of architectural patterns: Architectural patterns impose various kinds of design constraints on the detailed designs and implementations that should not be violated. We studied the application of containment checking for checking those design constraints for three popular architectural patterns: Model-View-Controller, Layers, and Pipe and Filter, as well as their variants. The quantitative evaluation of the realistic use case scenarios shows that the proposed approaches perform reasonably well in typical working environments of software developers and scale well enough for typical sizes of software design models.

Autor*innen

Muram Faiz Ul

Haupttitel (Englisch)

Supporting automated containment checking of software behavioural models

Publikationsjahr

2017

Umfangsangabe

xii, 226 Seiten : Illustrationen

Sprache

Englisch

Beurteiler*in

Uwe Zdun

Klassifikation

54 Informatik > 54.52 Software engineering

AC Nummer

AC14550501

Utheses ID

42092

Studienkennzahl

UA | 786 | 880 | |

Detailansicht

Abstracts

Schlagwörter