Sonderforschungbereich SFB/TR 14
Der Sonderforschungsbereich/Transregio „SFB/TR 14: Automatic Verification and Analysis of Complex Systems“, kurz: AVACS, ist ein an den Universitäten Freiburg, Saarbrücken und Oldenburg angesiedeltes Großprojekt in Kooperation mit dem Max-Planck-Institut für Informatik in Saarbrücken und unter Mitwirkung von Forschern an der Tschechischen Akademie der Wissenschaften in Prag.
Seit Anfang 2003 gehen hier Forscher der beteiligten Institutionen der Frage nach, wie sich die Zuverlässigkeit von computerbasierten Systemen verbessern lässt, die in sicherheitskritischen Bereichen technische Prozesse steuern. Die Komplexität solcher Steuerungssysteme, die im Transportwesen, in Kraftwerken oder Industrieanlagen zum Einsatz kommen und dort für erhöhte Funktionalität, gesteigerten Komfort und mehr Sicherheit sorgen, ist gewaltig. Sie ergibt sich aus der Interaktion digitaler und physikalischer Prozesse, der Vernetzung einer Vielzahl von Komponenten und dem Einsatz in wechselnden Umgebungen. Dabei werden die Funktionen, die die Steuergeräte erfüllen, immer vielfältiger und anspruchsvoller. Alle zwei Jahre verdoppelt sich die Leistungsfähigkeit der Basiskomponenten, die in der Regel schnell und flächendeckend in Verkehrsmitteln eingesetzt werden. Zugleich wächst jedoch die Fehleranfälligkeit der Systeme, die zwar in Qualitätskontrollen auf korrektes Verhalten überprüft werden, deren gesamter Funktionszusammenhang so aber nicht erfasst werden kann.
Die Zuverlässigkeit dieser Systeme lässt sich nur dann entscheidend verbessern, wenn die Softwareingenieure die kritischen Eigenschaften mit automatisierten Techniken, gewissermaßen auf Knopfdruck, analysieren und überprüfen können. Daher zielt AVACS auf die automatische Analyse hochgradig vernetzter Systeme bereits während der Entwicklungsphase ab (eine gemeinsame Fallstudie in AVACS ist das neue europäische Zugsteuerungssystem ETCS Level 3). Um dieses Ziel zu erreichen, setzen die an AVACS beteiligten Forscher auf die Kombination von Methoden der mathematischen Semantik komplexer Systeme (Fundierung) mit algorithmisch-deduktiven Methoden (Automatisierung).
In der ersten und zweiten Förderphase (2004-2007 bzw. 2008-2011) förderte und fördert die DFG den SFB/TR 14 mit jeweils rund 8 Mio. Euro. Eine Verlängerung der Förderdauer auf insgesamt 12 Jahre ist möglich.