Séminaires 68NQRT - année 2004-2005

Given a set of observations of an existing concurrent system with repetitive sub-functions, we consider the construction of an MSC graph representing the functionality of the concurrent system. We first introduce a formal structure that we call "lattice of repetitive sub-functions". This lattice provides us with a global view of all the repetitive sub-functions of the system and all the compatible observations. Using the lattice, we are able to propose an algorithm that constructs the MSC graph representation of the system functionality in a more general context than in previously published work. (with H. Ural, H. Yenigun)

Fault tolerance has been a long standing necessity in system design and operation. In systems with memory (state), however, modular redundancy and other traditional approaches to fault tolerance are undesirable not only because they are expensive but also because they rely heavily on the assumption that the error-correcting (e.g. voting) mechanism is fault-free. This talk presents a general framework that systematically addresses these issues in fault-tolerant discrete-time dynamic systems. Our approach replaces the original system with a redundant implementation in which the state and next-state transition mechanism of the original system are encoded. Error detection, correction and/or reconfiguration are then based on detecting and identifying violations on the state encoding of this redundant implementation. One of the implications and advantages of this approach is that, unlike traditional methodologies that rely on concurrent checking at the end of each time step, this approach allows the construction of redundant systems in which detection and identification of errors is based on non-concurrent (e.g. periodic) checks. In the resulting design, the checker can operate at a slower speed than the rest of the system, which relaxes the stringent requirements on its reliability. We demonstrate this approach in the context of linear dynamic systems and arbitrary finite-state machines. We also discuss how our framework can handle failures in the error correction mechanism, enabling in this way the construction of reliable systems exclusively from unreliable components. In particular, we construct reliable LFSMs using unreliable XOR gates and voters in a way that requires only a bounded amount of redundancy per machine and achieves arbitrarily low probability of failure during any finite time interval. The talk will conclude with open problems and directions for future research.

Hypernets, a new framework to express systems of distributed agents, adds the ambient-like mobility features to Petri nets. This is achieved as follows:

• hypernet consists of a set of agents,
• each agent is represented by an open Petri net,
• agents, as open Petri nets, exchange messages between other agents
• the messages are also agents.

• hierarchical organisation: agents contain as tokens other agents,
• modularity: agents are strucutured into modules, each module devoted to elaboration of agents of a special kind

The Object Management Group's Model Driven Architecture (MDA) paradigm is an approach to the development of software, based on the separation between the specification of the systems and their implementation using specific platforms. This workshop focuses on the scientific and practical aspects related with the adoption of Model Driven Development (MDD) methodologies (notation, process, methods, and tools) for supporting the construction of pervasive and embedded software.
Le programme de la journée est disponible sur la page du Workshop.

Les logiques spatiales sont des langages d'assertions permettant d'exprimer des propriétés ayant trait à la structure interne (ou configuration spatiale) des objets observés. Ces formalismes ont été mis en avant dans des contextes divers: 1/ exprimer des requètes sur des données semi-structurées (documents XML); 2/ raisonner sur des programmes manipulant des pointeurs; 3/ spécifier la "structure d'interaction" de systèmes distribués et mobiles (décrits dans des modèles algébriques tels que CCS, le pi-calcul, ou les Mobile Ambients). L'exposé présentera ce qui est commun à ces différentes logiques spatiales, pour mettre ensuite l'accent sur les logiques spatiales "dynamiques", qui correspondent au troisième point ci-dessus. On présentera des résultats portant sur l'expressivité et le pouvoir de séparation des logiques spatiales pour la concurrence. Ces résultats permettent en particulier de positionner ces formalismes par rapport aux outils classiques pour raisonner sur la concurrence (bisimulation, logiques modales). Ils permettent aussi de déduire des propriétés de décidabilité pour des questions liées à la logique.

