Skip Navigation

Barkhausen Institut

Verified System Design Automation

Die Verified System Design Automation Group (VerSA) konzentriert sich darauf, durch formale Verifikation und formal verifizierte Kompilierung die Zuverlässigkeit von Hardware- und Softwaresystemen von Grund auf sicherzustellen.

Verifizierung

In einer digitalen Gesellschaft werden die Systeme zunehmend komplexer. Mit Millionen von Ausführungswegen ist es sehr schwierig, Vertrauen in solche komplexen Systeme aufzubauen. Jeden einzelnen Pfad zu testen, ist praktisch unmöglich und kostet viel Energie.
In unserer Gruppe versuchen wir, teure Tests durch mathematische Schlussfolgerungen zu ersetzen. Bereits in der Designphase verwenden wir Theorembeweiser wie Coq, um die Korrektheit der von uns (mit)entwickelten Systeme mathematisch zu beweisen. Diese formale Verifikation stellt sicher, dass unsere Systeme gemäß unseren Erwartungen funktionieren (funktionale Korrektheit) und Sicherheit gegen potentielle Bedrohungen gewährleisten. Somit macht die formale Verifikation unsere Systementwürfe sowohl vertrauenswürdig als auch energieeffizient.

Automatisierung

Das Beweisen von Theoremen und das mathematische Argumentieren erfordern oft ein hohes Maß an Expertise, was die Integration in den konventionellen Entwicklungszyklus behindert. Um dieses Problem zu überwinden, identifizieren wir Anwendungsbereiche, in denen alle Programme gemeinsame Eigenschaften haben, z. B.  Hardware-Designs für skalierbare Mehrprozessorsysteme und verteilte Programme für Mikrokern-Betriebssysteme. Für solche Bereiche entwickeln wir spezifische Sprachen und Compiler. Unsere Compiler definieren wichtige Eigenschaften für Software und Hardware. Entwickler:innen können sie verwenden, um Hardware oder verteilte Programme zu entwerfen, ohne Fachwissen im Beweisen von Theoremen zu benötigen.

Unser Team

Sebastian Ertel
Dr.-Ing.Sebastian ErtelSenior Researcher
Lisza Zeidler
Dipl.-Inf.Lisza ZeidlerAssociate Researcher
Jeronimo Castrillon
Prof. Dr.Jeronimo CastrillonBI Research Fellow