IFIP Working Group 2.2 Meeting
14 - 17 May 2001, Rennes, France.

Abstracts of the talks

Manfred Broy
The essence of Messega Sequence Charts

Egon Boerger
Java and the Java Virtual Machine: Verifying and validating bytecode verification and execution

Concise abstract (ASM) code is provided for interpreting Java programs and for a fast Java Virtual Machine (JVM) which serves as platform for a general compilation scheme of Java programs to JVM code. These definitions allow us to prove that any compiler that satisfies some natural conditions compiles legal Java code correctly. As a by-product we provide a challenging realistic case study for mechanical verification of a compiler correctness proof.

The modularity of the ASM definitions for Java, the JVM and the compilation scheme exhibit orthogonal language, machine and compiler components, which fit together and provide the basis for a stepwise and provably correct design--for--reuse. The above definition for the JVM is extended to a defensive JVM which can be used as Java independent platform for safely executing byte code. Separating the checking mechanism from the execution we obtain a model for the bytecode verifier which can be proved to be correct and complete. By extending the compiler to a certifying compiler we can prove our compiler to generate code which successfully passes the bytecode verifier. As last step this bytecode verifier is integrated into a loading machine which together with the executing ASM provides a full JVM model.

The construction makes use of new composition techniques for building complex ASMs. These abstract machines for Java, the JVM and the compiler have also been refined to executable machines, which have been validated through experimentation with ASMGofer (available at http://www.uni-ulm.de/~s_jschmi/AsmGofer).

A full documentation is in the book R. Staerk, J. Schmid, E. Boerger: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer-Verlag (2001), see http://www.inf.ethz.ch/~jbook

Anders Ravn
Developing Embedded Systems - where are Foundations needed?

Catuscia Palamidessi (joint work with Mihaela Herescu)
On the generalized dining philosophers problem.

The problem of the dining philosophers, proposed by Dijkstra, is a very popular example of control problem in distributed systems. In the classic formulation the philosophers sit at a round table and there is a fork between any two philophers. In order to eat, each philosopher needs both his adjacent forks. The aim is to make sure that if there are hungry philosophers then some of them will eventually eat (deadlock freedom), or, more ambitiously, that every hungry philosopher will eventually eat (lockout freedom).

In the early 80's, Lehman and Rabin showed that there exist no deterministic, symmetric and fully distributed solution to the problem of the dining philosophers, and they proposed two randomized solutions: one which guarrantees deadlock freedom with probability 1 and another one which guarrantees lockout freedom with probability 1.

In this talk, we consider a generalization of the dining philosophers problem where the number of philosophers can exceed the number of forks (although each philosopher can still only access two forks), and we study whether the randomized algorithms of Lehman and Rabin still work in this situation. We show that the answer is "No": in most cases, a malicious scheduler can induce a deadlock. We then show a randomized solution, still fully distributed and symmetric, which works for any number of philosophers and any kind of connection graph, and guarrantees lockout freedom with probability 1.

Marcelo Fiore
On model checking security properties of cryptographic protocols

Stephan Merz
Temporal logic with(out) limits

We consider an extension of standard first-order temporal logic of linear time by assertions about the "limits" and "histories" of sequence-valued state variables. For example, the specification of a FIFO queue can in such a language be written as
[](hist out \prefix hist in) /\ (lim out = lim in)
where 'in' and 'out' are the variables representing the queue's input and output channels. (A standard result due to Sistla et al states that it is impossible to specify a FIFO queue in LTL without additional assumptions.) More precisely, we extend LTL formulas by predicates of the form
hist c \prefix hist d and lim c \prefix lim d
We show that the formulas of the extended language can be expressed in LTL augmented by history variables. We also consider the model checking problem for the extended logic over transition systems with finite control, but unbounded output channels over finite alphabet. Although that problem is undecidable in general, the problem of deciding
T |= lim c \prefix lim d
is decidable. This result could have applications in the verification of communication protocols and other systems involving buffered communication.

Wjciech Penczek
Bounded model checking for the universal subset of TCTL

Dina Goldin (based on work with Scott Smolka)
Modeling interactive computation: Turing machines or labeled transition systems?

Interactive computation, such as that of components, reactive systems, or embedded devices, has several characteristics that distinguish it from the ``algorithmic'' computation captured by the Church-Turing thesis: (a) inputs/outputs are consumed/produced during the computation, rather than before/after it; (b) input values are generated dynamically by the environment, and can depend on earlier outputs; (c) output values are generated dynamically by the computing device, and can depend on earlier inputs (``history dependence''); (d) computation is not assumed to terminate; (e) the environment is not assumed to be computable.

We present Persistent Turing Machines (PTMs), whose computation is a stream-based and persistent extension of Turing machine (TM) computation. A PTM repeatedly receives an input token from the environment, computes for a while, and then outputs the result; moreover, its work tape is persistent, so it ``remembers'' its previous contents upon commencing a new computation. We show that the class of PTMs is isomorphic to interactive transition systems, a very general class of effective LTSs. As a result, PTMs admit a much richer variety of equivalence relations than do TMs; bisimulation, and persistent stream language (PSL) equivalence are examples.

We also consider amnesic PTMs, where each new computation begins with a blank work tape, and a corresponding notion of equivalence based on amnesic stream languages (ASLs). It can be argued that amnesic stream languages are representative of the classical view of Turing-machine computation. We show that the class of ASLs is strictly contained in the class of PSLs. Furthermore, the hierarchy of PTM equivalence relations collapses for the subclass of amnesic PTMs. One may consequently conclude that, in a stream-based setting, the extension of the Turing-machine model with persistence is a nontrivial one. It results in a natural model of sequential interactive computation, offering a bridge between TM-based computational models and those based on LTSs, and providing a formal foundation for reasoning about interactive computation.

Davide Sangiorgi
Extensionality and intensionality in the Ambient Logic

Igor Walukiewicz
First-order logic on traces

Michel Bidoit
Abstract interpretation: an algebraic approach

Peter Mosses
A New Version of Action Semantics

Frank de Boer
Proof-Outlines for Threads in Java

In this talk I discussed the main ideas underlying my paper presented at CONCUR 2000 which introduces an assertional method for specifying and proving properties of the multi-threaded flow of control in Java. The method integrates in a modular manner reasoning about the shared-variable concurrency within one object and the communication of values between threads.

Markus Mueller-Olm
Limits of optimal parallel flow analysis

abstract (postscript)


WG 2.2 (darondeau@irisa.fr)