Vergleichende Analyse und Verifikation für Verteilte Sicherheitskritische Systeme (CAVER)

• Antragsteller: Professor Dr. Norbert Müller, seit 7/2018
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 255389725

Die wachsende Größe und die vernetzte und zeitkritische Natur von Telekommunikationsdiensten, Controllern, Webdiensten, mobilen und eingebetteten Geräten, usw., verursacht Probleme der präzisen Wahrnehmung ihres Verhaltens und der Gewährleistung ihrer sicheren Funktion. Allgemeine Ansätze zur Lösung dieses Problems beruhen auf rigorosen Formalismen und auf computergestützten Werkzeugen, die beim Entwurf und bei der Implementierung solcher Systeme auf allen Ebenen hilfreich sein können. CAVER wird neue und effiziente theoretische Rahmenbedingungen untersuchen, die sowohl mathematisch präzise als auch entwurfsfreundlich sein sollen und genügend Details über Struktur und Verhalten eines Systems zu zeigen in der Lage sind. Mit diesem Ziel möchte CAVER sich in eine Anzahl bereits existierender Teams mit ähnlichen Zielen im Bereich verteilter, zeitkritischer Systeme einreihen. Die Kombination von Expertise in den Bereichen der Modellierung, der Analyse, des Testens und der Verifikation von Systemen und Anwendungen im CAVER-Team eignet sich perfekt für ein Herangehen an theoretische und praktische Herausforderungen bei der Betrachtung verteilter und korrektheitskritischer Systeme (CCCS). Wir sehen unsere spezielle Rolle in folgenden Aktivitäten:Die Klassifikation formaler Modelle und die Unifikation von Verhaltensäquivalenzen für CCCS, um ein noch besseres Verständnis für die inhärent verteilte, nichtdeterministische und zeitabhängige Natur des Verhaltens eines Systems zu erlangen, und um existierende Resultate über das Verhältnis verschiedener Modelle und Äquivalenzen zueinander zu verstärken, sowie neue Resultate abzuleiten.Die Erarbeitung und Entwicklung verschiedener, auf Model-Checking und auf Constraint-Lösetechniken beruhender Verifikationsmethoden zur qualitativen und quantitativen Argumentation über das Verhalten von CCCS.Die Implementierung von Fallstudien und deren Leistungsanalyse, um die vorgeschlagenen theoretischen Methoden zu vergleichen und zu bewerten, und um ihre Anwendbarkeit und Vielseitigkeit aufzuzeigen. Die Algorithmen, die wir im Verlauf unserer Forschungen entwickeln wollen, sollen als Experimentierbett und zur Entwicklung von Prototypen dienen.Auch in ihren theoretischen Aspekten werden die Untersuchungen in CAVER von real existierenden Problemen beeinflusst; sie bezwecken die Förderung neuer Methodologien zur Korrektheitsprüfung und zur Herleitung der Eigenschaften von Systemen. Wir hoffen, dass die praktischen Konsequenzen dieses Vorhaben von vielfältiger Natur sind: der Entwurf von CCCS soll erleichtert und verbessert, und der Betrieb von CCCS soll verlässlicher und sicherer werden.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Russische Föderation
• Partnerorganisation: Russian Foundation for Basic Research
• Beteiligte Personen: Professor Dr. Peter Buchholz; Dr. Margarita Korovina; Privatdozentin Dr. Louchka Popova-Zeugman; Dr. Igor Tarasyuk; Professorin Dr. Irina Virbitskaite
• Ehemaliger Antragsteller: Professor Dr. Eike Best, bis 7/2018