TY - THES A1 - Peixoto Soares, Joao Pedro T1 - Werkzeugunterstütze Erreichbarkeitsanalyse von UML Diagrammen N2 - Da die Erfüllung bestimmter Modelleigenschaften und formeller Anforderungen entscheidend für den Erfolg von Softwareprojekten ist, führt dies zu einer klaren Motivation für die Entwicklung eines Werkzeuges, welche die Prüfung von Modelleigenschaften rationalisiert und beschleunigt. Diese Arbeit widmet sich dem Design und der Implementierung eines Plugins für Visual Paradigm, das die automatisierte formale Prüfung von der Erreichbarkeit der Zustände eines UML-Zustandsdiagramms ermöglicht. Das Plugin setzt sich aus dem Auslesen der Diagrammelemente, deren Übersetzung in das SMTLIB-Format und schlussendlich der Prüfung mithilfe des Z3-Solvers zusammen. Für die Evaluation des Plugins wurde eine Interviewstudie durchgeführt. Diese ergab, dass die korrekte Nutzung von Werkzeugen zur automatisierten Prüfung, zu einer signifikanten Reduzierung der benötigten Zeit und zur Verringerung der menschlichen Fehlerquote bei Erreichbarkeitsanalysen führt. Dies zeigt, dass die korrekte Nutzung des Plugins wahrscheinlich ebenso dieselben Ergebnisse vorweisen könnte. Y1 - 2024 UR - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:573-45901 CY - Ingolstadt ER -