IFIP WG 2.2 Meeting Bologna

September 05-06, 2009

Titles and abstracts of talks

(in chronological order)

 

 

Speaker: Frank de Boer
Title: On Deadlock Detection of Reentrant Multithreaded Programs

Abstract:

 

Missing.

 

 

Speaker: Luis Caires
Title: On Session Types and Linear Logic

Abstract:

Several expressive linear type systems for the pi-calculus have been proposed, in particular session type systems, which impose well-behaved communication protocols on concurrent processes. In this talk we discuss a new type system for the pi-calculus that exactly corresponds to the standard sequent calculus proof system for intuitionistic linear logic. Perhaps surprisingly, the induced type discipline establishes a close connection between intuitionistic linear logic, linear and session types, and forms of concurrent functional evaluation.

 

(Joint ongoing work with Frank Pfenning)

 

 

Speaker: Jan Rutten
Title: Kleene Coalgebra

Abstract:

 

We present an overview of four recent papers:

1. Marcello Bonsangue, Jan Rutten, Alexandra Silva.
Coalgebraic logic and synthesis of Mealy machines.
FoSSaCS 2008.

2. Marcello Bonsangue, Jan Rutten, Alexandra Silva.
A Kleene theorem for polynomial coalgebras.
FoSSaCS 2009.

3. Marcello Bonsangue, Jan Rutten, Alexandra Silva.
Algebras for Kripke polynomial coalgebras.
LICS 2009.

4. Filippo Bonchi, Marcello Bonsangue, Jan Rutten,
Alexandra Silva. Deriving syntax and axioms for
quantitative regular behaviours.
CONCUR 2009.

 

Speaker: Einar Broch Johnsen
Title: Runtime Evolution of Distributed Concurrent Objects

Abstract: Many long-lived and distributed systems must remain available yet evolve over time, due to, e.g., bugfixes, feature extensions, or changing user requirements. To facilitate such changes, formal methods can help in modeling and analyzing runtime software evolution. This paper presents an executable object-oriented modeling language which supports runtime software evolution. The language, based on Creol, targets distributed systems by active objects, asynchronous method calls, and futures. A dynamic class construct is proposed in this setting, providing an asynchronous and modular upgrade mechanism. At runtime, class redefinitions gradually upgrade existing instances of a class and of its subclasses. An upgrade may depend on previous upgrades of other classes. For asynchronous runtime upgrades, the static picture may differ from the actual runtime system. An operational semantics and a type and effect system are given for the language. The type analysis of an upgrade infers and collects dependencies on previous upgrades. These dependencies are exploited as runtime constraints to ensure type safety.

 

 

Speaker: Davide Sangiorgi
Title: Termination in higher-order concurrent languages

Abstract:

 

We discuss the problem of termination in concurrency, in particular higher-order concurrency. We first illustrate the interest of the problem, including the possibility of combining the termination analysis with deadlock analysis so to obtain a powerful analyser for general liveness properties. We then survey some recent works on the study of termination in a concurrent setting. Processes are pi-calculus processes, on which type systems are imposed that ensure termination of the process computations. Two approaches are exposed. The first one draws on the method of logical relations, which has been extensively used in the analysis of higher-order sequential languages. The second approach exploits notions from term rewriting. Finally I will illustrate an attempt at trying to combine the two approach and discuss its usefulness.


 

Speaker: Barbara Koenig
Title: Applying the Graph Minor Theorem to the Verification of Graph
Transformation Systems

Abstract:

 

We show how to view certain subclasses of (single-pushout) graph transformation systems as well-structured transition systems, which leads to decidability of the covering problem via a backward analysis. As the well-quasi order required for a well-structured transition system we use the graph minor ordering. We sketch an explicit construction of the backward step and apply our theory in order to show the correctness of a leader election protocol.

 

 

Speaker: Javier Esparza
Title: Newtonian Program Analysis

Abstract:

 

In this talk I'll look at a sequential program as a system of equations of the form

X_1 = f_1(X_1, ..., X_n)
...
X_n = f_n(X_1, ..., X_n)

where the f_i's are polynomials, and sum and product correspond to choice and sequential composition. (If you're familiar with process algebras, this should ring a bell.) I'll argue that static program analysis is the art of solving these equations over different interpretations,
depending on the information one is interested in.

After 40 years of research on static analysis we have not produced much theory on *generic* methods for solving these equations, i.e., on methods that work for *any* interpretation. The ones around are based on Knaster-Tarski's and Kleene's theorems. Unfortunately, these methods rarely terminate for infinite domains, and in metric interpretations their convergence is often hopelessly slow. Can't we do better?

I'll show that Newton's method, well-known from numerical mathematics, can be generalized to (almost) arbitrary interpretations, and that this generalization provides a unified view of many results of language theory, as well as a bridge between qualitative and quantitative program analysis.

(Joint work with Stefan Kiefer and Michael Luttenberger)

Slides

 

Speaker: Ugo Montanari
Title: Models for Open Transactions

Abstract:

 

Loosely coupled interactions permeate modern distributed systems, where autonomous applications need to collaborate by dynamical assembly. We can single out three different phases occurring in every collaboration: 1) negotiation of some sort of contracts, mediating the needs of prospective participants; 2) acceptance or rejection of the contract; 3) contract-guarantee execution. The above scheme, called NCE for short (Negotiation, Commit, Execution), covers a wide range of situations, ranging from sessions and transactions to proof-carrying code. In the talk we concentrate on the notion of open transaction and on Zero-Safe Nets, a model developed by Bruni and Montanari for modelling long transactions. We extend the latter to cover the three-phase process above.


