Efficient validation of UML sequence diagrams against UML state machines via Kronecker algebra

Abstract

Diese Arbeit stellt einen Ansatz zur Validierung von UML-Sequenzdiagrammen gegenüber Zustandsautomaten unter Verwendung von Kronecker Algebra vor. Aufbauend auf früheren Arbeiten zur Konsistenzprüfung zwischen Sequenz- und Zustandsdiagrammen erweitern wir bestehende Techniken, um UML-spezifische Kontrollflussstrukturen wie alt-Blöcke und Schleifen zu unterstützen.Wir definieren formal, wie Sequenzdiagramme mithilfe von Kronecker Algebra zu endlichen Zustandsautomaten (Finite State Machines, FSMs) synthetisiert werden können, wobei besonderes Augenmerk auf die Nachrichtenreihenfolge und Abhängigkeiten unter Berücksichtigung von Alternativen und Schleifen gelegt wird.Die vorgeschlagenen Ansätze werden anhand praktischer Beispiele demonstriert. Im Rahmen dieser Arbeit wurde eine C++-Implementierung für Kronecker Algebra entwickelt, um diese Beispiele zu konstruieren und zu verifizieren. Darüber hinaus stellen wir Algorithmen vor, die für Kronecker Algebra Operationen optimiert sind und es der Implementierung ermöglichen, für unsere Anwendungsfälle bestehende Bibliotheken zur Matrixberechnung zu übertreffen.Unsere Ergebnisse zeigen, dass sich Kronecker Algebra zur Modellierung von Kontrollflussstrukturen in UML-Sequenzdiagrammen eignet und dass sogar Verzweigungsbedingungen in bestimmten Szenarien verifiziert werden können. Dadurch wird es möglich, unerreichbare Abschnitte in Sequenzdiagrammen sowie Inkonsistenzen zwischen Sequenz- und Zustandsdiagrammen zu identifizieren.

This thesis presents an approach to validate UML sequence diagrams against state machines using Kronecker Algebra. Building upon prior work in consistency checking between sequence and state machine diagrams, we extend the existing techniques to support UML-specific control flow structures such as alt-blocks and loops. We formally define how sequence diagrams can be synthesized into finite state machines (FSMs) through Kronecker Algebra, with special attention to message ordering and dependencies in the presence of alternatives and loops. The proposed techniques are demonstrated through practical examples. A C++ implementation of Kronecker Algebra was developed as part of this work to construct and verify these examples. In addition, we provide algorithms optimized for Kronecker Algebra operations, enabling the implementation to outperform existing matrix computation libraries.Our results show that Kronecker Algebra is suitable for modeling control flow structures in UML sequence diagrams and even branching conditions can be respected in certain settings. Enabling us to identify unreachable sections in sequence diagrams and inconsistencies between sequences and state machines.