Inhalt

UML-Aktivitätsdiagramme können mit Model Checkern auf Eigenschaften untersucht werden. Am PST Lehrstuhl wurde dazu der Hugo/RT-Model Checker entwickelt. Oftmals sind die Modelle jedoch viel zu gross, um mit vertretbarem Aufwand checkbar zu sein. Um dem zu begegnen wird üblicherweise das Model von Hand abstrahiert.
Zweck dieser Diplomarbeit soll die Untersuchung von Abstraktionstechniken sein, die mit Hugo/RT verwendet werden können. Dabei kann auf eine bestehende Arbeit zu einem durch eine Problemstellung aus der Industrie motivierten Modell zurückgegriffen werden, wo bereits etliche Abstraktionsschritte vorgenommen wurden. In der Arbeit sollen diese Schritte generalisiert und bzgl. Automatisierbarkeit untersucht werden.

---

Voraussetzungen

• Wünschenswert sind Kenntnisse in formaler Spezifikation/UML/Model Checking
• Bereitschaft zum theoretischen Arbeiten

Auftragssteller

Prof. Dr. Alexander Knapp

Betreuer

Moritz Hammer