IFIP WG 2.2 Meeting Paris

September 21-23, 2011

Titles and abstracts of talks

(in chronological order)

Speaker: Igor Walukiewicz
Title: Krivine machines and higher order schemes

Abstract:

We discuss a new approach to analysing higher-order recursive schemes. Many results in the literature use automata models generalising pushdown automata, most notably higher-order pushdown automata with collapse (CPDA). Instead, we propose to use the Krivine machine model. Compared to CPDA, this model is closer to lambda-calculus, and incorporates nicely many invariants of computations, as for example the typing information. The usefulness of the proposed approach is demonstrated with new proofs of two central results in the field: the decidability of the local and global model checking problems for higher-order schemes with respect to the mu-calculus.

Speaker: Christel Baier
Title: On Operational Semantics of Message Sequence Graphs

Abstract:

Message sequence charts provide a visual formalism to specify communication scenarios of concurrent systems. Message sequence graphs (MSG) serve to combine message sequence charts via choice, concatenation and iteration. The talk gives a summary of formal semantics for message sequence graphs that have been proposed in the literature. The focus of the talk is on branching-time semantics (prime and flow event structures and the induced transition system semantics) that might serve as basis for probabilistic extensions of MSG.

Speaker: Kohei Honda
Title: Sessions, Types and Logics

Abstract:

In the current computing practice, the major, well-understood structuring principles for computing, from high-level modelling to systems software and beyond, centre on functions and objects. This talk will argue, through examples, that diverse factors in computing increasingly demand the positioning of communication as a central element of the description and organisation of computing. As a potentially widely usable structuring principle for communication-centred computing, we illustrate the key ideas behind an informal notion of sessions for communicating processes, explored in networking and other areas of computing for decades. We then outline how sessions induce an expressive notion of types for communication. If time allows, we shall discuss how a logical theory may be built on the basis of session types, offering a framework for flexible, concise specification and validation.

Speaker: Gilles Barthe
Title:Computer-Aided Security Proofs for the Working Cryptographer

Abstract:

As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of developing techniques that help tame the complexity of their proofs. Game-based techniques provide a popular approach in which proofs are structured as sequences of games, and in which proof steps establish the validity of transitions between successive games. We present two frameworks that allow to formally specify and verify game-based cryptographic proofs: CertiCrypt and EasyCrypt. Both frameworks take a language-based approach to proofs: games are represented as probabilistic programs and proof steps are justified by logical judgments.

Speaker: Einar Broch-Johnsen
Title: Deployment Components with Parametric Resources

Abstract missing

Speaker: Andrzej Tarlecki
Title: Compositional Property-oriented Semantics for Structured Specifications. Another Old Story (with a Few New Twists)

Abstract:

We discuss property-oriented semantics of specifications built using some collection of specification-building operations. Working in an arbitrary institution, we consider the structured specifications built from flat specifications using union, translation and hiding. We then have the standard compositional proof system, which determines the standard property-oriented semantics assigning a theory to each structured specification. It is not complete (unless the underlying logic has interpolation and enjoys some other technical properties) but otherwise it is "as good as can be expected". In particular, it is sound, monotone (and hence compositional) and closed complete. The last property means that the semantics (and the corresponding proof system) allows us to deduce all true consequences for specifications built by applying any specification-building operation to argument specifications, assuming that there is no discrepancy between the classes of models of the argument specifications and the classes of models of their respective property-oriented meanings. This was believed to ensure that the semantics is "as strong as possible" without loosing soundness and compositionality. We question this claim and show that it holds assuming in addition that the semantics considered are theory-oriented, i.e., the sets of properties assigned to specifications are closed under consequence, as well as non-absent-minded, i.e., no axioms from flat specifications are omitted as properties. We sketch examples to show that neither of these requirements may be dropped. We generalise this to the context of entailment systems, and show similar results and counterexamples.

Speaker: Frank de Boer
Title: Run-time Assertion Checking of Communication Histories in Java using Attribute Grammars

Abstract:

I presented a new approach to the specification of interfaces in Java in terms of communication histories, i.e., sequences of messages. This approach integrates attribute grammars which provide a powerful separation of concerns between high-level protocol-oriented properties, i.e., the kind of messages sent and received, and properties of the actual data communicated. I presented a corresponding modeling framework in Java for the integration of attribute grammars in the Java Modeling Language and illustrated corresponding tool-support for run-time assertion checking.

Speaker: Marco Pistore
Title: Composition (and Adapatation) of Service Based Applications

Abstract:

In the talk, we discuss the problem of service composition with digressions on service adaptation, two of the most challenging problems of the Service Oriented Computing paradigm. After an overview of these problems, we describe ASTRO, a framework for service composition and adaptation that has been developed in Trento during the last years, and that has been exploited both in research and in industrial projects. In particular, we show that, while service composition and service adaptation are in general intractable problems, in practical contexts they are used under specific conditions that make them tractable; moreover, as ASTRO witnesses, in these contexts formal methods provide practical and effective solutions to service composition and adaptation.

Speaker: Uwe Nestmann
Title: Synchronous and Asynchronous Interaction in Distributed Systems

Abstract:

A well-known result by Palamidessi tells us that the pi-calculus with mixed choice is more expressive than its subset with only separate choice. The proof of this result argues with their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of incestual processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role of breaking (initial) symmetries is more or less apparent. In this talk, we shed more light on this role by re-proving the above result - based on a proper formalization of what it means to break symmetries without referring to another layer of the distinguishing problem domain of leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from the pi-calculus with mixed choice into the pi-calculus with separate choice. We indicate how the respective proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential.

