Projektträger: Deutsche Forschungsgemeinschaft
Dauer: 1. Mai 2012 - 31. April 2014
Projektleitung: Prof. Dr. Ina Schaefer
Zusammenfassung:
Moderne Softwaresysteme existieren in verschiedenen Varianten zum selben Zeitpunkt, was als Variabilität im Raum bezeichnet wird. Zusätzlich sind entwickeln sich diese Systeme über die Zeit weiter, um sich an veränderte Anforderungen anzupassen, was zeitliche Variabilität genannt wird. Es ist wichtig, kritische Eigenschaften der Systemvarianten sicherzustellen. Jedoch ist es im allgemeinen nicht praktikabel, alle Varianten in Raum und Zeit einzeln zu überprüfen. Daher werden Verifikationstechniken benötigt, welche die Analyse effizienter ermöglichen.
Im beantragten Projekt entwickeln wir ein uniformes Varabilitätsmodellierungsframework, um Systemvarianten in Raum und in Zeit modular und hierarchisch zu beschreiben. Basierend auf der Variabilitätsmodellierung entwerfen wir Programmiersprachenkonstrukte, welche die Implementierung von variablen und sich fortentwickelnden Systemen auf eine strukturierte und semantisch fundierte Weise ermöglichen. Wir stellen eine formale Spezifikationssprache bereit, um gewünschte Systemeigenschaften und ihre Variabilität auf der Programmcodeebene zu spezifizieren. Für den Nachweis der Eigenschaften auf dem Programmcode entwickeln wir inkrementelle und kompositionale Verifikationstechniken, welche die Variabilitätsstrukturen ausnutzen, so dass es nicht notwendig ist, jede Systemvariante einzeln zu betrachten.