Methodologies for Trustworthiness
Das empirische Bestimmen von Systemeigenschaften, zum Beispiel durch das Testen von Software, ist in ihrer Aussagekraft sehr beschränkt. Vertrauenswürdigkeit muss bereits in der Systemspezifikation und im Entwurfsprozess von Systemen berücksichtigt werden. Dazu sind neuartige Methoden erforderlich, mithilfe derer das erwünschte Maß an Vertrauenswürdigkeit in die Systemspezifikation einfließen kann. Diese Methoden müssen mittels Verfahren umsetzbar sein, die automatisiert und maschinell ausführbar sind.
Die Arbeit an diesen Methoden zielt darauf ab, langfristig Systeme zu entwerfen, die von Anfang an („by design“) vertrauenswürdig sind. Zu diesem Zweck setzt das BI auf formale Methoden, also strenge mathematische Überlegungen und Beweise, anstelle empirischer Verfahren wie Messungen oder Tests.
Grundsätzlich verfolgt das BI einen ganzheitlichen Ansatz, der mehrere Phasen des Lebenszyklus dieser Systeme abdeckt – von der Standardisierung über den Entwurf und die Implementierung bis hin zur Bereitstellung und Laufzeit.
Derzeit liegt unser Fokus auf Methoden für den Entwurf und die Implementierung von vertrauenswürdigen Systemen. Konkret sind dies Methoden der formalen und automatisierbaren Spezifikation von Systemen, Programmiersprachen und Compiler, die diese Spezifikationen umsetzen, sowie Methoden zur formalen Verifikation der vom Compiler erzeugten Ergebnisse. Diese Themen werden von den Gruppen Trustworthy Data Processing und Verified System Design Automation bearbeitet.