Speaker: Peter Mosses
Title: PLanCompS: Programming Language Components and Specifications

Abstract:

The PLanCompS project aims to establish and test the practicality of a component-based framework for the design, specification and implementation of programming and domain-specific languages. The main novelty will be the creation of a substantial open-ended collection of highly reusable language components called 'funcons' (fundamental constructs). The static and dynamic semantics of each funcon will be specified independently, using frameworks such as Modular SOS; languages will be defined by specifying their translation to funcons. Language and funcon specifications will be validated empirically, by running tests using prototype implementations generated from them. This talk introduces and illustrates the PLanCompS framework, and compares it to some previous approaches.

PLanCompS [www.plancomps.org] is a 4-year joint research project, based at Swansea, Royal Holloway and City, starting in September 2011. It is funded by EPSRC grant EP/I032495/1 and related grants.

Speaker: Ugo Montanari
Title: Component-Based Network Models

Abstract:

A quite flourishing research thread in the recent literature on component-based system is concerned with the algebraic properties of various kinds of connectors for defining well-engineered systems. In the talk several of them are shortly reviewed, in particular an algebra of stateless connectors by Ivan Lanese and the authors for Fiadeiro et al. CommUnity model, and its representation in terms of tile systems. The algebra consists of five kinds of basic connectors, plus their duals. The connectors can be composed in series or in parallel and have an operational, an axiomatic and a denotational semantics, which coincide. Employing in addition a 1-state buffer, these connectors can model the coordination language Reo. Pawel Sobocinski in his CONCUR 2010 paper employed essentially the same stateful extension of connector algebra to provide a semantics-preserving mutual encoding of some sort of elementary Petri nets with boundaries. In their CONCUR 2011 paper, the authors show how the tile model can be used to extend Sobocinski's approach to deal with P/T nets, thus paving the way towards more expressive connector models.

(Joint work with Roberto Bruni, Pisa & Hernan Melgratti, Buenos Aires. Work supported by FET-IST EU project ASCENS)

Speaker: Patricia Bouyer
Title: Quantitative Models for Verification, a timed-automata-based perspective

Abstract:

In this talk I have presented several examples of systems for which standard models have to be refined in order to adequately represent important characteristics of such systems. The basic model is that of timed automata, which has proven to be of great interest for verification purpose, and extensions I have presented are game extensions, weighted extensions or stochastic extensions thereof. Those extensions are useful for modelling uncertainties, interaction, resources, etc.

Speaker: Wojciech Penczek
Title: A Practical Approach to Parametric Model Checking

Abstract:

First we show how bounded model checking can be applied to verification of parametric real-time CTL for Elementary Net Systems and parametric reachability for Time Petri Nets with discrete semantics. Then, we present parameter synthesis for parametric timed automata with continuous time. While it is known that the general problem is undecidable even for reachability, we show how to synthesize a part of the set of all the parameter valuations under which the given property holds in a model. The results form a full theory which can be easily applied to parametric verification of a wide range of temporal formulae - we present such an implementation for the existential part of CTL-X.

Speaker: Leslie Lamport
Title: What Will it Take to Get You to Teach With PlusCal?

Abstract:

PlusCal is an algorithm language based on TLA+. A PlusCal algorithm is automatically translated to a TLA+ specification that can be checked with the TLC model checker or reasoned about formally. PlusCal makes pseudo-code obsolete. It is the ideal language for teaching sequential, concurrent, and distributed algorithms.

Speaker: Ernst-Rüdiger Olderog
Title: An Abstract Model for Proving Safety of Multi-Lane Traffic Manoeuvres

Abstract:

We present an approach to prove safety (collision freedom) of multi-lane motorway traffic with lane-change manoeuvres. This is ultimately a hybrid verification problem due to the continuous dynamics of the cars. We abstract from the dynamics by introducing a new spatial interval logic based on the view of each car.

To guarantee safety, we present two variants of a lane-change controller, one with perfect knowledge of the safety envelopes of neighbouring cars and one which takes only the size of the neighbouring cars into account. Thereby we assume that each car can communicate with its neighbouring cars and is equipped with suitable sensors. The guards and state invariants of the controllers are described in the new logic.

Based on these controllers we provide a local safety proof for unboundedly many cars by showing that at any moment the reserved space of each car is disjoint from the reserved space of any other car.

(joint work with Martin Hilscher, Sven Linker and Anders P. Ravn)

Speaker: Catuscia Palamidessi
Title: Differential Privacy and Relation with Quantitative Information Flow

Abstract:

Differential privacy is a notion of privacy that has become very popular in the database community. Roughly, the idea is that a randomized query mechanism provides sufficient privacy protection if the ratio between the probabilities that two adjacent datasets give the same answer is bound by $e^\epsilon$. In the field of information flow there is a similar concern for controlling information leakage, i.e. limiting the possibility of inferring the secret information from the observables. In recent years, researchers have proposed to quantify the leakage in terms of R\'enyi min mutual information, a concept strictly related to the Bayes risk. In this talk, we show how to model the query system in terms of an information-theoretic channel, and we compare the notion of differential privacy with that of mutual information. We show that differential privacy implies a bound on the mutual information, but not vice-versa. Furthermore, we show that our bound is tight. Then, we consider the utility of the randomization mechanism, which represents how close the randomized answers are, in average, to the real ones. We show that the notion of differential privacy implies a bound on utility, also tight, and we propose a method that under certain conditions builds an optimal randomization mechanism, i.e. a mechanism which provides the best utility while guaranteeing $\epsilon$-differential privacy.

Speaker: Marcelo Frias
Title: Automated Scope Bounded Code Analysis: State of the Art

Abstract missing