EXTRA-Treffen Archiv WS 96/97

21. März
          Bericht über ESPRESS-Workshop in Berlin (24./25.Febr)
          Fachgruppentreffen Test, Analyse + Verifikation von Software
          (6./7.Maerz)

          Peter Amthor, Sabine Dick, Kolyang


7. Maerz

          An Overview of Corba/ILU

          Einar Karlsen

        The Corba (Common Object Broker Request Architecture) has
        become the standard for achieving interoperability between
        programs written in different languages (C,C++,Lisp,Python,
        Java...) running on different kind of platforms (Unix,
        MSWindows ...). It works according to the client/server
        paradigm. Tool interfaces are defined in IDL/ISL (Interface
        Definition Language,Interface Specification Language). ILU
        generates the needed client stubs and server skeletons
        and provide the necessary runtime system to establish RPC.
        A client written in Lisp may then call services provided by
        a server written in C++ (say).


28.Februar

          Axiomatische Klassen in Isabelle(/HOL)

          Burkhart Wolff

       Das Konzept von Typklassen ist von Haskell her wohlbekannt.
       Eine Klasse ist eine Art Menge von Typen, die gewisse
       Einschränkungen erfüllen müssen (Haskell:
       gewisse Operationen mit gewissen Signaturen  müssen definiert
        sein).

       In Isabelle gibt's Typklassen auch, hier kann man ihnen aber
       noch eine zusätzliche semantische und beweistechnische
       Bedeutung geben. Man kann z.B. Gruppen oder CPO's als Klassen
       auffassen, wobei nicht nur die Existenz von passenden
       Signaturelementen erzwungen wird, sondern auch ganz handfeste
       Eigenschaften (Kommutativität auf dem Plus).


21.Februar
          Realzeitverifikation mittels partieller Ordnungen

          (Wdh. des Vortrages aus dem Informatik-Kolloquium
          für alle, die den Termin nicht wahrnehmen konnten.)

          Holger Schlingloff

        In diesem Vortrag wird zunächst ein kurzer Überblick
        über verschiedene Modelle und Logiken für
        Realzeitsysteme gegeben. Danach präsentiere ich einen
        effizienten Modellprüfungsalgorithmus für elementare
        Petrinetze und eine zeitabhängige temporale Logik. Der
        Algorithmus ist eine Realzeit-Erweiterung des als ``stubborn
        set method'' bekannt gewordenen Ansatzes. Es wird die kausale
        Unabhängigkeit paralleler Teilkomponenten dazu ausgenutzt,
        den zu traversierenden Zustandsraum zu verringern. Eine
        Schaltfolge kann als partielle Ordnung aufgefasst werden, die
        durch die Topologie des Netzes und die gegebene Formel bestimmt
         wird. Jede solche partielle Ordnung bestimmt eine Menge von
        linearen Ordnungen, nämlich all diejenigen Sequenzen, die
        sich aus der partiellen Ordnung durch Interleaving erzeugen
        lassen. Zur Bestimmung des Wahrheitswertes einer Formel der
        linearen temporalen Aussagenlogik genügt es im
        allgemeinen, nur einige wenige dieser vielen möglichen
        Sequentialisierungen zu betrachten. Für hochgradig
        parallele Applikationen gelingt es damit, die
        Durchschnittskomplexität des Verifikationsproblems
        entscheidend zu verringern.



7. Februar:
         Ein Kalkül zur Compilergenerierung

          Besma Abd Moulah

        In den meisten Implementierungen der polymorphen Sprachen werden Typen
        nicht in allen Phasen voll ausgenutzt. Dies wird hauptsächlich
        durch die größere Komplexität der Typen relativ
        zu den monomorphen Typsystemen bedingt. Um dieses Problem zu
        überwinden, stellt der Lambda(_i^ML)-Kalkül einen
        formalen Rahmen dar, der typbewahrende Transformationen
        unterstützt. Mit den Typinformationen läßt sich die
        Korrektheit aller Kompilationsschritte von der Quellsprache bis zur
        Low-Level-Zielsprache beweisen.


13. Januar:
          Eta-Expansions in Type Theory

          Neil Ghani, Ecole Normale Superieur

   The use of expansionary eta-rewrite rules in various typed lambda
   calculi has become increasingly common in recent years as their
   advantages over contractive eta-rewrite rules have become apparent. In
   particular, rewrite relations using expansions retain key properties
   when combined with first order rewrite systems, generalise more easily
   to other type constructors and are supported by a categorical theory
   of reduction. My talk will be a survey of the subject and will justify
   these claims.



