University of Freiburg | Faculty of Applied Sciences | Institute for Computer Science | Computer Networks and Telematics
The tele Research Group
Home         Teaching         Research        Tools         Openings        Publications





Computer Networks and Telematics


Prof. Dr. Stefan Leue
Dr. Richard Mayr

Winter Term 2003


  • Einladung zum Oberseminar der Arbeitsgruppe Tele.

    Vortragstitel: Component Synthesis from Service Specifications
    Referent: Ingolf Krüger (UC San Diego)
    Zeit und Ort: 15.9.2003, 15:00, 00-010/14 Geb. 101


    The notion of service enjoys increasing popularity as a means for
    structuring complex distributed systems. The current trend towards "web
    services" is just one example of this increase in popularity; others
    occur in safety-critical systems (such as in the automotive or avionics
    domain), where precise specification, and correct implementation of
    requirements are essential. In this presentation, we suggest a formal
    foundation for services. Catering to the importance of interaction
    modeling in specifying and deploying services, we show how Message
    Sequence Charts (MSCs) -- an integral part of the emerging UML 2.0
    standard -- can be semantically mapped to our service definition. We
    also address aspects of service modeling missing from MSCs; these
    include overlapping interactions, liveness specifications, and
    preemption. Starting from interaction models for services we show how to
    synthesize state machine models implementing the specified interaction

  • 6.11.2003: Verification of Optimizing Compilers
    Sabine Glesner, Universität Karlsruhe

    -- Abstract:
    Compiler correctness is a necessary prerequisite to ensure software
    correctness and reliability as most modern software is written in
    higher programming languages and needs to be translated into native
    machine code. In this talk, we report on results as well as on ongoing
    research concerning verification of optimizing compilers.

    Starting from intermediate representations in static single assignment
    form, we consider optimizing machine code generation based on
    bottom-up rewrite systems. We show how such transformation algorithms
    can be formally verified. In particular, we address the issue of
    formalizing these proofs within the Isabelle/HOL system. Furthermore,
    we discuss the use of program checking to ensure the correctness of
    the corresponding compiler implementations. Thereby, we introduce a
    novel checking method which we call "program checking with
    certificates" and discuss its application to optimizing code
    generation. We have implemented this algorithm in a checker for a code
    generator used in an industrial project. This experiment reveals that
    the code generator and its checker are closely connected, in
    particular that most of the checker code is also part of the code
    generator implementation.

  • Freitag, 7.11.2003, 15:00 Uhr s.t.

    Raum 02-018, Georges-Köhler Allee 101, 79110 Freiburg

    Routing in Ad-Hoc-Fahrzeugnetzen: Simulations- und Testergebnisse aus
    dem Projekt FleetNet

    Prof. Dr. Hannes Hartenstein

    Universität Karlsruhe


    Das vom BMBF geförderte Projekt 'FleetNet - Internet on the Road'

    ( entwickelt eine Kommunikationsplattform für die
    Kommunikation zwischen Fahrzeugen auf Basis von
    Ad-Hoc-Netzwerkprinzipien. In dem Vortrag gebe ich einen Überblick über
    das Projekt und widme mich insbesondere der Frage nach dem Routing in
    solchen hochdynamischen Netzen. Ich stelle das sogenannte
    positionsbasierte Routing vor und verdeutliche anhand von
    Simulationsstudien sowie durch Messungen an dem
    FleetNet-Demonstratorsystem die Leistungsfähigkeit dieses Ansatzes.

  • 12.12.2003, 11:00., Room 01-018, building 101.: Dr. Christoph Sprenger

    Compositional and Inductive Reasoning in the Verification of Temporal
    Program Properties


Modern computing systems are characterised by their highly dynamic and modular
nature: at runtime new components are created, old ones are removed and both
communication and data structures evolve dynamically. The verification of
temporal properties of such systems requires the combination of compositional
and inductive reasoning techniques. Compositional reasoning also supports
scalability to larger systems by decomposing a complex verification task into a
number of (hopefully) simpler ones.

In the first part of this talk, I will outline the main features of a
compositional proof systems for the modal mu-calculus, a modal logic with least
and greatest fixed point recursion. I will discuss how compositional and
inductive reasoning are achieved in this system. To facilitate automatic proof
search, we use a global style of induction based on circular proofs and an
external well-foundedness condition.

In the second part, I will focus on automatic compositional verification. In
particular, I will present a method for the verification of control-flow based
safety properties of multi-applet JavaCard applications. Here, compositionality
supports secure post-issuance loading of new applets onto a smartcard that has
already been issued to a user. We model applets by pushdown processes and use a
technique based on maximal models to reduce the compositional model checking
problem to a standard one.

  • 16.12.2003, Raum 01-016 im Geb. 101 um 11:00 s.t.: Herr Aljazzar (Uni Marburg).

    Titel: Massenoperation auf Indexstrukturen für Datenströme


    In Anwendungen, die große Datenmengen bearbeiten, werden so genannte Indexstrukturen
    wie B-Bäume eingesetz, um die Bearbeitungseffizienz durch geschickte Datenorganisation.
    zu erhöhen.
    In vielen Anwendungen ist es notwendig historische Anfragen zu unterstützen, deshalb
    müssen mehrere Versionen des Datenbestands verwaltet werden. Der Multiversions-B-Baum
    (MVBT) kann diese Aufgabe asymptotisch optimal erledigen.
    Aber die rashe Datenübertragung stellt eine neue Herausforderung dar. Damit MVBT in
    schnellen Anwendungen wie Datenströmen einsetzbar wird, muss es so erweitert werden,
    dass große Datenmengen schnell hinzugefügt werden können.
    Die Idee dieser Diplomarbeit ist es, das s.g. Buffer-Tree zu verwnden, um die ankommenden
    Daten erst in Puffern zu sammeln und mengenweise einzufügen.
    In diesem Vortrag wird demonstriert, wie das realisiert wird und welche Vor- und Nachteile
    das zur Folge hat.

  • 8.1.2004, 15:00-16:00. Room 00-034, building 51.:

    Spi Calculus Translated to pi-Calculus Preserving Testing

    Michael Baldamus, Uppsala University

    joint work together with Joachim Parrow and Björn Victor

    The spi-calculus is used to describe cryptographic protocols
    and has primitives and data types for encryption, keys and hash
    codes. It is an extension of the pi-calculus, a class of formalisms
    for parallel processes with dynamic structure. We present a translation
    of spi into a basic dialect of pi. The translation is proven sound
    with respect to testing and is has been implemented in a
    prototype tool. As a consequence, protocols can be described in the spi
    calculus and analysed with the emerging flora of tools already available
    for pi. The translation also entails a more detailed operational view of
    the semantics of spi since the high level constructs are encoded in a
    well known lower level.

    The talk will include a demonstration of the prototype tool.

  • 16.1. um 14:30: 02-016, Geb. 101. Herr Zhan (Uni Mannheim): On Hierarchically Developing Reactive Systems".

    The hierarchical development method is one of the most practical and
    effective methods for designing large reactive systems by
    allowing a design at different levels of abstraction.
    Relating hierarchical specification to hierarchical implementation
    plays a key role in decreasing the complexity of
    the verification of these systems. But, up to now,
    few work has been done related to the topic.

    In this talk, we propose an approach on combining
    hierarchical specification and hierarchical implementation of a
    complex system in order to simplify the verification of
    the system. To the end, we define a refinement mapping from a high-level
    specification and the properties of the refined lower-level component
    to a lower-level specification, which preserves the type of
    the property to be refined. Furthermore, we establish a
    correspondence between hierarchical specification and hierarchical implementation that
    supports `a priori' verification in system design.

  • 26.1.2004, 16:00, Raum 02-17 Geb. 52: Barbara König, Universität Stuttgart.

    TITLE: Analysis of Graph Transformation Systems


    Graph transformation systems are a natural and elegant specification
    formalism for concurrent, mobile and dynamically evolving systems. But
    so far there exists little work about verification and analysis
    techniques. We present a technique inspired by the framework of
    abstract interpretation where a complex system is safely approximated
    by a simpler one, such that the simpler system exhibits at least all
    possible behaviours of the original system. In our case we approximate
    graph transformation systems by Petri nets, using an unfolding
    technique known from the area of Petri nets. The approximating Petri
    net can then be analyzed in order to obtain properties of the original
    system, such as security properties, deadlock freedom or absence of
    unwanted computation paths. We have in mind applications such as the
    analysis of mobile and distributed systems, but also analysis of
    evolving data structures in a program (shape analysis).

    This is joint work with Paolo Baldan (Universita Ca' Foscari di
    Venezia) and Andrea Corradini (Universita di Pisa).

  • Montag, 9.2.2004, 16:00 Uhr s.t. Raum 02-017, Georges-K?hler Allee 52, 79110 Freiburg

    The Security Bug Catcher, or finding vulnerabilities automatically

    Dr. Philippe Oechslin

    EPF Lausanne


    Again and again hackers find and exploit new vulnerabilities in existing software. Typical examples are the SQL-Slammer and MS-blaster worms that wreaked havoc in the Internet last year. Vulnerabilities are often discovered by accident or by experienced hackers. The Internet would be much safer and more reliable if vulnerabilities could be found before products are shipped. The Security Bug Catcher is a tool being developed at LASEC which aims at finding vulnerabilities automatically. It is based on a formal description of the system under test and a model of typical vulnerabilities. First vulnerabilities have already been discovered in FTP and POP3 servers. In this talk we want to present the challenges of creating such a tool and to discuss first results and possible evolutions.

  • Dienstag, 10.2.2004, 11:00 Uhr

    Raum 02-016, Georges-K?hler Allee 101, 79110 Freiburg

    The Cryptanalytical Time-Memory Trade-Off: how fast can you go?

    Dr. Philippe Oechslin

    EPF Lausanne


    Since Martin Hellman introduced the Cryptanalytical Time-Memory Trade-Off in 1980, only few optimisations have been suggested. At Lasec we have developed a new way of organizing the trade-off which makes it an order of magnitude faster. Moreover the new trade-off has a more regular structure, which reduces precomputation time, allows for a better analysis of its performance and opens up possibilities for other improvements. We will present the original trade-off, the new version that was presented at Crypto '03 (with the 5 second windows password cracker demo) and new directions for creating an even more efficient trade-off.

  • Friday 26.3.2004, 11:00 st., Room: 02-016 building 101: . Prof. Sekerinski

    Title: A Model and Language for Concurrent Object-Oriented Programming

It has been argued for a long time that objects can be naturally thought of as evolving independently and thus concurrently; an object is a natural "unit" of concurrency. Yet, current mainstream object-oriented languages treat concurrency independently of objects: concurrency is expressed in terms of threads that have to be managed separately from objects. We argue for a model for concurrent object-oriented programs in which no such distinction is made. The only syntactic additions needed are extending classes by actions and allowing methods to be guarded. Execution is governed by a simple rule for atomicity. The model allows concurrency to be seamlessly introduced in classes, thus for example allowing concurrency to be introduced in subclasses of a class hierarchy. This permits concurrency to be treated as an implementation issue in the same way as the choice of an algorithm. The model relieves the programmer from having to distinguish between the process (thread) and class aspects in software design. We illustrate the model by examples, discuss its rationale, outline a theory of class verification and refinement, and sketch the current implementation of Lime, a language following this model.

The Slides(PDF)