EXTRA-Treffen Archiv WS 99/00 und SS 00

Bisheriges Program (SS'01)

• 23.03.2001

  Secrecy
  Jan Jürjens

  We present a notion of secrecy (following the standard approach of Dolev and Yao (1983)) in a formal model which is preserved under refinement and composable. Both these properties are considered to be useful and are notoriously difficult to achieve for security properties (``refinement paradox''). As an example for a use of this notion, we analyse a variant of the Internet security protocol TLS (current successor of SSL) proposed at INFCOM'99, uncovering a previously unpublished flaw.

  In ongoing work, we aim to transfer our concepts to the setting of Casl-Chart (a recent extension of Casl to reactive systems using statecharts).

  
  
  
• 23.02.2001

  Erzeugen von Diagrammeditoren mit DIAGEN.
  Berthold Hoffmann

  In diesem Vortrag will ich einen Überblick über ein System geben, das mein Lieblings-Koautor Mark Minas (Univ. Erlangen) entwickelt und das die Grundlage für unsere künftigen gemeinsame Arbeiten sein soll.

  In DIAGEN können Diagrammsprachen mit Graphen, kontextfreien Graphgrammatiken und Graphtransformationen spefifiziert werden, so dass automatisch Editoren für diese Sprachen erzeugt werden konnen. Die Editoren erlauben sowohl freies als auch strukturiertes Editieren, geben sinnvolle Fehlemeldungen und bauen eine anzugebende semantische Darstellung auf, die meistens textuell ist und von anderen Werkzeugen weiter verarbeitet werden kann. Das Layout von Diagrammen kann entweder mit constraints spezifiziert oder über eine Programmier-Schnittstelle von Hand programmiert werden.

  Mit DIAGEN lassen sich praktisch beliebige Diagrammsprachen bearbeiten, wie z.B. Nassi-Shneiderman-Diagramme, Statecharts, UML-Klassendiagramme und viele mehr.

  Mark Minas und ich wollen DIAGEN um eine visuelle regelbasierte Sprache, DIAPLAN, erweitern, mit der sich die Semantik von Diagrammen, z. B. die Animation von Statecharts oder die Transformation von Klassendiagrammen direkt programmieren lassen.

  
  
  
• 02.02.2001

  An introduction to Computational Monads
  Christoph Lüth

  Der Vortrag wird eine allgemein verständlich gehaltene Einführung in die Theorie der Monaden, insbesondere Moggi's Computational Monads, und die Praxis ihrer Verwendung in Haskell. Vorkenntnisse in Kategorientheorie sind nicht erforderlich. Wer sich schon immer gewundert hat, was ist eigentlich ein Monad, was hat es in meinem Haskell-Programm zu suchen, und wieso kann ich Zustände damit modellieren, ist bei diesem Vortrag richtig.

  Eines der Ziele des Vortrages ist es, eine Diskussion darüber anzustoßen, inwieweit Monaden in CASL zur Spezifikation von zustandsbehafteten Programmen benutzt werden können. Darauf werde ich allerdings in dem Vortrag selber nur dann eingehen, wenn dazu auch Zeit bleibt.