La programmation par contraintes est un sujet de recherche qui tire profit de nombreuses autres disciplines : mathématiques discrètes, analyse numérique, intelligence artificielle, recherche opérationnelle et calcul formel. Elle a prouvé son intérêt et son efficacité dans de nombreux domaines : optimisation combinatoire, finance, simulation et synthèse de composants, diagnostic de panne, biologie moléculaire, ou encore problèmes géométriques. Néanmoins, un certain nombre de limitations et de difficultés restent : comment concevoir des algorithmes génériques et stables, comment traiter efficacement les problèmes dynamiques, comment rendre accessible les concepts et les outils, ...

Depuis quelques années, nous plaidons pour l'utilisation de la notion d'explication pour la programmation par contraintes car elle permet, nous l'avons montré, de répondre de manière satisfaisante à ces limitations. On peut considérer les explications comme une trace explicite et limitée du fonctionnement interne du solveur de contraintes. Nos travaux dans ce domaine nous ont conduit a non seulement développer les aspects théoriques des explications (permettant ainsi de caractériser précisément leur nature dans le processus de résolution) et à étudier différentes techniques de calcul et propositions d'implémentation (en fournissant en particulier le système PaLM : un solveur de contraintes avec explications), mais aussi et surtout à étudier leurs différentes utilisations. Les utilisations des explications sont en effet très variées. Une application évidente et directe consiste à les utiliser pour informer l'utilisateur des justifications de l'état courant du problème (résultat des actions du solveur de contraintes). Cette information peut aussi être utilisée pour résoudre des problèmes dont le système de contraintes évolue au cours de la résolution (ce qu'on appelle les problèmes dynamiques). On obtient alors un solveur de contraintes véritablement incrémental (acceptant aussi bien ajout que retrait de contraintes en cours de résolution). D'autres applications des explications concernent la modification des algorithmes classiques de résolution de problème avec contraintes. En effet, une véritable évolution de la programmation par contrainte peut être obtenue en utilisant à chaque instant de la résolution (pour avancer dans la recherche, pour sortir d'une impasse, ...) l'information apportée par les explications. On assiste alors à une véritable évolution de la programmation par contraintes. Cette évolution a été baptisée e-constraints (explanation-based constraint programming - programmation par contraintes basée sur les explications).

Nous présenterons à la fois les principaux résultats obtenus et les diverses perspectives dans le domaine en montrant ainsi comment ce récent sujet de recherche a ouvert de nouvelles voies et semble promis à un bel avenir.

We study the class of lazy linear hybrid automata with finite precision. The key features of this class are:

1. The state of the system is observed and the mode changes are actuated at discrete time points.
2. The values of the continuous variables can be measured only with finite precision.
3. The transition guards are finite conjunctions of linear constraints.
4. There are (bounded) delays associated with the observation of the states as well as the rate changes effected through mode switchings.

Bruyère et Carton ont introduit des automates acceptant des mots indexés par des ordres linéaires. Ces structures linéaires contiennent les mots infinis, bi-infinis, les mots indexés par des ordinaux et leurs miroirs. Des expressions rationnelles ont été introduites et le théorème de Kleene a été généralisé pour les mots indexés par des ordres linéaires dispersés, i.e. ne contenant pas de sous-ordre dense.

On montre que le complément d'un ensemble rationnel de mots indexés par des ordres linéaires dispersés est rationnel. Pour obtenir ce résultat, on développe une structure algébrique qui étend la reconnaissance classique par demi-groupes finis. On généralise les demi-groupes aux diamant-demi-groupes et on prouve qu'un ensemble est rationnel ssi il est reconnu par un diamant-demi-groupe fini. On étend également le théorème de Schutzenberger sur les langages sans étoile : un ensemble de mots indexés par des ordres linéaires dispersés est sans étoile si et seulement s'il est reconnu par un diamant-demi-groupe fini apériodique.

A data word is a word where every position has - apart from the usual letter from a finite alphabet A - an associated data value from an infinite set D. We reason about data words using first-order logic, where the data values can be accessed only by verifying if two positions have the same data value.

We show that satisfiability is decidable for formulas with two variables, and the obtained languages correspond to vector addition systems with states. When three variables are allowed, satisfiability becomes undecidable.

Joint work with Claire David, Anca Muscholl, Thomas Schwentick, Luc Segoufin

Dans cet exposé nous considérons le problème de description des séries formelles qui sont des séries génératrices de systèmes dynamiques affines polynomiaux. Nous introduisons les notions de grammaires pondérées de multi-ensembles et des automates pondérés de multi-ensembles. Nous montrons que les séries génératrices de systèmes dynamiques polynomiaux sont engendrées par de telles grammaires. Nous conjecturons également que toute série formelle engendrée par une grammaire pondérée de multi-ensembles est une série génératrice d'un système dynamique polynomial.

Dans cet exposé nous présentons un système de types prescriptif pour la programmation logique avec contraintes. Ce système combine polymorphisme paramétrique, sous-typage et surcharge afin d'obtenir la souplesse nécessaire afin de pouvoir typer les programmes usant de technique comme la méta-programmtion et l'utilisation conjointe de différents domaines de contraintes. Nous présenterons ensuite nos résultats sur la résolution des contraintes de sous-typage dans les quasi-treillis, qui constituent des structures de types riches, ajoutant ainsi de la souplesse au système de type. En particulier, le problème de satisfiabilité est montré NP-complet dans le cas de quasi-treillis dont les extrema sont des constantes en nombre fini.

La technologie LPV vise à faire de la vérification formelle à partir d'algorithmes de programmation linéaire. Elle a donné lieu à un dépôt de brevet puis à un essaimage universitaire: Valiosys. Après un rappel des principaux résultats scientifiques, je me propose de faire un bilan de la technologie après cinq ans d'application en milieu industriel: quels sont ses points forts et ses points faibles ? A quels problèmes s'applique-t-elle ? Quelles sont ses perspectives ?

Imagining what the nature of future viral attacks might look like is the key to successfully protecting against them. This paper discusses how cryptography and key management techniques may definitively checkmate antiviral analysis and mechanisms. We present a generic virus, denoted Bradley which protects its code with a very secure, high speed symmetric encryption. Since the main drawback of using encryption in that case lies on the existence of the secret key or information about it within the viral code, we show how to bypass this limitation by using suitable key management techniques. Finally, we show that the complexity of the Bradley code analysis is at least as high as that of the cryptanalysis of its underlying encryption algorithm.

A logic program consists of a logic component and a control component. The former is a specification in predicate logic whereas the latter defines the order of sub-goal selection. The order of sub-goal selection is often controlled with delay declarations that specify that a sub-goal is to suspend until some condition on its arguments is satisfied. Reasoning delay declarations is notoriously difficult for the programmer and it is not usual for a program and goal to reduce to a state that contains a sub-goal that suspends indefinitely. Suspending sub-goals are usually unintended and often indicate an error in the logic or control. A number of abstract interpretation schemes have therefore been proposed for checking that a given program and goal cannot reduce to such a state. This talk considers a reversal of this problem, advocating an analysis that for a given program infers a class of goals that do not lead to suspension. During the talk I will attempt to demonstrate such a reversed analysis and explain how it has been used to locate bugs in real programs.

Web services are network-based software components deployed and accessed through the Internet using standard interface description languages and uniform communication protocols. Each service solves a precise task, and may communicate with possible mates by exchanging messages.

Formal methods, and in particular process algebra, provide an adequate framework to tackle different issues raised in the web services area. First, they provide an abstract way to describe services (or their interfaces). Hence, composition of interacting services can be formalised as well. In addition, process algebra are often equipped with automated reasoning tools which are useful to ensure the correct development of services or to check their compatibility. All these issues will be illustrated through examples of e-business services.

Number Decision Diagrams (NDD) are the automata-based symbolic representation for manipulating regular sets of integer vectors encoded as strings of digit vectors (least or most significant digit first). Since 1969, we know that any Presburger-definable set (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a NDD, and efficient algorithm for manipulating these sets have been recently developed. However, the problem of deciding if a NDD represents such a set, is a well-known hard problem first solved by Muchnik in 1991 with a quadruply-exponential time algorithm. In this presentation, we show how to determine in polynomial time whether a NDD represents a Presburger-definable set, and we provide in the positive case a polynomial time algorithm that constructs from the NDD a Presburger-formula that defines the same set.

This presentation corresponds to the first 50 minutes of the workshop that will be given at JSI'05 paper.

ReactiveML est un langage de programmation dédié à la programmation de systèmes réactifs (e.g., simulation de systèmes dynamiques, interfaces graphiques, jeux video). Ce sont des systèmes "interactifs" au sens de Harel et Pnueli.

ReactiveML est fondé sur le modèle "réactif synchrone" introduit par F. Boussinot. Ce modèle permet de combiner les principes du synchrone --- composition parallèle synchrone de processus, communication par diffusion --- et des mécanismes de création dynamique.

Le langage est une extension conservative de Ocaml. Il ajoute des constructions supplémentaires pour décrire les comportements temporels des systèmes. Les programmes sont statiquement typés puis des mécanismes de compilation sont utilisés pour les traduire en Ocaml.

La première partie de cet exposé sera consacrée à la présentation du langage à partir d'un exemple. La seconde partie sera sur la description formelle de ReactiveML (sémantique, système de type et quelques techniques de compilation). Nous terminerons avec l'application à la simulation de réseaux mobiles ad-hoc.

Dans ma thèse, j'ai proposé une nouvelle approche le test statistique de logiciel à partir d'une description graphique des comportements du système à tester (graphe de contrôle, statecharts). Son originalité repose sur la combinaison de résultats et d'outils de combinatoire (génération aléatoire de structures combinatoires) et d'un solveur de contraintes, pour obtenir une méthode de test complètement automatisée. Contrairement aux approches classiques qui tirent des entrées, la génération aléatoire uniforme est utilisée pour tirer des chemins parmi un ensemble de chemins d'exécution ou de traces du système à tester. Puis, une étape de résolution de contraintes est utilisée pour déterminer les entrées qui permettront d'exécuter ces chemins. De plus, je montre comment les techniques de programmation linéaire peuvent améliorer la qualité d'un ensemble de tests.

Une première application a été effectuée pour le test statistique structurel défini par Thévénod-Fosse et Waeselynck (LAAS) et un prototype a été développé. Des expériences (plus de 10000 réalisées sur quatre fonctions issues d'un logiciel industriel) ont été effectuées pour évaluer notre approche et sa stabilité.

Ici un résumé plus étendu.

``(omega-)Regular model checking'' is the name of a family of symbolic techniques for analyzing infinite-state systems in which states are represented by (in)finite words, sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. In this context, the central problem is then to compute the iterative closure of a finite-state transducer.

A simple technique for iterating transducers is to use "widening", which amounts to computing successive approximations of the closure and to apply a simple extrapolation technique to these approximation in order to compute a sound guess of their limit. The first part of the talk is devoted to the use of such widening techniques in the case of systems using specific types of data for which regular model checking had not been used before (systems with integers, systems with reals, heterogenous systems, ...). The techniques we present build on earlier work, but exploit a number of new conceptual and algorithmic ideas, which experiments helped to induce.

In the second part of the talk, we address the problem of verifying liveness properties using the regular model checking framework. We show how this problem can be reduced to the one of computing the transitive closure of a transducer. The last part of the talk is devoted to a brief presentation of other existing techniques (tree regular model checking, abstract regular model checking, ...) and possible future work.

We discuss how the unfolding semantics of graph transformation systems can be used as a basis for their formal verification.

For general, possibly infinite-state, graph transformation systems one can construct finite under- and over- approximations of the (infinite) unfolding, with arbitrary accuracy. Such approximations can be used to check behavioural properties of a graph transformation system, expressed in a suitable temporal graph logic.

For finite-state graph transformation systems, a variant of McMillan's approach (originally developed for Petri nets) allows us to single out a finite under-approximation of the unfolding which is "complete", i.e., which provides an "exact" representation of the behaviour the original system as far as reachability properties are concerned. Some problems related to the construction of the complete prefix and to its use are discussed.

Nous nous intéressons à l'expressivité et la vérification de diverses structures communicantes par passage de messages, ce afin de modéliser les protocoles de communication.

Ces structures génèrent des exécutions sous forme de diagrammes de séquence (Message Sequence Charts MSC). Ce sont les automates communicants, les (C)MSC-graphes et les formules MSO. Les questions de vérification qui nous intéressent sont le model-checking, ainsi que l'implémentation des structures à choix globaux en automates communicants (choix locaux).

Nous exhibons une restriction assez expressive qui empêche l'indécidabilité de nombreux problèmes. Plus précisément, dès que les communications d'un langage peuvent être réordonnées pour qu'il y ait toujours au plus K messages en transit, nous montrons comment représenter ce langage par un ensemble régulier. Sous cette restriction, nous montrons la décidabilité d'une nouvelle logique, celle des templates MSCs.

PROUVÉ est un projet RNTL sur trois ans qui réunit CRIL Technology, France Télécom R&D, INRIA Lorraine, LSV et VERIMAG. Le projet porte sur la vérification de protocoles cryptographiques. Le point de départ du projet est une critique des méthodes existantes de vérification de protocoles cryptographiques :

• l'absence d'un langage d'entrée commun et d'une sémantique commune des outils de vérification existants
• des langages de spécification de protocoles trop simples ou trop abstraits
• une abstraction des méthodes de chiffrement qui est trop éloignée des vraies implémentations de protocoles

• développement d'un langage de spécification de protocoles cryptographiques expressif avec une sémantique précise, et d'un langage générique de propriétés de protocoles dans lequel peuvent s'exprimer de nombreuses variantes des propriétés classiques
• intégration des outils existants de vérification issus des laboratoires partenaires du projet dans une boîte d'outils, en particulier développement des traducteurs du langage de spécification et du langage de propriétés vers les langages d'entrée des outils
• vérification de protocoles cryptographiques sous affaiblissement de l'hypothèse du chiffrement parfait, en particulier le remplacement de nonces par des timestamps ou des compteurs, et prise en compte des propriétés algébriques des primitives cryptographiques
• développement d'une interface commune avec une présentation uniforme de preuves et d'attaques

Protocols may contain parameters that are chosen from a wide range or are unbounded, leading to infinite state systems. This makes their verification difficult. However, techniques and tools are now being developed for the verification of parametric and infinite state systems. We explore the use of one such tool, FAST, for verifying several properties of the stop-and-wait class of protocols.

Security properties are profitably expressed using notions of contextual equivalence, and logical relations are a powerful proof technique to establish contextual equivalence in typed lambda calculi. Through Sumii and Pierce's cryptographic lambda-calculus, one could apply the technique of logical relations to the verification of security protocols. Indeed, Sumii and Pierce define a series of operational logical relations for their language, while we shall present some logical relations based on denotational models. We start with a Kripke logical relation for Pitts and Stark's nu-calculus, which aims at dealing with dynamic name creation (key generation) and can be regarded as a syntactical subset of the cryptographic lambda-calculus. This logical relation is derived from the general logical relations for monadic types by Goubault-Larrecq et al., and it identifies Pitts and Stark's operational logical relation for the nu-calculus, hence it is sound and complete (w.r.t. contextual equivalence) up to first-order types. To get the completeness for all types, we appeal to the notion of lax logical relations. We define logical relations which are lax at encryption and function types but strict (non-lax) at various other types, and show that they are sound and complete for contextual equivalence at all types.

This talk includes some joint work with Jean Goubault-Larrecq, Slawomir Lasota and David nowak.