10. Januar
          Chu spaces as models of parallel systems

      Rait Harnett, University of Capetown, South Africa

   Labelled, partially ordered sets are often used to describe the
   behavioural or operational semantics of parallel systems.  Vaughan
   Pratt and his student Gupta, using Chu spaces, have extended the idea
   of a partially ordered set describing the behaviour of a system.
   Following them, we will show how a specification of a parallel system
   given statically as a Chu space can be interpreted dynamically as

      an automaton, or
      a schedule, whose underlying structure is not just a partially
           ordered set, but  a lattice generated by the events the system may
           engage.

   The automaton and schedule associated with a Chu space are dual to each
   other, i.e., one can be recovered from the other.
   If time allows, we will briefly sketch how we are using Chu spaces to
   give Statecharts a denotational semantics.


12. Dezember
       Testfallerzeugung aus Z-Spezifikationen mit Isabelle

          Thomas Santen, GMD FIRST Berlin

   Neben der größeren Präzision in der Beschreibung von
   Anforderungen
   an ein Softwaresystem ermöglichen formale Spezifikationen eine
   weitergehende Maschinenunterstützung des
   Softwareentwicklungsprozesses, als das mit klassischen Methoden
   möglich ist.  Die Automatisierung von Testaktivitäten ist aus der
   Sicht der Praxis ein lohnendes Ziel, weil der zum Testen benötigte
   Aufwand heute einen großen Teil der Gesamtkosten eines
   Softwaresystems, insbesondere für sicherheitskritische Anwendungen,
   ausmacht.

   Der Vortrag konzentriert sich auf den Test von Datentransformationen,
   die mit der Spezifikationssprache Z spezifiziert sind. Nach einer
   kurzen Einführung in die Terminologie wird gezeigt, wie sich
   verschiedene Testaufgaben als Beweisprobleme auffassen lassen.  Der
   Hauptteil des Vortrags behandelt die Erzeugung von Testfällen für
   Einzeloperationen aus einer Z Spezifikation. Die grundlegende, aus der
   Literatur bekannte Idee ist die Transformation des
   Ein-/Ausgabeprädikats einer Operation in eine disjunktive Normalform,
   deren Glieder sich als Testfälle auffassen lassen. Die erzeugten
   Fälle sollen dabei erfüllbar und redundanzfrei sein.

   Auf der Basis der in Kooperation der GMD mit der Universität
   Bremen
   entwickelten Repräsentation von Z im Beweiser Isabelle wurde an der
   GMD eine solche Transformation entwickelt. Die Grundzüge des
   Algorithmus werden vorgestellt, wobei besonders auf die Eigenschaften
   des Beweisers und der Z-Repäsentation eingegangen wird, die es
   erlauben, mit geringem Aufwand eine vertrauenswürdige und effiziente
   Implementierung zu realisieren.

29. November:
       Disjunktive logische Programmierung mit Constraints und ihre Anwendung

       Frieder Stolzenburg, Universität Koblenz

       Die Constraint-Logikprogrammierung verbindet Hornklausellogik mit dem
       Constraint-Schließen. Doch die Spezifikation vieler
       Problemstellungen erfordert oft zusätzlich disjunktive, d.h.
       Nicht-Horn-Regeln. Hier soll ein Verfahren vorgestellt werden, das
       sich gut für eine Implementation eignet: die
       Constraint-Modellelimination. Dieser
       Kalkül basiert auf der Modellelimination und läßt
       sich gut für die (positive) Disjunktive Logische Programmierung
       mit Constraints einsetzen, und damit allgemein fuer die schnelle
       Erstellung von Software.

       Die Grundidee dabei ist es, den Logik-Anteil einer Problembeschreibung
       nach Prolog zu compilieren und beim Lösen der Constraints auf
       vorhandene Constraint-Verfahren aufzusetzen. Beides ist
       zusammengeschlossen im Protein-System, entwickelt an der Universität
       Koblenz. Eine Reihe von Anwendungen sind bereits untersucht worden. Im
       Vortrag soll insbesondere auf die Analyse von Regelwerken zur Berech-
       nung von Gebühren eingegangen werden.


22. November:
       Methodenkombination bei der Verifikation des
              DASA FTC Fault-Management Layers

       Prof. Jan Peleska, Dr. Buth, Dr. Shi

       FTC ist die Bezeichnung eines 4-fach redundante
       fehlertoleranten Systems, welches von der DASA als
       zentrale  Vermittlungskomponente zwischen Sensoren und
       Applikationen zur Steuerung von Experimenten in der
       DMS-R Raumstation entwickelt wurde.  Das in OCCAM
       implementierte  Fault-Management
       Layer (ca 11000 Zeilen OCCAM Code)
       und das Avionics Interface wurden bisher von uns
       bzgl. Deadlock-Freiheit verifiziert.  Hierzu wurde eine
       Kombination von Methoden auf der Grundlage von CSP
       eingesetzt:

                 (1) Theorem Proving mit der kompositionellen
                    Beweistheorie
                 (2) Abstrakte Interpretation
                 (3) Model Checking.

       Wir stellen das Verifikationskonzept vor
       und geben Beispiele fuer die konkrete Vorgehensweise.



