EXTRA-Treffen Archiv WS 97/98 and SS 98
- 24.07.98
Markus Roggenbach (Uni Mannheim)
Bisimulation wird von Milner [Mil80] und Park [Park81] auf Transitionssystemen eingeführt, um Prozesse zu identifizieren, die aus Sicht eines externen Beobachters nicht zu unterscheiden sind. In der Theorie paralleler Systeme gewinnt dieser Begriff als Abstraktionsmechanismus große Bedeutung und wird auch auf andere Modelle parallelen Rechnens wie Petri Netze, Ereignisstrukturen, Transitionssysteme mit Unabhängigkeit übertragen. Angesichts der so entstandenen Vielzahl von unterschiedlichen Bisimulationen stellt sich die Frage nach einem gemeinsamen Überbegriff, nach einer abstrakten Charakterisierung von Bisimulation.
Der Vortrag diskutiert verschiedene abstrakte Charakterisierungen von Bisimulation. Dazu wird zunächst der Begriff der Bisimulation an Hand von Beispielen motiviert und illustriert. Anschließend werden verschiedene abstrakte Charakterisierungen von Bisimulation eingeführt und miteinander verglichen. Diese Gegenüberstellung führt zu dem Schluß, daß das Konzept der AM-Bisimulation von den untersuchten Charakterisierungen am umfassendsten und flexibelsten ist.
[Mil80] Robin Miler. A calculus of communicating systems, Springer
LNCS 92, 1980.
[Park81] David Park. Concurrency and automata on infinite sequences,
Springer LNCS 104, 1981.
Vorträge bisher (WS '97/98, SoSe 98)
- 16.07.98
- 22.04.98
- Einmal wird aus komplexitätstheoretischer Sicht untersucht, warum das
Wiederverwenden von Plänen nicht die Effizienzgewinne für
Planungssysteme erbringen kann, die man sich ursprünglich erhoffte.
- Zum anderen wird anhand eines konkreten Planungssystems vorgestellt, daß bestimmte Wiederverwendungstechniken trotz der äußerst kritischen komplexitätstheoretischen Ergebnisse sinnvoll und erfolgreich eingesetzt werden können.
- 13.03.98
Eine Funktionale Modulsprache Andreas Rossberg (Universität Braunschweig)
Die wesentlichen Elemente des Programmierens-im-Grossen sind Module, Komponenten, und ihre Schnittstellen. Betrachtet man Module als elementare Werte und ihre Schnittstellen als elementare Typen, so kann das Programmieren-im-Grossen als typisiertes, funktionales Programmieren aufgefasst werden: die Komponenten eines Programmsystems sind Funktionen, die über die benötigten Module oder Komponenten parametrisiert sind. Durch Anwendung solcher Funktionen kann ein - den jeweiligen Anforderungen entsprechend konfiguriertes - System Schicht für Schicht generiert und integriert werden. Die Sprache M verwirklicht diese Idee in Form einer referentiell transparenten, d.h. rein applikativen Programmiersprache höherer Ordnung. M-Quelltexte sind ausführbare Beschreibungen einer Software-Architektur, das Ergebnis ihrer Ausführung ist konzeptionell ein lauffähig montiertes, garantiert konsistentes Programm.
- 06.03.98
Visualisierung von Prozeßgraphen für CSP ohne Zeit Sabine Dick
Für ein Arbeiten und Entwickeln mit Prozeßspezifikationen in CSP sind Visualisierungen verschiedener Art nützlich, um insbesondere Werkzeuge und ihre Verwendung zu unterstützen.
Vorgestellt werden Prozeßgraphen, die die Untersuchung nicht zeitbehafteter Eigenschaften erlauben und sich insbesondere als Hilfsmittel für die Deadlock-Analyse eignen. Mit Hilfe von Datenflußgraphen lassen sich potentielle Kommunikationsabhängigkeiten zwischen Prozessen syntaktisch aus FDR-Definitionsfiles feststellen. Im Rahmen von UniForM ist hierfür eine erste Toolversion entstanden, die vorgeführt wird. Die Darstellung der Graphen erfolgt mit Hilfe von daVinci. Eine Anschlußmöglichkeit der Visualisierung von CSP-Prozessen steht über eine abstrakte Syntax bereit.
- 27.02.98
Development of a Fail-Safe Data Transceiver for use in Safety-Critical Environment Micheal Schronen
It is essential that data transmission between safe systems, in distributed safety-critical applications occurs in a safe manner. To date this safe data transmission has generally been in a parallel form. In some applications e.g. railway interlocking where the geographical area is large the resulting cabling and labour costs have made this method of data transfer expensive.
This talk will focus on the development of low cost, serial, microprocessor based Fail Safe Data Transmission System (FSDTS) which can be used in these safety-critical applications. Topics covered will include: background into the project, error control strategies for serial transmission, system and hardware safety techniques when using microprocessors, calculating hardware safety, the design of a Fail-Safe Data Transceiver (FSDT), testing, future work involving verification using formal methods.
- 20.02.98:
Bericht über die AMAST'97 Bettina Buth
- 13.02.98:
Codeerzeugung in Isabelle/HOL Thomas Meyer
Eine wichtige Motivation für Theorembeweiser ist die Entwicklung von verifizierten Programmen. Techniken zur transformationellen Programmentwicklung enden mit einer formalisierten Übersetzung von Spezifikationen in eine Formel, die einem bestimmten Programmausführungsbegriff genügt. In diesem Vortrag werden drei Programmausführungsbegriffe, die auf drei verschiedenen Rekursionsformen basieren, und deren Formalisierungen in Isabelle/HOL vorgestellt. Diese Formalisierungen dienen als semantische Schnittstelle zu einem generischen Code-Generator.
- 30.01.98:
Generic Graphical User Interfaces -- The Next Generation. Christoph Lüth
Eine der Besonderheiten der graphischen Benutzeroberfläche für das Transformationssystem und Isabelle ist seine generische Systemarchitektur: im wesentlichen ist die graphische Benutzeroberfläache ein SML-Funktor, der für verschiedene Applikationen instantiiert werden kann. Wir werden in diesem Vortrag die Grundprinzipien des Designs noch einmal kurz vorstellen, und insbesondere die Schwierigkeiten diskutieren, die sich ergeben, wenn man dieses Design so erweitert, daß zu jedem Zeitpunkt die Oberfläche rekonstruierbar ist (Persistenz), und auf die dynamische Veränderung externer Objekte (z.B. Isabelle-Theorien) reagiert werden kann (Dynamisierung).
- 19.12.1997:
HOL-CSP. Haykal Tej
Dieser Vortrag gibt eine allgemeinverständliche Einführung in die Kodierung von CSP in Isabelle/HOL.
- 08.12.1997:
Monads & Modularity -- An Introduction to Categorical Rewriting. Christoph Lüth
Term rewriting systems are widely used throughout computer science as they provide an abstract model of computation while retaining a comparatively simple syntax and semantics. A particularly interesting question is the modularity of properties: if two term rewriting systems satisfy a certain property, then does their disjoint union? Motivated by the treatment of universal algebra in category theory, we propose a new semantics for term rewriting systems, based on the concept of an enriched monad. We show how this semantics can be used to prove modularity results in a more elegant way, slightly generalizing some results from the literature.
- 05.12.1997:
The UniForM User Interaction Manager Einar W. Karlsen
The UniForM User Interaction Manager (UIM) provides presentation integration facilities within the UniForM WorkBench - a tool integration framework in Concurrent Haskell. The UIM consist of 3 components: a concurrent encapsulation of Tk, an encapsulation of the graph visualization system daVinci, as well as a Haskell interface to the World-Wide-Web. Notable features of the UIM are its support for concurrency, its higher order approach to event handling and the degree of composability offered.
- 28.11.1997:
Static and Semantic Analysis of CASL Kolyang
This talk presents a static and semantic analysis of CASL. Represented in the higher-order logical framework of Isabelle, the embedding yields abstract syntax trees, that are readed for a static-semantic check. Furthermore, an overload resolution algorithm is implemented that takes the resulting abstract trees and yields CASL fully qualified abstract trees.
At the end, a schematic overall architecture of the embedding of CASL in a logical framework, using thus all facilities given by a generic theorem prover, is presented.
Discussions should go in the directions of integrating HOL-CASL in the UniForM Workbench (no clear ideas here!)
This is joint work with T. Mossakowski and B. Krieg-Brückner. - 31.10. und 7.11.1997:
Bericht über die FME'97 Haykal Tej, Burkhart Wolff, Christoph Lüth
- 17.10. und 24.10.97:
Bericht über das 7. Kolloquium
Software-Entwicklung-Methoden-Werkzeuge, Erfahrungen '97 Peter Amthor, Sabine Dick
Besma Abd Moulah und Kolyang
Formale Methoden gewinnen mehr und mehr an Bedeutung, auch für grössere industrielle Anwendungen. Ihre Akezeptanz ruht aber vor allem auf der Verfügbarkeit von Werkzeugen, die sie im Softwareentwicklungsprozess begleiten. Eine dieser Methoden ist B, die alle Entwicklungsphasen (von der Spezifikation bis zum Code) unterstützt. Eine Realisierung von B ist das Werkzeug Atelier B. Anhand eines kurzen Beispieles wird Atelier B vorgeführt. Am Ende des Vortrages sollen eine mögliche Kombination zwischen Z und B und eine mögliche Integration von B in der UniForM Workbench diskutiert werden.
Jana Köhler (Uni Freiburg)
Das Erzeugen von Plänen wie zum Beispiel Handlungsplänen für autonome intelligente Systeme oder Beweisplänen zur Steuerung von Deduktionssystemen ist ein außerordentlich komplexer Prozeß. Zu Beginn der 90er Jahre begann man deshalb, sich verstärkt mit der Wiederverwendung bereits generierter Pläne zu beschäftigen in der Hoffnung, ähnliche Planungsprobleme auf einfachere Weise durch die Wiederverwendung und Modifizierung von vorhandenen Plänen zu lösen.
Der Vortrag betrachtet das Wiederverwendungsproblem aus zwei verschiedenen Perspektiven:
Autor: n/a
| Zuletzt geändert am: 30. August 2002 |  |