03. Juli 2009

Ein Elektro-Schiri prüft die Software

Freiburger Wissenschaftler erarbeiten Computerprogramme, die testen, ob andere Programme halten, was Hersteller versprechen

FREIBURG. Ein elektronischer Schiedsrichter entscheidet für "Salomo". Dieses Forschungsprojekt soll Vertragsabschlüsse kleiner und mittelständischer Unternehmen mit Softwareherstellern vereinfachen. Sie scheitern oft an unsicherer Rechtslage und daran, dass die Qualität von Programmen schwer kontrollierbar ist. Das Wissenschaftsministerium des Landes fördert "Salomo" mit einer Million Euro. In Mannheim feilen Rechtswissenschaftler an standardisierten, sicheren Verträgen. In Freiburg arbeitet das Team des Informatikers Andreas Podelski am Elektro-Schiri – an Software, die Software prüft.

Verifikation heißt diese Informatikdisziplin. "Freiburg ist eine Hochburg in dieser Forschungsrichtung", sagt Andreas Podelski. "Sie ist so etwas wie der heilige Gral der Informatik." Die Korrektheit von Programmen gilt als nicht berechenbar. "Sie können einen Lügner nicht entlarven, indem sie ihn fragen, ob er lügt", erklärt der Inhaber des Lehrstuhls für Softwaretechnik. Unfehlbarkeit werden elektronische Schiedsrichter also nie erlangen, ihr durch Verbesserungen aber stetig näher kommen. "Einige Ideen dahinter sind recht alt", sagt Podelski. Die Anfänge der Model-Checking-Algorithmen – dem Herz des digitalen Unparteiischen – etwa 30 Jahre. Diese Verfahren seien extrem rechenintensiv, sie eigneten sich höchstens, um Miniprogramme in hochspeziellen Fällen zu überprüfen. Nur große Firmen konnten sich entsprechende Rechner leisten, nur die Programmierer ihre kleinen Prüfsoftware-Pakete bedienen und verstehen. Deshalb ist der elektronische Schiedsrichter in kaum brauchbare, verstreute Teile zerstückelt.

Um sich auf den aktuellen Stand zu bringen, schauen sich die Informatiker auffindbare Teile an. Sie sammeln nützliche Ideen, schreiben neue Programmteile und führen sie zusammen. Nun müssen sie garantieren, dass ihr Programm funktioniert, Qualität besitzt und benutzbar ist. "Wir müssen sein riesiges Potenzial hinter wenigen ,Knöpfen’ verbergen und das Ergebnis so gestalten, dass es ein typischer Software-Entwickler versteht", sagt Projektleiter Bernd Westphal. Der Elektro-Schiri soll zuerst ein paar Spezialfälle entscheiden. "Er guckt sich jede Programmzeile an", sagt Westphal. Wie einen Routenplan, der bei Stau, Baustellen und roten Ampeln alternative Wege anbietet, wird er alle Strecken und Verzweigungen eines Programms abfahren. Dabei stößt er vielleicht auf Widersprüche: Entgegen der Anweisung ist rechts Abbiegen an der Kreuzung X verboten. Womöglich fehlen auch wichtige Streckenalternativen? So macht er sich ein Bild von der Software. "Danach geht der Daumen hoch oder runter", sagt Doktorand Daniel Dietsch. Zeigt der Finger aufwärts, erfüllt ein Programm die geforderten Eigenschaften sicher.

Bisher war es besonders für kleine und mittelständische Unternehmen (KMU) zu aufwendig, maßgeschneiderte Software zu prüfen. Sie mussten digitale Katzen in virtuellen Säcken kaufen. Weil auch Rechtsberatungen zu Verträgen mit Softwareentwicklern teuer und zeitraubend sind, nahmen KMU eher in Kauf, dass Umsätze flöten gingen: Sie schlugen sich mit komplizierten und unzuverlässigen Programmen durch. "Weil die Firmen nicht wussten, wie sie sichere Verträge abschließen können, haben sie solche Aufträge gar nicht vergeben", sagt Podelski. Er und Louis Pahlow, Lehrstuhlinhaber für Bürgerliches Recht, Recht des Geistigen Eigentums und Wettbewerbs an der Uni Mannheim, kooperieren mit zwei KMU, um deren Sorgen zu berücksichtigen. Ihnen soll "Salomo" Sicherheit bringen sowie Zeit und Geld sparen. Deshalb suchen die Wissenschaftler mehr Informationen zu den Anforderungen der KMU, zu juristischen und technischen Tücken. "Wer da Erfahrungen hat, kann sich gerne melden", sagt Podelski.

Denn juristisch ist nicht einmal klar, ob Programme überhaupt gegenständlich sind oder geistiges Eigentum. Softwareentwicklungsverträge fallen in keine vor Gericht gültigen Kategorien. Und was bedeutet Zuverlässigkeit bei Programmen: Darf es einmal täglich abstürzen oder nur einmal im Jahr? Mit dieser Unsicherheit sollen standardisierte Musterverträge aufräumen, an denen Pahlows Gruppe arbeitet. Die Vertragspartner müssen nur individuelle Passagen einfügen. Sie legen etwa Eigenschaften fest, die das Produkt erfüllen muss und die der elektronische Schiedsrichter prüfen kann. "Beide Seiten erkennen ihn an", sagt Podelski. Das erscheint fair: Der Vertrag stammt aus einer unparteiischen Quelle, das Kontrollprogramm ebenso. Der Schiri ersetze allerdings nicht den gesunden Menschenverstand, warnt Andreas Podelski: "Er ist kein elektronischer Richter – dafür bräuchte er ja künstliche Intelligenz." Soweit sind selbst die Freiburger Spezialisten noch nicht.  

Autor: Jürgen Schickinger