15. November:
        Ausführbare Spezifikationen in HOL

        Burkhart Wolff

        HOL ist eine klassische Logik hoeherer Stufe, in der
        zunächst mal kein irgendwie gearteter Berechenbarkeitsbegriff
        angelegt ist.  Es stellt sich die Frage, wie Programme in HOL
        dargestellt werden koennen.

        Die Problematik ist hoechst unoriginell (siehe alle möglichen
        Ansätze in algebr. Spezifikation), und doch dringlich
        (schliesslich wollen wir ja im Transformationssystem Spezifikationen
        erzeugen, aus denen richtiger Code gemacht wird).

        Nach der Diskussion einiger Schieflaeufer und ad-hoc Loesungen
        werde ich einen Vorschlag fuer Isabelle/HOL machen, der sich auf die
        Theorie der wohlfundierten Rekursoren stützt und das aber nett
        verpackt.


1. November:
       Model-Checking und Prozesstransformation in CSP

       Dr. Hui Shi, Haykal Tej

       Stichworte:
          -  CSP
          -  Verfeinerungsrelation und Model-Checking
          -  Prozessentwicklung durch Transformation (Idee und Beispiele)


18. Oktober:
      (Integrierte) formale Entwicklungsumgebung für Z in Isabelle

      Kolyang

      In der Welt der formalen Methoden, nimmt die Spezifikationssprache Z
      einen wichtigen Platz ein. Der Vortrag wird hauptsächlich zwei
      Schwerpunkte haben.

          -  Eine strukturerhaltende Einbettung von Z in Isabelle.
             Details über die Einbettungsidee, die Beschreibung der
             Theorien usw. werden vorgestellt.
          -  Eine starke Beweisunterstützung. Theoreme aus Isabelle
             werden zu Z-Schema spezifischen Prädikaten. Isabelle
             Taktiken werden entsprechend fuer Z aufgearbeitet.
             Dadurch erhält die Einbettung die Mächtigkeit der
             Isabelle Beweisumgebung.

      Die Integration dieser Einbettung in eine Umgebung, wie die eines
      Transformationsanwendungs- oder -entwicklungssystems (TAS), wird
      skizziert.


27. September:

      Ein Paradigma für Spezifikation, Design und Verifikation zuverlässiger
      Systeme mit kombinierten Methoden

      Jan Peleska

          Bezug zum Development Manager
          Bezug zum V-Modell
          Beispiele für Instantiierungen des Paradigmas mit konkreten Methoden


20. September, Peter Amthor:

       Entwicklung und Implementierung einer Verifikationskomponente
       für SDL

       Im Bereich Theoretische Informatik der Universität Oldenburg wird
       ein System zur Verifikation und Simulation von SDL-Spezifikationen
       entwickelt. In diesem System ist es möglich, SDL-Diagramme zu
       editieren, welche dann in M-Netze (High-Level Petrinetze) und in
       Petriboxen (Low-Level Petrinetze) übersetzt werden können.
       Simulation ist auf M-Netz- und Petribox-Ebene möglich.

       Der Beitrag dieser Diplomarbeit ist die Bereitstellung einer Temporalen
       Logik für SDL, um Eigenschaften von SDL-Diagrammen verifizieren zu
       können. Zur Erreichung dieses Zieles wird ein Modelchecking-Algo-
       rithmus für Petriboxen genutzt, der an der Universität
       Hildesheim implementiert wurde. Mit Hilfe der Logik können nun
       SDL-Formeln kreiert werden, mit denen man Eigenschaften von SDL-Diagram-
       men beschreibt. Die SDL-Formeln werden dann in Petriboxformeln
       übersetzt, die man mit dem Modelchecker überprüft.
       Das vom Modelchecker zurückgelieferte Ergebnis für eine
       Petriboxformel ist so auch für die zugehörige SDL-Formel
       gültig.



13. September, Christoph Lüth:

       Konferenzbericht

       7th Intern. Conf. on Rewriting Techniques and Applications (RTA)/

       IEEE Symposium on Logic in Computer Science (LICS),

       im Rahmen der Federated Logic Conference (FLoC)

       26.Juli bis 3.August, Rutgers University, New Jersey, USA