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
expressivity
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
p.d.mosses@swan.ac.uk
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
underlying
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?
Reference
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.