Multi-Logik-Systeme als Basis für heterogene Spezifikation und Entwicklung

• Applicant: Professor Dr. Bernd Krieg-Brückner
• Subject Area: Theoretical Computer Science
• Term: from 2000 to 2008
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5230411

Formale Methoden sind für die Entwicklung korrekter Software insbesondere in sicherheitskritischen Bereichen bedeutsam. Bei Softwareentwicklungsprojekten werden oft für verschiedene Zwecke mehrere Sprachen und Werkzeuge gleichzeitig in die Entwicklung eingebracht. Um die Wirksamkeit vielfältiger Konzepte und Methoden innerhalb einer Systementwicklung zu gewährleisten, müssen sie semantisch verträglich sein. Basierend auf der neuen international standardisierten Spezifikationssprache CASL (Common Algebraic Specification Language) wurde im ersten Teil des Projekts ein Graph von Logiken entwickelt, der Teilsprachen und Erweiterungen von CASL sowie exemplarisch andere Spezifikationssprachen umfasst, mit denen bereits erfolgreich Anwendungen entwickelt wurden (CSP, OBJ, Larch, Z), siehe auch den beigefügten Zwischenbericht. Im zweiten Teil soll es nun um die Implementierung einer darauf basierenden heterogenen Spezifikationssprache gehen. Dazu sollen existierende Analyse- und Beweiswerkzeuge integriert und ein umfassenden Beweismanagement entwickelt werden. Der Logik-Graph ist so die semantische Basis für die heterogene Kombination von Methoden und Werkzeugen.

• DFG Programme: Research Grants
• Participating Person: Professor Dr. Hans-Jörg Kreowski