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

• Final Report Year: 2008

Final Report Abstract

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, z.B. Logiken für Datentypen, Prozesskalküle, räumliche und raum-zeitliche Logiken, Beschreibungslogiken für das semantic web uws. Um die Wirksamkeit vielfältiger Konzepte und Methoden innerhalb einer Systementwicklung zu gewährleisten, müssen sie semantisch verträglich sein. Gegenwärtig ist es nicht vorstellbar, dass alle diese Logiken in eine große Logik kombiniert werden — dies wäre zu komplex und unhandlich. Stattdessen verfolgt der Ansatz der Vteiüpomt-Speziflkationen das Paradigma, die'verschiedenen Aspekte eines komplexen Systems in verschiedenen spezialisierten Sprachen zu beschreiben, und auch verschiedene spezialisierte Beweiswerkzeuge dafür einzusetzen. Statt einer monopolistischen "unilateralen" Sicht wird also eine "multilaterale" Sicht der Dinge realisiert. Basierend auf der neuen international standardisierten Spezifikationssprache CASL (Common Algebraic Specification Language) wurde ein Graph von Logiken entwickelt, der Teilsprachen und Erweiterungen von CASL sowie exemplarisch andere Spezifikationssprachen umfasst, darunter auch die Web Ontology Language OWL-DL, die für das Semantic Web verwendet wird. Die heterogene Spezifikationssprache HETÜASL ermöglicht, Spezifikationen in verschiedenen Logiken aufzuschreiben und diese durch Logik-Übersetzungen zu verbinden. DieBeweisumgebung des Heterogeneous Tool Set HETS integriert diverse existierende Analyse- und Beweiswerkzeuge und kombiniert diese zu einem umfassenden Beweismanagement entwickelt werden. Ein Logik-Graph ist dabei die semantische Basis für die heterogene Kombination von Methoden und Werkzeugen. Diese Methode wird mit einem kleinen Beispiel illustriert, nämlich dem Beweis der Korrektheit eines Kalküls zum qualitativen räumlichen Schließen. Der Beweis involviert zwei verschiedene Logiken und Beweiser: einen automatischer first-order Beweiser, der die große Mehrzahl der Beweisziele automatisch abarbeiten kann, und einen interaktiven higher-order Beweiser, mit dem wenige Brückenlemmata, die beide Welten verbinden, bewiesen werden.

Publications

• Algebraic-co-algebraic specification in CoCASL. In Martin Wirsing, Dirk Pattinson, and Rolf Hennicker, editors, Recent Developments in Algebraic Development Techniques, 16th International Workshop, WADT'02, volume 2755 of Lecture Notes in Computer Science, pages 376-392. Springer; Berlin, 2003
  Till Mossakowski, Horst Reichel, Markus Roggenbach, and Lutz Schröder
  
• CASL, the Common Algebraic Specification Language: Semantics and proof theory. Computing and Informatics, 22:285-321, 2003
  Till Mossakowski, Anne Haxthausen, Donald Sannella, and Andrzej Tarlecki
  
• CoCASL at work — modelling process algebra. In Hans-Peter Gumm, editor, Coalgebraic Methods in Computer Science, volume 82 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2003
  Till Mossakowski, Markus Roggenbach, and Lutz Schröder
  
• Foundations of heterogeneous specification. In M. Wirsing, D. Pattinson, and R. Hennicker, editors, Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002, Frauenchiemsee, Germany, 2002, Revised Selected Papers, Lecture Notes in Computer Science, pages 359-375. Springer Verlag, London, 2003
  T. Mossakowski
  
• CASL logic. In Peter D. Mosses, editor, CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science, part IV. Springer Verlag, London, 2004. Edited by T, Mossakowski
  Till Mossakowski, Piotr Hoffman, Serge Autexier, and Dieter Hntter
  
• Casl semantics. In Peter D. Mosses, editor, CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science, part III. Springer Verlag, London, 2004. Edited by D. Sannella and A. Tarlecki
  Hubert Baumeister, Maura Cerioli, Anne Haxthausen, Till Mossakowski, Peter D. Mosses, Doziald Sannella, and Andrzej Tarlecki
  
• CASL sublanguages and extensions. In Peter D. Mosses, editor, CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science, chapter 1:7, pages 61-69. Springer Verlag, London, 2004
  T. Mossakowski
  
• CASL tools. In M. Bidoit and P. D. Mosses, editors, CASL User Manual, volume 2000 of Lecture Notes in Computer Science, pages 131- 142. Springer Verlag, London, 2004
  T. Mossakowski
  
• HETCASL- heterogeneous specification, language summary, 2004
  T. Mossakowski
  
• ModalCASL - specification with multi-modal logics, language summary, 2004
  T. Mossakowski
  
• A simple refinement language for CASL. In Jose Luiz Fiadeiro, editor, WADT 2004, volume 3423 of Lecture Notes in Computer Science, pages 162-185. Springer; Berlin, 2005
  T. Mossakowski, D. Sannella, and A. Tarlecki
  
• Amalgamation in the semantics of CASL. Theoretical Computer Science, 331(l):215-247, 2005
  Lutz Schröder, Till Mossakowski, Andrzej Tarlecki, Piotr Hoffman, and Bartek Klin
  
• Heterogeneous specification and the heterogeneous tool set. Technical report, Universitaet Bremen, 2005. Habilitation thesis
  Till Mossakowski
  
• Iterative circular coinduction for CoCASL in Isabelle/HOL. In Maura Cerioli, editor, Fundamental Approaches to Software Engineering 2005, volume 3442 of Lecture Notes in Computer Science, pages 341-356- Springer; Berlin; 2005
  Daniel Hausmann, Till Mossakowski, and Lutz Schroder
  
• What is a logic? In Jean-Yves Beziau, editor, Logica, Universalis, pages 113- 133. Birkhäuser, 2005
  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, and Andrzej Tarlecki
  
• Algebraic-co-algebraic specification in CoCASL. Journal of Logic and Algebraic Programming, 67(1-2):146-197, 2006
  Till Mossakowski, Lutz Schröder, Markus Roggenbach, and Horst Reichel
  
• Development graphs - proof management for structured specifications. Journal of Logic and Algebraic Programming, 67(1-2):114-145, 2006
  T. Mossakowski, S. Autexier, and D. Hutter
  
• HETS user guide. Technical report. Department of Computer Science; Universität Bremen; Bibliothekstr. 1, 28359 Bremen; 2006
  Till Mossakowski
  
• Institutional 2-cells and grothendieck institutions. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, editors, Algebra, Meaning and Computation. Essays Dedicated to Joseph A, Goguen on the Occasion of His 65th Birthday, volume 4060 of Lecture Notes in Computer Science, pages 124-149. Springer; Berlin, 2006
  Till Mossakowski
  
• Reasoning Support for CASL with Automated Theorem Proving Systems. In J. Fiadeiro, editor, WADT 2006, volume 4409, pages 74-91. Springer-Verlag Heidelberg, 2007
  Klaus Lüttich and Till Mossakowski
  
• Structured CSP - a process algebra as an institution. In J. Fiadeiro, editor, WADT 2006, volume 4409 of Lecture Notes in Computer Science, pages 92-110. Springer-Verlag Heidelberg, 2007
  Till Mossakowski and Markus Roggenbach
  
• The Heterogeneous Tool Set. In Orna Grumberg and Michael Huth, editors, TACAS 2007, volume 4424 of Lecture Notes in Computer Science, pages 519-522. Springer-Verlag Heidelberg, 2007
  Till Mossakowski, Christian Maeder, and Klaus Lüttich