Detailseite
Projekt
Testoptimierung von Quanten-Software auf Basis von funktionalen Eigenschaftsbeschreibungen und Techniken zur Verifikation von Quantenzuständen
Antragsteller
Professor Dr. Otfried Gühne; Professor Dr. Malte Lochau
Fachliche Zuordnung
Softwaretechnik und Programmiersprachen
Optik, Quantenoptik und Physik der Atome, Moleküle und Plasmen
Optik, Quantenoptik und Physik der Atome, Moleküle und Plasmen
Förderung
Förderung seit 2025
Projektkennung
Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 563437167
Die Programmierung eines Quanten-Computers ist schwierig und fehleranfällig. Das erschwert es den Entwicklern neuer Quanten-Algorithmen, funktional korrekten Code zu schreiben. In der klassischen Software-Entwicklung ist Software-Testen eine weit verbreitete und einfach zu nutzende Technik, um systematisch Fehlerstellen im Programm-Code zu finden. Da Software-Testen auf der tatsächlichen Programmausführung beruht, können so nicht nur Fehler in der Software gefunden werden, sondern auch fehlerhafte Effekte auf Ebene der Hardware, was insbesondere für fehleranfällige Quanten-Hardware von großer Bedeutung ist. Allerdings ist die Übertragung klassischer Testkonzepte auf Quanten-Programme schwierig. Das liegt unter anderem daran, dass der Zustand von Quanten-Variablen in Programmausführungen nicht direkt zugreifbar ist und das Messungen auf den Variablen probabilistisch verteilte Ergebnisse liefern. Das Ziel dieses Projektes ist eine neuartige Methodik für den funktionalen White-Box-Test von Quanten-Programmen. Dafür definieren wir zunächst eine Quanten-spezifische Testspezifikationssprache zur Formalisierung funktionaler Korrektheitseigenschaften, die zu testen sind. Das Design der Sprache soll es Entwicklern ermöglichen, Eigenschaften auszudrücken, die zu effektiven Korrektheitstests führen und die zugleich aber auch in einer Quanten-Computing-Umgebung praktisch testbar sind. Wir kombinieren hierfür Ansätze zur Generierung von Testfällen aus probabilistischen Testmodellen mit Techniken zur Verifikation von Quanten-Zuständen, um die Ausführung und Evaluation der generierten Testfälle in Simulatoren zu ermöglichen. Wir verwenden Kostenschätzungen für diese Techniken, um die Balance zwischen Effizienz (Testaufwand) und Effektivität (Wahrscheinlichkeit des Erkennens von Eigenschaftsverletzungen) zu optimieren und ein Verlässlichkeitsmaß für Testergebnisse zu erhalten. Wir untersuchen die praktische Nutzbarkeit der Methodik anhand von zwei Anwendungsszenarien. Das erste Szenario besteht aus einer Sammlung kanonischer Quanten-Algorithmen mit klassischen Ein- und Ausgaben wie z.B. Shor’s Algorithmus. Wir verwenden hierfür Programm-Repositories mit bekannten Fehlern, um verschiedene Teststrategien miteinander zu vergleichen. Das zweite Szenario besteht aus neu entwickelten Algorithmen zur Präparierung von Quanten-Graph-Zuständen als Ausgaben, wofür weiterführende Testkonzepte wie Hyper-Eigenschaften notwendig sind. Um schließlich die Auswirkung von Hardware-Fehlern auf die Verlässlichkeit von Testergebnissen zu untersuchen, verwenden wir zum Simulationen die realistische Fehler mit einschließen, und möglicherweise auch eine Erprobung der Methode auf realer Hardware. Wir interessieren uns hierbei insbesondere für die Frage, ob der Unterschied zwischen Software- und Hardware-Fehlern anhand von Testfällen charakterisiert werden kann.
DFG-Verfahren
Schwerpunktprogramme
