Aufgrund der immer weiter gehenden Erfolge bei der Miniaturisierung ist es einerseits prinzipiell möglich, immer komplexere Hard- und Softwaresysteme zu bauen, und andererseits können diesen Systemen immer neue Anwendungsgebiete erschlossen werden. Informationsverarbeitende Systeme sind heute nicht nur im Bereich von klassischen Großrechnern und Personalcomputern zu finden, sondern mehr und mehr auch in Eingebetteten Systemen, die eingebettet in sie umgebende technische Systeme komplexe Steuerungs-, Regelungs- und Datenverarbeitungsaufgaben übernehmen. Auf zahlreichen Gebieten des täglichen Lebens finden sich typische Anwendungsfelder solcher eingebetteter Systeme, beispielsweise in Automobilbau, Luft- und Raumfahrt, Telekommunikation, der Steuerung und Regelung von Produktionsprozessen oder auch Instrumented Homes.

Aus der beschriebenen Situation ergeben sich die zwei wesentlichen Schwerpunkte unserer Forschung:

Mit der wachsenden Komplexität heutiger Hard- und Softwaresysteme wird es völlig unmöglich, diese Systeme von Hand zu entwerfen. Eine Unterstützung durch Rechner ist unerlässlich. Wir beschäftigen uns daher mit rechnergestützten, automatisierten Entwurfsmethoden für Hard- und Softwaresysteme .

Darüber hinaus wird es immer schwieriger, die Korrektheit hochkomplexer Entwürfe zu garantieren. Da die so entworfenen informationsverarbeitenden Systeme aber häufig in sicherheitskritischen Bereichen eingesetzt werden, sind Kompromisse bezüglich Zuverlässigkeitsgarantien nicht akzeptabel. Es wird immer wichtiger, sich schon in frühen Phasen der Projektplanung mit Zuverlässigkeitsfragen auseinander zu setzen und einen ausreichenden Aufwand zur Gewährleistung der Entwurfskorrektheit zu betreiben. Aus diesem Grund beschäftigen wir uns insbesondere mit formalen Methoden zur Verifikation von Hard- und Softwaresystemen .

• Formale Verifikation durch Äquivalenztests und Modellprüfung: 
  Wir entwickeln formale Methoden, um die Korrektheit informationsverarbeitender Systeme zu beweisen. Formale Verifikation garantiert allgemein die Äquivalenz von (in abstrakterer Form) gegebenen Spezifikationen und dazugehörigen Implementierungen (in konkreterer Form).
  
  
  Für Spezifikationen, die aus einer Menge von temporalen Systemeigenschaften bestehen, entwickeln wir spezielle Modellprüfungsverfahren. Hierbei liegen die Herausforderungen sowohl in einer effizienten Darstellung der Menge aller möglichen Zustände großer Systeme als auch im Umgang mit unvollständiger Information. Unvollständige Information tritt auf bei Implementierungen, die noch nicht vollständig abgeschlossen sind bzw. bei denen es Teilkomponenten gibt, die von Fremdanbietern entworfen wurden, so dass bestimmte Implementierungsdetails nicht offen gelegt sind. Unser Schwerpunkt liegt in der Entwicklung effizienter Datenstrukturen und Algorithmen, insbesondere auch in der Entwicklung Verfahren, die aus Effizienzgründen Approximationen verwenden, aber dennoch in der Lage sind, definitive Aussagen zu liefern.
  
  
  

   

• Fehlerdiagnose:
  Wir beschäftigen uns damit, in fehlerhaften Designs die mögliche Lage der Fehler zu lokalisieren, um dem Entwerfer Ansatzpunkte zur Fehlerkorrektur liefern.
  
  

   

• VLSI-Entwurf, insbesondere FPGA-Synthese:
  Wir befassen uns im Bereich des VLSI-Entwurfs beispielsweise mit der automatisierten Abbildung von Verhaltensspezifikationen auf FPGAs. FPGAs (Field Programmable Gate Arrays) sind rekonfigurierbare Recheneinheiten, die sehr flexibel eingesetzt werden können, da sie ihre Funktion erst beim Anwender durch Konfigurierung erhalten. Darüber hinaus können sie sogar zur Laufzeit dynamisch neu konfiguriert werden.
     

   

• Echtzeitbetriebssysteme:
  Im Rahmen des neu eingerichteten Graduiertenkollegs „Embedded Microsystems“ befassen wir uns mit der Generierung von Echtzeitbetriebssystemen, die angepasst an die vorgegebene Anwendung und Architektur harten Speicherplatz-, Laufzeit- und Energieanforderungen gerecht werden können.