EXTRA-Treffen Archiv WS 98/99 und SS 99
Vorträge bisher (SS99, WS '98/99)
- 18.06.99
- 25.06.99
- 02.07.99
- Graphstrukturierung (hierarchische Graphen)
- funktionale Abstraktion (Graphprozeduren)
- Datenabstraktion (Graphklassen)
- 11.06.99
- 21.05.99
- The role of the semantics in the design process of CASL
- Why and where is the CASL semantics needed?
- The style of the rules of the CASL semantics
- Example rules of the CASL semantics
- Institution independence of the semantics of CASL-in-the-large
- 23.04.99
- 09.04.99
- 16.04.99
- Hybrid modelling & simulation
- Object-orientation and reactive programming
- Synchronous Programming
- Distribution of Reactive Programs
- Model-checking
- Tool certification and code validation
- 12.03.99
- 05.03.99
- 26.02.99
- 12.02.99
- A1: algebraic techniques are used at the metalevel
- A2: a concurrent specification language is complemented with the possibility of abstractly specifying the (static) data
- A3: algebraic specifications having ¨dynamic sorts¨
- A4:abstract data types which change along time
- 05.02.99
- 15.01.99:
Bericht von der 11. Internationalen Konferenz der Z-Benutzer ZUM'98 Christoph Lüth
Die ZUM ist die zentrale Konferenz für alle Z-Benutzer, Entwickler (insbesondere von Tools) und Interessierte; diese Konferenz gibt deshalb einen repräsentativen Eindruck vom Stand der Kunst auf diesem Gebiet.
Lutz Schröder
Überraschend häufig begegnet man in der Mathematik Strukturen, die schwächer sind als Kategorien in dem Sinne, daß die Komponierbarkeit von Morphismen nur eingschränkt gegeben oder gar etwa das Assoziativgesetz verletzt ist. Beispiele sind einerseits "schlechte Konstrukte", d.h. Ansammlungen strukturierter Mengen (etwa Wahrscheinlichkeitsräume) mit nicht kompositionsstabilen Morphismen, andererseits auch "naiv" gebildete Quotienten von Kategorien. Ferner dienen solche Strukturen als Systeme von Erzeugenden und Relationen für Kategorien.
Ein Formalisierungsansatz für dieses Phänomen ist der Begriff des Kompositionsgraphen, d.h. eines Graphen mit einer partiellen Komposition, die einzig dem Axiom genügt, daß komponierbare Paare kommutative Dreiecke ergeben; die Bedeutung weiterer Axiome, insbesondere verschiedener Assoziativ- und Identitätsgesetze, wird dann im einzelnen untersucht. Ein Hauptaspekt bei der weiteren Nachforschung ist die Frage, welche Teile der Kategorientheorie sich in diesen allgemeineren Kontext übertragen lassen; es zeigt sich hierbei, daß sich insbesondere für die Begriffe "natürliche Transformation", "natürlicher Isomorphismus", "adjungierter Funktor" und "Äquivalenz" Verallgemeinerungen angeben lassen, die sich anhand damit verbundener Resultate als die "richtigen" Definitionen darstellen.
Berthold Hoffmann
Mit Graphtransformationen lässt sich das Verhalten von Systemen spezifizieren, insbesondere wenn diese Systeme interaktiv sind und graphisch sind.
Im Vortrag geht es um Ideen, das Konzept der Graphtransformation zu einer vollständigen visuellen Spezifikations- und Programmiersprache weiter zu entwickeln.
Im Vordergrund stehen Überlegungen zu folgenden Aspekten:
Christoph Lüth
In den letzten Jahren sind sog. coalgebraische Methoden immer öfter in Erscheinung getreten, als genereller Rahmen für Bisimulationen (Co-Induktion), als Semantik für unendliche Datentypen (Listen/Streams) oder auch im Zusammenhang mit "hiding" und beobachtbarer oder Verhaltensgleichheit.
In diesem Vortrag würde ich gerne zeigen, wie man Coalgebra als einfache Dualisierung von Algebra erhält, indem man die Äquivalenz von Algebra und Monaden ausnutzt, und in der Basiskategorie des Monaden einfach alle Pfeile umdreht. Etwas allgemeiner können wir induktive Datentypen als kleinste Fixpunkte und initiale Algebren betrachten; der entsprechende duale Begriff ist der größte Fixpunkt und terminale Algebren. Ich werde versuchen, diese Begriffe alle in einen allgemeinen Rahmen zu bringen, zu zeigen, wie man coalgebraische Methoden als einfache und systematische Dualisierung von algebraischen Methoden erhält, und mit Beispielen zu zeigen, wozu all dieses nützlich sein kann.
Till Mossakowski
CASL is a language that has been designed in a collaborative effort with the goal to achieve a standard in the area of specification languages. An important aspect of CASL is that it has a complete mathematical semantics. In this talk, I will present some aspects of the CASL semantics:
More about CASL and the Common Framework Initiative.
Christoph Lüth.
The European Joint Conferences on Theory and Practice of Software ETAPS'99 bill themselves as
the new European forum for academic and industrial researchers working on topics relating to Software Science. During 8 days, ETAPS will give you the opportunity to choose between more than 100 regular papers covering a wide range of topics from Theory to Practice, 7 invited lectures, 6 tutorials, and 5 satellite events offering dozens more talks!I shall endeavour to truthfully report on this extravaganza.
Björn Gottfried
Es wird der Roboter-Simulator ROSI und das Forschungsprojekt Integration Kognitiver Systeme an der FH-Hamburg beschrieben, in dem es um den Bau autonomer mobiler Roboter geht.
Aufgrund der Bedeutung der Wahrnehmung bei mobilen Robotern werden einige Aspekte der Robotik aus der Perspektive der Wahrnehmungspsychologie beschrieben.
Peter Amthor
The talk is about two conferences I visited recently and shall give an overview accompanied by several more detailed remarks to certain contributions.
Till Mossakowski
Motivation:
Bei dem Einsatz formaler Methoden zur Entwicklung korrekter Software, insbesondere bei großen Softwareentwicklungsprojekten, an denen viele Personen und möglicherweise auch mehrere Entwicklungsteams beteiligt sind, kann man nicht davon ausgehen, das eine einzige formale Spezifikationssprache mit einer einheitlichen Entwicklungsumgebung zum Einsatz kommt. Für verschiedene Zwecke werden von unterschiedlichen Beteiligten 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.
Inhalte:
Was ist eine Logik? Formalisierung des Begriffs
Logik-unabhängige Spezifiktionssprachen
Zwei Typen von Abbildungen zwischen Logiken: Repräsentation und
Projektion/Kombination
"Ausleihen" von Theorembeweisern
Heterogene Spezifikationssprachen (basierend auf einem Logik-Graph)
Holger Schlingloff
Christoph Lüth
Der pi-Kalkül ist ein auf Robin Milner, David Walker und Joachim Parrow zurückgehender Kalkül zur Studie der Theorie von nebenläufigen Prozessen. Der pi-Kalkül soll dabei weniger eine weitere Spezifikationssprache für nebenläufige Systeme à la CSP oder CCS sein, sondern vielmehr ein grundlegender Kalkül zur Modellierung dieser Systeme (wie der lambda-Kalkül für sequentielle Programme) wobei die Benennung von Prozessen die grundlegende Operation ist.
Mein Vortrag gründet sich im wesentlichen auf Robin's Papier The Polyadic pi-Calculus: a Tutorial. Ich werde den einfachen (monadischen) pi-Kalkül vorstellen, die Erweiterung zum polyadischen pi-Kalkül sowie Sorting und higher-order, und die Verbindungen zu linearer Logik skizzieren.
Markus Roggenbach
Der Vortrag beruht auf dem Kapitel
E.Astesiano, M.Broy, G.Reggio:aus dem IFIP Buch
Algebraic Specification of Concurrent Systems
Astesiono, Kreowski, Krieg-Brückner (eds):Dieses Kapitel stellt Methoden zusammen, die es erlauben, sowohl nebenläufige als auch algebraische Aspekte eines Systems zu spezifizieren. Die AutorInnen ordnen die Spezifikationsmethoden in vier Gruppen:
Algebraic Foundations of Systems Specification.
Für den Vortrag habe ich aus der Vielzahl der vorgestellten Methoden für jede dieser Gruppen eine repräsentative ausgewählt. Dies sind im einzelnen CCS (A1), Lotos (A2), Labelled Transition Logic (A3) und Evolving Algebras (A4). An einem einfachen Musterbeispiel will ich sowohl die Möglichkeiten als auch die Grenzen dieser Spezifikationsmethoden aufzeigen. Dabei hoffe ich auf eine intensive Diskussion mit Euch, was an den verschiedenen Methoden überzeugt, aber auch darüber, an welchen Stellen sie ¨verbesserungswürdig¨ sind.
Till Mossakowski
CASL (The Common Algebraic Specification Language) ist eine Sprache zur Spezifikation von Datyentypen, die Logik erster Stufe, partielle Funktionen und Untersorten kombiniert. In dieser Arbeit wird CASL mit Funktionen und Prädikaten höherer Stufe verallgemeinert. Dies ist insbesondere wichtig, um funktionale Programme, die oft mit höheren Funktionen arbeiten, spezifizieren zu können.
Die Kombination von Partialität, Untersorten und höheren Funktionen wird schrittweise über eine Reduktion auf den jeweils vorhergehenden Schritt eingeführt. Durch diese modulare Vorgehensweise kann die Interaktion verschiedener Features besser in den Griff bekommen werden. Verschiedene Entwurfsalternativen werden u.a. unter dem Aspekt einer treuen Einbettung von CASL nach higher-order CASL diskutiert.
(In Zusammenarbeit mit Anne Haxthausen und Bernd Krieg-Brückner)
Autor: n/a
| Zuletzt geändert am: 30. August 2002 |  |