Heterogene Software Spezifikation

Ziel dieses Forschungsthemas ist die Verbesserung der theoretischen Grundlagen sowie der Anwendbarkeit von Spezifikationsformalismen reaktiver Systeme, welche Zustandsautomaten mit logischen Operatoren kombinieren. Aktuelle Beispiele hierzu sind die Interface Theorien von de Alfaro/Henzinger und Caillaud et al., die Konjunktion betrachten, und die Contractual State Machines von Paige et al., die temporale Logikoperatoren beinhalten. Obwohl diese heterogenen Sprachen mehr Prägnanz beim Spezifizieren versprechen und von modernen, Verfeinerungs basierten Ansätzen des Software Entwurfs begleitet werden, fehlt ihnen jeweils eine mathematisch robuste Semantik, die auch die Nebenläufigkeitsaspekte reaktiver Systeme berücksichtigt.

Unsere Forschung soll diese Unzulänglichkeiten mittels Techniken der Logic Labelled Transition Systems (Logic LTS), die an dem Bamberger Lehrstuhl Softwaretechnik und Programmiersprachen mitentwickelt worden sind, beheben. Dies wird die Entwicklung neuer Software Werkzeuge ermöglichen, einschließlich automatischer Verfeinerungs-Checker für Interface Theorien und Contractual State Machines. Weiterhin soll Logic LTS so erweitert werden, dass Sicherheits-, Lebendigkeits- und Fairnesseigenschaften in Spezifikationen eingebettet und somit reichhaltigere Interface Theorien entwickelt werden können. Dies wird eine prägnantere Beschreibung der Software reaktiver Systeme ermöglichen und dadurch Programmierer bei der Software Spezifikation und dem Software Design unterstützten.

Kontakt: Prof. Dr. Gerald Lüttgen