Um die Sicherheit von Computerprogrammen und der Hardware zu erhöhen, werden mathematische Analysemethoden benötigt. Ein Forscherteam um den Computerwissenschaftler Krishnendu Chatterjee hat nun innerhalb eines vom Wissenschaftsfonds FWF finanzierten Projekts Möglichkeiten gefunden, diese Methoden in Zukunft deutlich zu beschleunigen. „Dieses Gebiet hat eine lange Tradition“, sagt Chatterjee, der Professor am IST Austria ist. „Es gibt seit langer Zeit Versuche, eine formale Basis zu finden, um korrekte Systeme zu designen.“ Das mittlerweile beendete Projekt war sehr erfolgreich: Es gelang, mehrere seit den Neunzigerjahren bestehende Schranken für die Geschwindigkeit bestimmter Verifikationsalgorithmen zu durchbrechen, etwa im Bereich sogenannter „Markov Decision Processes“. Das sind Modelle, die mehrere Auswahlmöglichkeiten und ein Zufallselement beinhalten. „Ein Beispiel ist die Entwicklung von Robotern“, erklärt Chatterjee. „Ein Roboter interagiert mit einer Umgebung, in der es Unsicherheit gibt, und er hat Auswahlmöglichkeiten, kann etwa nach links oder rechts gehen. ‚Markov Decision Processes‘ sind ein Modell dafür.“ Für viele Anwendungen ist die Beantwortung der Frage zentral, welche Ereignisse in so einem Modell mit absoluter Sicherheit eintreten. „Der bisher effizienteste Algorithmus dafür war von 1995 und hatte quadratische Komplexität“, sagt Chatterjee. Damit ist gemeint, dass die Laufzeit des Algorithmus mit der Größe des untersuchten Systems quadratisch steigt – ein doppelt so großes System braucht also die vierfache Laufzeit. „In unserem Projekt konnten wir diese Grenze mit Graph-algorithmischen Techniken überwinden.“ Er betont aber auch, dass es sich um ein reines Grundlagenprojekt handelte. „Unsere erste Arbeit war sehr theoretisch. Nun versuchen wir, Grenzen oder Bedingungen aufzuzeigen, wie schwierig es sein wird, unsere Algorithmen weiter zu verbessern. Auf der anderen Seite wollen wir sehen, wie sich diese Zugänge in der Praxis umsetzen lassen.“
Für die mathematische Analyse von Computersystemen wird die sogenannte „Graphentheorie“ genutzt. Ihr Gegenstand sind Objekte, die man sich als Netzwerke aus miteinander verbundenen Punkten oder Knoten vorstellen kann. Computersysteme lassen sich mathematisch als Graphen darstellen: Ein Knoten steht für einen bestimmten Zustand, in dem sich das System befindet, eine Kante steht für einen Übergang zwischen zwei Zuständen. Zum Beispiel befindet sich ein Computer, der gerade diesen Artikel anzeigt, in einem definierten Zustand, der als Knoten dargestellt wird. Beim Klicken auf einen Link wechselt das System in einen neuen Zustand, dieser Wechsel wird als Kante dargestellt. ik
Teilen:
