Participation is free, but please register if you intend to attend the seminar.

Security proofs are usually based on non-interference. In this work, we try to formalize security properties based on independence, i.e. non existence of interactions between subterms. This is joint work with Tomasz Blanc.

Les graphes planaires sont souvent présentés comme des chimères à la fois combinatoires et topologiques; leur étude, bien que relevant principalement de la combinatoire, fait cependant appel – le plus souvent de façon imprécise – au théorème de Jordan, un résultat assez difficile d'analyse. Nous montrons qu'en remplaçant ces graphes topologiques par des hypercartes, nous obtenons une théorie purement combinatoire de la planarité, comportant entre autres un équivalent du résultat de Jordan. Grâce à ses nombreuses symétries, cette théorie permet de formuler des démonstrations complètement formelles de propriétés complexes des cartes planaires qui sont au cœur de la preuve formelle du théorème des quatre couleurs.

Cet exposé présente différents modèles de systèmes distribués. Ces modèles correspondent à différents niveaux d'abstraction et à différents niveaux de synchronisation entre les processus. Ces modèles sont étudiés à travers le problème de l'élection qui met en évidence les bons objets combinatoires pour les comprendre et comparer leur puissance. Cette étude permet d'obtenir une caractérisation des réseaux asynchrones qui communiquent par échange de messages en mode synchrone et admettant un algorithme d'élection (idem pour les réseaux fonctionnant suivant le modèle d'Angluin). Cette étude permet également d'obtenir une caractérisation des réseaux asynchrones qui communiquent par échange de messages en mode asynchrone et admettant un algorithme d'élection. Cet algorithme nécessite un nombre polynomial de messages de taille polynomiale alors que le précédent algorithme, du à Yamashita et Kameda, nécessite un nombre exponentiel de messages de taille exponentielle.

(Ce travail a été effectué en collaboration avec Jérémie Chalopin, CNRS-LIF-Marseille).

An enumeration algorithm on a graph is an algorithm which computes a bijection from the nodes of the graph to all natural numbers between 1 and the number of nodes. Mazurkiewicz's enumeration algorithm is a distributed algorithm which terminates for covering-minimal (non-ambiguous) graphs. In this talk, we present a complete development (using refinement) of this algorithm and a mechanical proof of its correction and termination.

This work was carried out in the RIMEL project supported by Agence Nationale de la Recherche

This is a discursive talk. That is, it shows no formulas, no theorems, no proofs. Instead it postulates. The postulates are, however firmly rooted, I think, in Vol.3 (Domains, Requirements and Software Design) of my book Software Engineering (Springer March 2006).

First I present a summary of essentials of domain engineering, its motivation, and its modelling of abstractions of domains through the modelling of the intrinsics, support technologies, management and organisation, rules and regulations, scripts, and human behaviour of whichever domain is being described. Then I present the essense of two (of three) aspects or requirements: the domain requirements and the interface requirements prescriptions as they relate to domain descriptions and I survey the basic operations that turn a domain description into a domain requirements prescription: projection, instatiation, determination, extension and fitting. We likewise may have time for me to also cover an essence of interface requirements: the merging of shared entities, functions, events and behaviours of the domain with those of the machine (i.e., the hardware and software to be designed).

An objective of the talk is to summarise my work in recent years. Another objective is make a plea for what I consider a more proper approach to software development.

Considering an asynchronous system made up of n processes and where up to t of them can crash, finding the weakest assumptions that such a system has to satisfy for a common leader to be eventually elected is one of the holy grail quests of fault-tolerant asynchronous computing. This talk is a step in such a quest. It has two main parts. First, it proposes an asynchronous system model, in which an eventual leader can be elected, that is weaker and more general than previous models. This model is captured by the notion of intermittent rotating t-star. An x-star is a set of x+1 processes: a process p (the center of the star) plus a set of x processes (the points of the star). Intuitively, assuming logical times rn (round numbers), the intermittent rotating t-star assumption means that there are a process p, a subset of the round numbers rn, and associated sets Q(rn) such that each set Q(rn) plus p is a t-star centered at p, and each process of Q(rn) receives from p a message tagged rn in a timely manner or among the first (n-t) messages tagged rn it ever receives. The star is called t-rotating because the set Q(rn) is allowed to change with rn. It is called intermittent because the star can disappear during finite periods. This assumption, not only combines, but generalizes several synchrony and time-free assumptions that have been previously proposed to elect an eventual leader (e.g., eventual t-source, eventual t-moving source, message pattern assumption). Each of these assumptions appears as a particular case of the intermittent rotating t-star assumption. The second part of the talk presents an algorithm that eventually elects a common leader in any system that satisfies the intermittent rotating t-star assumption. That algorithm enjoys, among others, two noteworthy properties. Firstly, from a design point of view, it is simple. Secondly, from a cost point of view, only the round numbers can increase without bound. This means that, be the execution finite or infinite, be links timely or not (or have the corresponding sender crashed or not), all the other local variables (including the timers) and message fields have a finite domain.

Un grand nombre de modèles ont été élaborés pour le calcul dans les systèmes distribués en présence de fautes. Tous ces modèles reposent sur deux principes fondamentaux :

1. les fautes sont définies en fonction de leur cause (asynchronisme ou panne)
2. les composants responsables des fautes (les coupables) sont identifiables et identifiés.

J'illustrerai cette nouvelle approche avec l'algorithme fondamental de Consensus que Leslie Lamport a proposé en 1989, l'algorithme PAXOS, en donnant une expression simple de cet algorithme et des conditions garantissant sa terminaison.