Coordination: Rigorous Systems Engineering (RiSE)

Computersoftware und -systeme haben in den letzten Jahren immer zahlreichere An-wendungen in verschiedenen oft sicherheitskritischen Bereichen gefunden. Die zunehmende Komplexität und Größe dieser Systeme erfordert den Einsatz computerbasierter Methoden und Werkzeuge, die auf einer soliden mathematischen Grundlage beruhen und den Entwicklungsprozess unterstützen. Obwohl Techniken wie Model Checking und Statische Analyse in der Entwicklung von Hardware und spezifischen Klassen von Software mittler-weile als Standardwerkzeuge eingesetzt werden, sind durch die massive Parallelität moderner Systeme von Multi-Core bis Cloud Computing viele traditionelle Methoden unzureichend geworden: Der korrekte Umgang mit Parallelität gilt als die zentrale Herausforderung für die Software- und Systementwicklung. Das klassische Szenario für den Einsatz von Model Checking und verwandten Methoden sieht eine a posteriori Analyse vor, das heißt, ein Programm oder Modell wird nach Fertig-stellung analysiert. Da ein solcher Ansatz aufwendig ist und die Qualitätssicherung vom Entwicklungsprozess nachteilig entkoppelt, strebt unser Projekt eine Entwicklungsmethodik an, in welcher mathematische Methoden wie Model Checking ein essentieller Teil des Entwicklungsprozesses sind. Diese neuartige Entwicklungsmethodik fassen wir unter dem Begriff "Rigorous Systems Engineering" zusammen. Innerhalb von RiSE konzentrieren wir uns auf Anwendungsfelder aus dem Bereich parallele und eingebettete Systeme, so etwa unter dem Aspekt von Multi-Core und Software-as-a-Service speziell auf Software Trans-actions und Data Center Programming; unter dem Aspekt der Echtzeit auf Virtualisierung und Verteilte Message Passing Systeme; und unter dem Aspekt der Werkzeugunterstützung auf die Entwicklung hochskalierender Analysetools, die Model Checking mit Testen kombinieren. Die Umsetzung des Projektes erfolgt anhand dreier Problemgruppen: (1) Neue Paradigmen für Sprachen, Architekturen und Verifikation hochparalleler Software unter Berücksichtigung von Echtzeitanforderungen. (2) Neue spieltheoretische Algorithmen zur Analyse und Syn-these einzelner Komponenten im Kontext größerer Systeme. (3) Neuentwicklung und Ver-besserung von Entscheidungsprozeduren als zentraler Bestandteil aller automatischen Methoden und Werkzeuge der Systemanalyse und Systementwicklung. Das Konsortium von RiSE besteht aus fünf international angesehenen Wissenschaftlern aus dem Bereich Model Checking und vier weiteren renommierten Wissenschaftlern aus den angrenzenden Gebieten der Softwaresysteme, Verteilten Systeme und der Computationalen Logik. Diese Konstellation stellt die Integration unterschiedlicher Sichtweisen und kom-plementärer Lösungsansätze für die wissenschaftlichen Fragestellungen im Rahmen von RiSE sicher.