EXTRA-Treffen Archiv WS 99/00 und SS 00

Bisheriges Program (SS'00)

• 05.05.2000
Architektur-Spezifikationen in CASL

Piotr Hoffman und Till Mossakowski

CASL, die Common Algebraic Specification Language, ist eine ausdrucksstarke Spezifikationssprache. Ein wichtiges Sprachkonstrukt sind die sogenannten Architektur-Spezifikationen, die erlauben, die modulare Struktur von Implementierungen zu beschreiben.

Wir stellen kurz einen einfachen Verfeinerungs- und Entwicklungsbegriff fuer CASL-Spezifikationen vor, geben dann motivierende Beispiele fuer Architektur-Spezifikationen, erklaeren die Sprachkonstrukte und skizzieren die Semantik.

Bisheriges Program (WS'99/00)

• 03.03.00
Internet-Standards für die Verwaltung, Verteilung und Vermittlung mathematischen Wissens

Dr. Michael Kohlhase, FB Informatik, Universität des Saarlandes

In diesem Vortrag möchte ich auf die neuen Möglichkeiten eingehen, die sich durch das Internet für die drei V's im Titel ergeben. Dabei der Terminus ``mathematisches Wissen'' nur als Platzhalter für gut konzeptualisierte, hochstrukturierte Wissens- und Anwendungsgebiete stehen, insbesondere für formale Methoden/Spezifikation in der Programmentwicklung.

Es ist plausibel anzunehmen, dass sich -- zumindest in Anwendung und Lehre -- die Art Mathematik zu betreiben in den nächsten 10 Jahren fundamental ändern wird. Ein besonderes interessanter Aspekt ist dabei die Verteilung, sowohl des mathematischen Wissens, als auch der Berechnung über das Internet.

Ich möchte am Beispiel des des MBase-Systems verteiltes Wissensmanagement in MathWeb (Verteiltes mathematische Berechnung) vorstellen.

Hauptaugenmerk soll dabei den Internet-Standards für die Kommunikation zwischen den beteiligten Software-Systemen (mathematische Services). Ich werde dabei den OpenMath-Standard und die von mir entwickelte dokumentenorientierte Erweiterung OMDoc (OpenMath Documents) vorstellen. Dabei sollen sowohl

• die Grundlagen (XML, XSL, XSLT,...),
• die Software-Werkzeuge zur Manipulation und Visualisierung von
• OpenMath/OMDoc, als auch
• die Verbindungen zu CASL
behandelt werden.
• 26.01.00
Eine erste Konzeption von CSP-CASL

Markus Roggenbach

Unter der Rubrik

"Schnellschüsse" (Diskussionsbeiträge über laufende Arbeit)

möchte ich im Rahmen des Extra-Treffens erste Schritte auf dem Weg zu einer Kombination der Spezifiationssprachen CASL und CSP vorstellen. CSP-CASL soll es ermöglichen, in einem Formalismus sowohl über Datentypen als auch über parallele Systeme reden und Beweise führen zu können.

Für CASL haben Kolyang und Till eine Codierung in Isabelle/HOL vorgenommen, Haykal und Burkhart habe CSP in Isabelle/HOL codiert. Die Konzeption von CSP-CASL soll die theoretische Grundlage zur Integration dieser Codierungen schaffen.

• 10.12.99
Combining Methods for the Analysis of a Fault-Tolerant System

Shi Hui

This paper presents experiences gained from the verification of a large-scale real-world embedded system by means of formal methods. This industrial verification project was performed for a fault-tolerant system designed and implemented by DaimlerChrysler Aerospace for the International Space Station ISS. The verification involved various aspects of system correctness, like deadlock and livelock analysis, correct protocol implementation, etc. The approach is based on CSP specifications and uses the model-checking tool FDR. It is realized by combining methods for the development as well as for the analysis. It is illustrated by examples and results obtained during the verification of the Byzantine agreement protocol implementation, where the combination of different abstraction methods is required.

• 19.11.99
Bericht von der World Conference on Formal Methods FM'99

Bettina Buth, Bernd Krieg-Brücker, Christoph Lüth, Oliver Meyer, Till Mossakoswsi

Collected impressions from the mother of all formal method conferences FM'99 in Toulouse.

• 05.11.99
LEPLAS - Konzeption und didaktische Erfahrungen mit einen Softwaretechnik-Praktikum

Burkhart Wolff (Albert-Ludwigs Universität Freiburg)

LEPLAS ist ein Lehrplanungssystem für eine Universität, das von Studenten im Rahmen eines Softwaretechnik-Praktikums entworfen, formal spezifiziert und teilweise implementiert wird. Diese recht komplexe Übung wurde bereits zweimal an der Albert-Ludwigs-Universität Freiburg mit jeweils ca 20 - 30 Studenten durchgeführt.

• 29.10.99
Eine Spezifikation von reellen Zahlen CASL

Markus Roggenbach und Till Mossakowski

There seem to be two obstacles to specify real numbers within a first order logic: As the real numbers are not countable, they can not be specified as a monomorphic datatype due to the theorem of Loewenheim and Skolem. Furtheron the common axiomatizations and constructions of the real numbers use higher-order concepts. As a consequence, first order algebraic specification languages do either not provide a datatype corresponding to the real numbers or have only a specification of a floating point system as basic datatype. Both solutions are unsatisfactory: The first leaves a great deal of applications out of scope. The second is of course better, but nevertheless problematic: It forces a specifier to deal with implemention details even on the level of a requirement specifications, and the development of numerical algorithms can not be described.

In this talk Markus will present a weak axiomatization BasicReal of the real numbers in the first order specification language CASL. This axiomatization allows to study concepts like continuity, derivability, and integrabiblity of functions, and it is suitable to study numerical algorithms.

After that, Till will give an overview over different possible axiomatizations of (fragments) of set theory in CASL, namely: ZFC, VNBG (von Neumann-Bernays-Goedel), and higher-order CASL.