Koalgebraische Softwareverifikation

• Antragsteller: Professor Dr. Horst Reichel
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2002 bis 2005
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5369843

Das beantragte Teilprojekt soll einen Beitrag zum Nachweis von qualitativen Eigenschaften des dynamischen Verhaltens von Softwarekomponenten liefern. Der Schwerpunkt liegt dabei in der Formalisierung und der Analyse des dynamischen Verhaltens und im Nachweis von Sicherheits- und Lebendigkeitseigenschaften (dabei werden den Sicherheitseigenschaften im Sinne von "safety" und nicht im Sinne von "security" verstanden). Mit dem Projekt werden zwei Ziele verfolgt: 1. Der formale Apparat der koalgebraischen Formalisierung von reaktiven Systemen und die koinduktiven Beweismethoden sollen an realen Anwendungen erprobt werden. 2. Nachweis qualitativer Sicherheitseigenschaften für zentrale Codestücke des Medienservers, der in dem früheren Teilprojekt G3 Entwurf von echtzeitfähigen Medienobjekt-Speichersystemen des SFB 358 konzipiert wurde, und jetzt unter der Leitung von Professor Dr. Meyer-Wegener an der Universität Erlangen weiterentwickelt wird.

• DFG-Verfahren: Sachbeihilfen