WG 2.2 Meeting
September 05-06, 2009
and abstracts of talks
(in chronological order)
Frank de Boer
Title: On Deadlock Detection of Reentrant Multithreaded Programs
Title: On Session Types and Linear Logic
Title: Kleene Coalgebra
We present an overview of four recent papers:
1. Marcello Bonsangue, Jan Rutten, Alexandra Silva.
Coalgebraic logic and synthesis of Mealy machines.
2. Marcello Bonsangue, Jan Rutten, Alexandra Silva.
A Kleene theorem for polynomial coalgebras.
3. Marcello Bonsangue, Jan Rutten, Alexandra Silva.
Algebras for Kripke polynomial coalgebras.
4. Filippo Bonchi, Marcello Bonsangue, Jan Rutten,
Alexandra Silva. Deriving syntax and axioms for
quantitative regular behaviours.
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.
Title: Termination in higher-order concurrent languages
Title: Applying the Graph Minor Theorem to the Verification of Graph
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
Title: Newtonian Program Analysis
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)
Title: Models for Open Transactions
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)
Rocco De Nicola
Title: Rate-based Transition Systems for Stochastic Process Calculi
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)
Title: Abstraction of Probabilistic Systems: From Theory to Practice
Title: Actors Performing: Domain Specific Modeling and Analysis
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.
Title: Use Process Calculi for 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).
Title: Weak Alternating Timed Automata
Title: Finite Automata as Time-Invariant Linear Systems: Observability, Reachability and More
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.
Title: Rigorous abstraction from continuous control to automata