(Joint work with Roberto Bruni)

 

 

Speaker: Rocco De Nicola
Title: Rate-based Transition Systems for Stochastic Process Calculi

Abstract:

 

A variant of Rate Transition Systems (RTS) is introduced and used as the basic model for defining stochastic behaviour of processes and for associating Continuous Time Markov Chains to process terms. The transition relation used in our variant associates to each process, for each action, the set of possible futures paired with a measure indicating their rates.We show how RTS can be used for providing the operational semantics of stochastic extensions of classical formalisms, namely CSP and CCS. We also show that our semantics for stochastic CCS guarantees associativity of parallel composition. Similarly, in contrast with the original definition by Priami, we argue that a similar approach for defining the semantics of stochastic pi-calculus guarantees associativity of parallel composition.

(Joint work with Diego Latella, Michele Loreti and Mieke Massink)

Slides

 

Speaker: Joost-Pieter Katoen
Title: Abstraction of Probabilistic Systems: From Theory to Practice

Abstract:

 

Model checking of probabilistic models is used in many different areas such as performance and dependability evaluation, security protocols, randomized algorithms, and biological systems. Tools have been successfully applied to numerous case studies, but like in traditional model checking, the state explosion problem forms a serious limitation. Although many techniques from traditional model checking have been generalized towards probabilistic models such as BDDs and partial-order reduction, more aggressive reduction techniques are needed. In this talk, we introduce model checking of continuous-time Markov chains (CTMCs), present a three-valued abstraction technique, and present several examples to show its effectiveness when applied to huge, and even infinite CTMCs such as arising from systems biology and classical performance analysis, i.e., queuing networks.

 

 

Speaker: Marjan Sirjani
Title: Actors Performing: Domain Specific Modeling and Analysis

Abstract:

 

Actor model for concurrent object-based computation is being more widely used in various domains including system-level designs and agent-based systems. Likewise, actor-based architectures and languages are getting more popular in software development industry today. However, actor model is not supported by sufficient formal analysis techniques and tools.
The Reactive Object Language, Rebeca, is an imperative interpretation of actors which is designed as an analyzable modeling language for real-world applications. It is supported by model checking tools and compositional verification approaches. Reduction techniques including slicing, partial order and symmetry detection are developed based on the computational model of Rebeca.
Rebeca has a simple kernel and is extended specifically for the domain of applications. In this talk, we present the computational model of Rebeca, its analysis techniques, and extensions for various domains.


 

Speaker: Uwe Nestmann
Title: Use Process Calculi for Fault-Tolerant Distributed Algorithms?

Abstract:

 

We report on a case study with the goal to evaluate in how far a particular style of equational reasoning in a process calculus context scales up to the domain of fault-tolerant distributed algorithms.

More precisely, we sketch Milner's scheduler example as known from his textbook and examine the involved proof strategy. It is essentially based on a concise notation to capture all reachable states in a way that makes it possible to succinctly describe and analyze invariants. The actual proofs then involve so-called "bisimulation up-to" techniques.

Following this strategy, we show that it indeed scales up to the chosen case study: a distributed consensus algorithm due to Chandra and Toueg in the context of the failure detector S. Apart from the fact that this algorithm requires non-trivial analysis work, we conclude that using process calculi this way provides us with a useful tool to formally connect an invariant-style state-based reasoning to the underlying algorithm code (formally spelled out within the process calculus, as opposed to informal pseduo code).

 

Speaker: Igor Walukiewicz
Title: Weak Alternating Timed Automata

Abstract:

 

Alternating timed automata on infinite words are considered. The main result is a characterization of acceptance conditions for which the emptiness problem for the automata is decidable. This result implies new decidability results for fragments of timed temporal logics. It is also shown that, unlike for MITL, the characterization remains the same even if no punctual constraints are allowed.

Slides

 

Speaker: Radu Grosu
Title: Finite Automata as Time-Invariant Linear Systems: Observability, Reachability and More

Abstract:

 

We show that regarding finite automata (FA) as discrete, time-invariant linear systems over semimodules, allows to: (1) Express FA minimization and FA determinization as particular observability and reachability transformations of FA, respectively; (2) Express FA pumping as a property of the FA's reachability matrix; (3) Derive canonical forms for FAs. These results are to our knowledge new, and they may support a fresh look into hybrid automata properties, such as minimality. Moreover, they may allow to derive generalized notions of characteristic polynomials and associated eigenvalues, in the context of FA.

Published in Proc. of HSCC'09, the 12th International Conference on Hybrid
Systems: Computation and Control, San Francisco, USA, April, 2009, pp. 194-208,
Springer, LNCS 5469.

*This work was supported by the NSF Faculty Early Career Development Award
CCR01-33583 and the NSF CCF05-23863 Award.

 

Speaker: Anders Ravn
Title: Rigorous abstraction from continuous control to automata

Abstract:

 

Many embedded programs control dynamical systems that are modelled using principles from physics; the models are thus continuous, differentiable functions. However, the control is essentially discrete, and for advanced applications, it is no longer feasible to discretize with some global sampling rate and use standard results. The control needs to be designed as supervisory finite state machines that switch between simple continuous control functions. Such designs have been done using a variety of ad-hoc techniques; but recently systematic techniques have been developed that cover interesting classes of continuous control systems. Technically they rely on (bi)simulations parametrized by granularity and precision constants. These constructions will be outlined.