Entwicklung. Implementierung und Anwendung mathematisch-algebraischer Algorithmen bei der formalen Verifikation digitaler Systeme mit Arithmetikblöcken

• Antragsteller: Professor Dr. Gert-Martin Greuel; Professor Dr.-Ing. Wolfgang Kunz
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2006 bis 2011
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 16728219

Industrieller Hintergrund dieses Forschungsvorhabens sind die aktuellen, großen Erfolge bei der Hardwareverifikation durch sog. formale Methoden. Im Unterschied zur bislang üblichen Simulation garantieren formale Methoden bestimmte Eigenschaften eines Systems mit mathematischer Exaktheit. Trotz ihres großen Erfolges sind formale Verifikationsmethoden dafür berüchtigt, dass sie bei arithmetischen Schaltungs- und Prozessorblöcken häufig auf unüberwindliche Komplexitätsprobleme stoßen. Durch Weiterentwicklung der gebräuchlichen Beweistechniken konnte dieses Problem bislang nicht gelöst werden. Daher soll in diesem interdisziplinären Projekt zwischen Informationstechnik und Mathematik ein grundsätzlich neuer Ansatz entwickelt und untersucht werden. Die arithmetischen Komponenten der Schaltung werden mithilfe einer von den Antragstellern aus der Informationstechnik entwickelten Methodik auf der Bitebene so modelliert, dass darauf nicht logische, sondern bestimmte arithmetische 1-Bit Operationen ausgeführt werden können. Diese Beschreibung stellt die Ausgangsbasis für eine abstrakte, algebraische Modellierung dar. In interdisziplinärer Zusammenarbeit zwischen Mathematik und Informationstechnik wird eine algebraische Modellierung des Gesamtsystems entwickelt, bei der die arithmetischen Blöcke auf Wortebene sowie ihr Zusammenwirken mit der umgebenden Logik auf Bitebene erfasst werden. Die Antragsteller aus der Mathematik entwickeln und erforschen neue algebraische Methoden, die auf diese Problemstellung angepasst sind. Das große Potential für die Anwendung algebraischer Methoden besteht darin, dass sie einen universellen Formalismus zur Verfügung stellen und arithmetische Modelle auf höheren Ebenen gemeinsam mit Modellen auf niedrigeren Ebenen effizient verarbeiten können. Darüber hinaus eröffnen neue Algorithmen zu symbolisch-algebraischen Berechnungen kombiniert mit speziellen Datenstrukturen die Perspektive, über die Grenzen des bisher Berechenbaren deutlich hinaus zu gehen.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Gerhard Pfister