Grundlagen Invasiven Rechnens (A01)

Trotz strikter Isolierbarkeit paralleler Programme auf Mehrkernsystemen durch invasives Rechnen, vereiteln Unsicherheiten der Eingabe, des Maschinenzustands und der Umgebung immer noch die Berechnung enger Schranken nichtfunktionaler Eigenschaften wie Ausführungszeit und Leistungsverbrauch sowie deren Einhaltung. Zur Lösung werden neue Konzepte und Methoden zur Laufzeitdurchsetzung solcher Eigenschaften untersucht. Dies umfasst (a) zentrale und verteilte, (b) leichte und strikte, (c) formale Verifikationstechniken zur strikten Durchsetzung und für allgemeine Programmeigenschaften, sowie (d) zur Generierung von Durchsetzern.