IFIP WG 2.2 Meeting Nancy
September 17-19, 2007
Titles and abstracts for talks
(in chronological order)
Speaker: Davide Sangiorgi
Title: Some remarks on equality and bisimulation in higher-order languages
Abstract: I discuss some of the approaches to defining equality between terms of (sequential) higher-order languages (eg, the lambda-calculus). In particular I discuss bisimulation, recalling the "standard" definition of bisimulation in lambda-calculus and proposing some modifications to it.
Speaker: Jan Rutten
Title: Coinduction: basics, examples, variations
Abstract: We present the basics of coinduction in terms of (final) coalgebra; illustrate it by means of some examples; and conclude by showing some recent extensions and variations.
The talk is structured as follows: first I will describe methods for finite-state
systems (using model-checking tools, isomorphism checking and unfoldings),
then I will talk about infinite-state systems (shape analysis, abstract graph
transformation, approximated unfoldings). The
talk concludes with some considerations about logics.
1. Relationship between the families of generators in terms of their
2. Algorithmic properties of infinite structures that are thus generated.
To support future semantic description of programming languages, the digital library could also include an evolving repository of reusable components in modular description frameworks such as Monadic Semantics, Modular SOS and Action Semantics.
WG 2.2 Members and Observers who have access to (printed or electronic) copies of significant semantic descriptions are requested to send the relevant publication data to
at their earliest convenience. It is anticipated that an initial version
of the library will be available by summer 2008.
This talk reviews the foundations of this technique and discusses some of the recent advances such as algorithms for counterexample generation.
Speaker: Herbert Wiklicky
Title: Abstract Interpretation for Worst and Average Case Analysis
(joint work with Alessandra Di Pierro Universita di Verona)
Abstract: This presentation focused on comparing the theoretical foundations
a coherent framework for qualitative and quantitative approaches in static program analysis. Central to such a unifying point of view are two closely related notions of ``approximation'' which formalise the concepts of ``correctness'' and ``closeness'' in different ways. This leads on the one hand to the framework of classical Abstract Interpretation (AI) based on
so-called Galois Connections - introduced by Cousot and Cousot in the 1970s - and on the other to Probabilistic Abstract Interpretation (PAI) based on the so-called Moore-Penrose Pseudo-Inverse - introduced by the authors. As an example, we discussed the concept of probabilistic bisimulation (introduced by Larsen and Skou) in the context of Probabilistic Abstract Interpretation, how to introduce an approximative version of this notion, as well as possible applications in the area of computer security.
Speaker: Uwe Nestmann
Title: Formal Methods (aka: Concurrency Theory) for Distributed Algorithms
Abstract: The formal verification of distributed algorithms, in particular fault-tolerant ones, still represents a rather non-trivial challenge. The field of Concurrency Theory offers a range of methods and techniques to formally specify and possibly verify concurrent and distributed systems. In this talk, we focus on the use of process calculi on this matter. The emphasis is put on the general approach and applicability of typical process calculus methods, referring to the traditional comparison between abstract high-level black-box specifications with concrete low-level white-box implementations, using notions of equivalence or congruence,
respectively. A number of verification examples are presented; their advantages and disadvantages as well as potential pitfalls are outlined.
Speaker: Einar Broch Johnsen
Title: Open distributed systems: an executable OO model
Abstract: We present an overview of the Creol language, an object-oriented modeling language for open distributed systems. The language, based on concurrent objects, addresses distribution by asynchronous method calls, delegation by first-class futures, and openness by a dynamic class construct which allow class definitions to evolve at runtime. Creol is an executable modeling language; i.e., although it is executable, its execution is highly nondeterministic. Specifically, it abstracts from particular network properties and allows local computation to adapt to the delays of the environment by an underspecified local scheduling. The language is statically typed, has a semantics defined in rewriting logic, and executes on the Maude system.
Speaker: Wolfgang Reisig
Title: Service modeling from scratch
Abstract: The paradigm of "Service-oriented Computing" provides a framework for interorganizational business processes and for the emerging ideas of "programming in-the-large". Services are to be comprehensible without reference to implementation details. Interaction of services is established by their composition. This gives rise to a number of problems:
- Are two services partners, i.e. do they properly compose?
- Does a service have partners at all (otherwise, it is definitely ill-designed)?
- How to characterize all partners of a service?
- How to represent an operating guideline for a service?
- Is there a canonical (most liberal) partner of a service?
- Can a service S' substitute a service S?
- Is there a canonical (most abstract) S' to substitute S?
- Can S' substitute S at runtime?
- How to adapt (i.e. mediate between) two services that "almost" properly compose?
Such issues can be discussed by means of models of services. We show how services can intelligibly be modelled, and we discuss algorithms and tools to analyze the above mentioned problems.
We also propose a new application of automata and the theory of decidable graph classes using tree interpretations: analysing heap invariants in programs.We present a preliminary study that is a general abstraction-refinement paradigm based on automata based shapes to capture invariants.
Speaker: Marino Miculan
Title: Directed bigraphs - a metamodel for communication, mobility and resources
Abstract: The plethora of calculi and models of concurrent systems motivate the research for general metamodels, i.e., frameworks, for describing uniformly as many computational paradigms as possible. In this talk we discuss "directed bigraphs", a bigraphical metamodel in the line of Milner's bigraphs, intended to express the aspects of distributed computing such as communications, location, mobility and resources. The key novelty with respect to other variants of bigraphs (which are subsumed), is that directed bigraphs take account of the ?resource request flow? from controls to edges (through names). Directed bigraphs support a general construction (called IPO construction) for deriving labelled transition systems from (possibly open) reactive systems; remarkably, these bisimulations are always congruences. After having presented the formalism, we exemplify the encoding methodology by showing how the lambda-calculus and the fusion calculus are represented.
Speaker: Thao Dang
Title: Coverage-guided test generation for hybrid systems
Abstract: Hybrid systems have been recognized as a high-level model appropriate for embedded systems, since this model can describe, within a unified framework, the logical part and the continuous part of an embedded system. Due to the gap between the capacity of exhaustive formal verification methods and the complexity of embedded systems, testing is still the most commonly-used validation method in industry. Its success is probably due to the fact that testing suffers less from the `state explosion' problem. Since it is impossible to enumerate all the admissible external inputs to the hybrid system in question, much effort has been invested in defining and implementing notions of coverage that guarantee, to some extent, that the finite set of input stimuli against which the system is tested is sufficient for validating correctness. For discrete systems, specified using programming languages or hardware design languages, some syntactic coverage measures can be defined, like exercising every statement or transition, etc. In this work, we treat continuous and hybrid systems that operate in a metric space and where there is not much inspiration coming from the syntax to the coverage issue. On the other hand, the metric nature of the state space encourages more semantic notions of coverage, namely that all system trajectories generated by the input test patterns form a kind of dense network in the reachable state space without too many big unexplored `holes'.
In this work we adopt a model-based testing approach. We propose a test coverage measure for hybrid systems, which is defined using the star discrepancy notion from statistics. This coverage measure is used to quantify the validation `completeness'. It is also used to guide input stimulus generation by identifying the portions of the system behaviors that are not adequately examined. We propose an algorithm for generating tests from hybrid systems models, which is based on the RRT (Rapidly-exploring Random Tree) algorithm from robotic motion planning and guided by the coverage measure. We also present an implementation of the algorithm and some experimental results on a number of case studies from control systems and analog and mixed-signal circuits.
Speaker: Ahmed Bouajjani
Title: Automata-based techniques for the verification of programs with dynamic linked data structures
(joint work with Peter Habermehl, Pierre Moro, Adam Rogalewicz, and Tomas Vojnar)
Abstract: We propose an approach for the automatic analysis of programs with dynamic linked structures using finite-state word/tree automata as representations for (potentially infinite) sets of heap structures. A heap of a given program is encoded as a word or a tree over an appropriate alphabet, and each statement in the program is translated into a transducer (I/O automaton) defining a transformation on the heap encodings. Then, iterative reachability analysis is performed using automata techniques in order to compute an upper-approximation of the set of all reachable heap configurations. The reachability analysis uses abstractions on automata representations (corresponding to finite index equivalence relations on their state space) allowing to speed up the fixpoint computation and to force termination. Automatic abstraction refinement is applied by need based on counterexample analysis. The proposed approach has been implemented and applied on various non trivial examples of programs.
Speaker: Christel Baier
Title: Probabilistic Buechi Automata
Speaker: Wojciech Penczek
Title: Model Checking of (Timed) Security Protocols
Abstract: In this talk we offer a novel methodology for verifying correctness of (timed) security protocols. The idea consists in computing the time of a correct execution of a session and finding out whether the Intruder can change it to shorter or longer by an active attack.Moreover, we generalize the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. An implementation of our method is discussed. As case studies we verify generalized (timed) authentication of Kerberos, TMN, Neumann Stubblebine Protocol, Andrew Secure Protocol, Wide Mouthed Frog, and NSPK.
Speaker: Catuscia Palamidessi
Title: Formal approaches to Information-hiding - An overview
(Partly based on joint work with Konstantinos Chatzikokolakis and Prakash Panangaden)
Abstract: We give an overview of various formal approaches from literature
to information-hiding: The possibilistic approaches, the probabilistic approaches,
the information-theoretic approaches, and the one based on statistical inference.
We compare the various frameworks and point out the relations. Finally, we
show how to specify information-hiding protocols and verify them (in the various
approaches) using language- based techniques.
Speaker: Antonin Kucera
Title: Quantitative analysis of probabilistic pushdown automata
Abstract: Probabilistic pushdown automata are obtained from "ordinary" non-deterministic PDA by attaching probabilities to transitions. Thus, each probabilistic PDA determines a discrete-time Markov chain with infinitely many states. We present selected constructions
and proof techniques that have recently been used to solve some natural problems of quantitative analysis of probabilistic PDA.
Speaker: R. Ramanujam
Title: A logic for strategies
Abstract: The analysis of non-zero-sum games proceeds by determining the response of players to opponents' strategies. However, this requires each player to know what every other player would do in every possible situation, which is quite unrealistic in large games. We look at situations where players construct bounded memory strategies in a structured manner, where the opponent's strategy may be known only by its properties. In the new setting we study the algorithmic question of finding best response for a player.
We also present a simple modal logic to reason about strategies and show
that checking assertion on a game graph is decidable.
Speaker: Frank de Boer
Title: Tasks for Actors
Speaker: Eike Best
Title: Separability, and other Equivalence Results
Abstract: The following four results were briefly discussed:
that bounded Petri nets can be transformed into pomset-equivalent safe nets;
that live and bounded marked graphs can be transformed into step-equivalent live and safe marked graphs;
that safe labelled marked graphs can be transformed into pomset-equivalent tau-free safe labelled marked graphs;
and that marked graphs can be separated.
Two open problems that have arisen in this context were also mentioned, namely:
can every safe labelled Petri net be transformed into a pomset-equivalent
tau-free safe labelled
Petri net; and are live and bounded persistent nets separable?
Eike Best, Philippe Darondeau, and Harro Wimmel:
Making Petri Nets Safe and Free of Internal Transitions.Fundamenta Informaticae 80(2007), 1-16.
Speaker: Marcelo Frias
Title: Combining Lightweight and Heavyweight Formal Methods
Abstract: The talk contained two main contributions. On the theoretical side, it presented a novel complete proof calculus for Alloy. On the applied side we presented Dynamite, a tool that combines the semi-automatic theorem prover PVS with the Alloy Analyzer. Dynamite allows one to prove an Alloy assertion from an Alloy specification using PVS, while using the Alloy Analyzer for the automated analysis of hypotheses introduced during the proof process.
Speaker: Luis Caires
Title: Logical Semantics of Types for Concurrency
Abstract: The subject-reduction proof method to the soundness of type systems turned out to be very successful and applicable to many kinds of programming languages, in particular, to concurrent process calculi. Nevertheless, it appears to have contributed in the long term to widespread a too syntactic understanding of types and typing, rather far from the original and more natural semantic view of types as properties or predicates.
In this talk, we motivate a logical semantic approach to types for concurrency
and to the soundness of related systems. The approach is illustrated by the
development of a generic type system for the pi-calculus, which may be instantiated
for specific notions of typing
by extension with adequate subtyping principles. Soundness of our type system is established using a logical predicate technique, based on a compositional spatial logic interpretation of types. This development gives some evidence that the intensional character of behavioral-spatial logics seems rather adequate for the characterization of several common type-like properties.