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
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
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
Das vom BMBF geförderte Projekt 'FleetNet - Internet on the Road'
(www.fleetnet.de) entwickelt eine Kommunikationsplattform für die
Kommunikation zwischen Fahrzeugen auf Basis von
Ad-Hoc-Netzwerkprinzipien. In dem Vortrag gebe ich einen Überblick
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
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
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
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.
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
already been issued to a user. We model applets by pushdown processes and
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
wie B-Bäume eingesetz, um die Bearbeitungseffizienz durch geschickte
In vielen Anwendungen ist es notwendig historische Anfragen zu unterstützen,
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
dass große Datenmengen schnell hinzugefügt werden können.
Die Idee dieser Diplomarbeit ist es, das s.g. Buffer-Tree zu verwnden, um
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
supports `a priori' verification in system design.
- 26.1.2004, 16:00, Raum 02-17 Geb. 52: Barbara König, Universität
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,
The Security Bug Catcher, or finding vulnerabilities automatically
Dr. Philippe Oechslin
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
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.