Einsatz von Verifikationstechniken unter Berücksichtigung unvollständiger Information

• Applicant: Professor Dr. Bernd Becker
• Subject Area: Software Engineering and Programming Languages
• Term: from 2003 to 2010
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5392100

Technologische Fortschritte ermöglichen stetig steigende Integrationsdichte in der Chipherstellung. Neben dem eigentlichen Entwurf wird dabei zunehmend der Nachweis seiner Korrektheit zu einer Herausforderung, die Kosten dafür machen teilweise mehr als die Hälfte der gesamten Entwurfskosten aus. Da durch reine Simulation zumindest bei größeren Systemen nur ein verschwindend geringer Bruchteil des Systemverhaltens erfasst werden kann, haben in jüngster Zeit auch im industriellen Umfeld automatisierte, formale Methoden zum Beweis der Korrektheit von Schaltungen eine enorme Bedeutung erlangt. Allerdings sind diese Methoden zur Zeit noch fast ausschließlich darauf beschränkt, die Korrektheit auf der Basis einer vollständigen Beschreibung des Entwurfes nachzuweisen. Andererseits führen erst spät im Designablauf entdeckte Fehler zu enorm hohen Kosten. Es ist deshalb erstrebenswert, schon möglichst früh, d.h. auch zu einem Zeitpunkt, wenn nur unvollständige Information über den Gesamtentwurf zur Verfügung steht, Maßnahmen zu einer möglichst vollständigen Entdeckung schon vorhandener Fehler zu ergreifen. Bisher werden dazu, wenn überhaupt, fast ausschließlich simulationsbasierte Methoden angewendet. Es ist zu vermuten, dass durch die Anwendung von formalen Verifikationstechniken schon in frühen Phasen des Designablaufs eine wesentlich exaktere Fehlererkennung möglich ist. Es sollen deshalb Techniken zur (formalen) Verifikation bei unvollständiger Information entwickelt werden auf den Gebieten. Äquivalenztest kombinatorischer Schaltungen, Äquivalynztest sequentieller Schaltungen und Beweis von Eigenschaften sequentieller Schaltungen. Ein Sondergutachter für Informatik schreibt: "...Das Projekt ist kompetent beschrieben und ich bin überzeugt, dass von den vielen kleineren Aufgaben eine Reihe gelöst werden kann. Den Aufwand dafür kann ich nicht abschätzen. Das Projekt ist wichtig und Verbesserungen auf diesem Gebiet sind erwünscht. Die Kosten erscheinen mir aber im Verhältnis zu dem Gewinn zu hoch. Mein Vorschlag wäre, eine Bat IIa-Stelle zu streichen. Es sollte versucht werden, die oberen Komplexitätsgrenzen des Verfahrens und die Skalierbarkeit zu untersuchen. Zusammenfassend spreche ich mich für eine Förderung aus, mit der angegebenen Kürzung. Ich würde eine hohe, aber nicht die höchste Priorität ansetzen, da die Arbeiten zwar sehr interessant sind, aber sehr stark auf dem aufbauen, was andere auf diesem Gebiet geleistet haben."

• DFG Programme: Research Grants
• Participating Person: Professor Dr.-Ing. Christoph Scholl