Séminaires 68NQRT - année 2003-2004
Je décris l'outil PathCrawler de génération automatique de tests structurels de chemin de programmes C. PathCrawler prend en entrée le code source et la description des entrées légitimes du programme à tester et produit une suite de test couvrant 100% des chemins faisables. Il adopte une approche "mixte" combinant l'analyse statique et l'exécution de code instrumenté de façon à éviter les inconvénients des approches purement statiques ou dynamiques. Au lieu d'être basé sur le graphe de contrôle, PathCrawler construit itérativement le graphe des chemins faisables d'exécution. Une analyse statique globale complexe est remplacée par de nombreuses analyses locales exactes, ce qui simplifie le traitement des alias et la détection d'infaisabilité. La stratégie de recherche d'un nouveau cas de test est basée sur la structure des chemins déjà couverts, permettant une implémentation efficace en programmation par contraintes.
J'illustre la méthode de base sur un exemple représentatif de fonction C. Ensuite, j'expose le traitement des alias et, finalement, je mentionne les possibilités d'extension que nous étudions.
A formula of the form BX.f(X) is true when there is a finite bound on the size of sets X that satisfy f(X). We consider monadic second-order logic extended with the B quantifier. Some decidability results for trees are presented.
De nos jours, les protocoles de sécurité (ssh, https,...) sont intensivement utilisés. Nous nous intéressons à la vérification de tels protocoles d'un point de vue symbolique : même si l'on suppose que les primitives cryptographiques utilisées sont parfaites, des failles peuvent néanmoins intervenir à cause de la parallelisation des sessions. C'est ce qu'on appelle par exemple les "man in the middle attacks". Nous avons pour objectif de vérifier qu'un protocole ne comporte pas de telles failles.
D'un point de vue général, même dans des cas très restreints, ce problème est indécidable pour un nombre non borné de sessions. Nous utilisons alors une méthode introduite par Genet et Klay utilisant des approximations et des abstractions. Nous montrerons comment cette méthode peut être automatisée pour devenir semi-algorithmique et pour fournir, en pratique, des résultats concluants. Nous présenterons aussi l'outil TA4SP développé dans ce cadre et utilisant un langage de spécification (HLPSL) de haut niveau.
Nous commencerons par introduire une relation de raffinement exprimée par une relation de simulation entre un système concret et un système abstrait respectant certaines propriétés ( non-observabilité des nouvelles transitions, non-introduction de cycles ou de blocages par les nouvelles transitions, ...). L'avantage principal de ce raffinement est qu'il garantit la préservation de la LTL. Dans certains cas, il est de plus possible de raffiner - conjointement au système - les propriétés à vérifier, avec un coût de vérification réduit.
Nous traiterons ensuite la question des systèmes spécifiés sous la forme système à composants synchronisés. L'objectif consiste à étudier le raffinement du système complet en étudiant uniquement le raffinement de ses composants. L'étude du raffinement de chacun composant nécessite la prise en compte de l'environnement du composant, sous la forme d'un composant sous-contexte. Une relation de raffinement affaiblie est alors donnée permettant de conclure à propos du raffinement du système complet. Nous montrerons aussi que certaines propriétés LTL peuvent se vérifier de manière compositionnelle, conjointement au raffinement ; ces propriétés étant soit locales à un composant, soit vérifiables sur les composants sous-contextes.
Pour finir, nous présenterons SynCo, un prototype mettant en oeuvre la démarche de vérification par raffinement des systèmes à composants synchronisés présentée dans cet exposé.
Ce travail a été réalisé avec Olga Kouchnarenko.
BZ-Testing-Tools est une méthode de génération automatique de tests fonctionnels aux limites utilisant la Programmation Logique avec Contraintes. Les techniques d'abstraction utilisées permettent de limiter l'explosion combinatoire du nombre d'états considérés en conservant l'indéterminisme de la spécification initiale. Les systèmes de contraintes issus des spécifications sont résolus par le solveur de contraintes ensemblistes CLPS initialement dédié à la résolution de problèmes combinatoires.
Nous présentons les travaux d'intégration réalisés sur le solveur CLPS qui s'articulent autour de la définition de structures relationnelles et de la mise en oeuvre de règles d'inférence spécifiques permettant de maintenir la consistance des systèmes de contraintes manipulés. L'application du solveur CLPS à la problématique de génération de tests nous a aussi conduit à renforcer les règles existantes en les outillant par une nouvelle représentation de domaines et par l'intégration de contraintes gardées pour l'évaluation des contraintes n-aires. Nous rapportons les résultats obtenus à l'échelle industrielle et nous donnons les perspectives liées aux évolutions du solveur CLPS
Depuis la première version de l'article fondateur de Chandra et Toueg en 1991, intitulé "Unreliable failure detectors for reliable distributed systems", le concept de détecteurs de fautes (oracles) a été très étudié, investigué et analysé. Ceci n'est pas surprenant dès que l'on prend conscience que la détection des fautes surgit à tout moment dans la conception, l'analyse et la mise en oeuvre de de la plupart des algorithmes répartis que l'on rencontre au coeur des systèmes distribués.
La littérature sur le sujet est généralement très technique et se trouve principalement dans les revues et les conférences qui présentent une orientation théorique très marquée. Le but de l'exposé est d'offrir une introduction simple au concept de détecteur de fautes, destinée aux personnes qui désirent en comprendre les principes, la puissance et la limitation. Pour atteindre ce but, l'exposé présente les motivations qui ont conduit au concept de détecteur de fautes, et les illustre avec des problèmes fondamentaux du calcul réparti.
Nous nous intéressons à l'analyse statique de logiciels comportant des objets alloués dynamiquement sur un tas et repérés par des pointeurs. Le but final étant de trouver des erreurs dans un programme (problèmes de déréférencements, d'alias...) ou de prouver qu'un programme est correct (relativement à ces problèmes) de façon automatique.
Ishtiaq, O'Hearn, Reynolds & al ont récemment développé des logiques de fragmentation qui sont des logiques de Hoare avec un langage d'assertions/de prédicats permettant de démontrer qu'un programme manipulant des pointeurs sur un tas est correct.
Nous présenterons une logique de fragmentation que nous avons enrichie de points fixes ainsi que les weakest liberal preconditions (wlp) et strongest postconditions (sp) pour chaque commande. Cette ajout de pointfixes nous permet la définition de formules récursives ainsi que l'expression des "wlp" et "sp" dans le cas des boucle "while".
Nous nous proposons ici d'adapter la theorie classique de Ramadge et Wonham en restreignant l'espace des superviseurs aux reseaux de Petri bornes et etiquetes injectivement. La classe de leurs graphes de marquage etant une sous-classe stricte de la classe des automates finis, on perd necessairement en generalite.
Nous montrons qu'en restreignant encore davantage les reseaux et plus precisement en leur imposant d'etre distribuables, on gagne pourtant sur un aspect crucial, puisque on aboutit automatiquement a des superviseurs qui sont a la fois asynchrones et distribues.
De facon plus precise on a sur chaque site un controleur local qui est un automate fini, et ces controleurs locaux communiquent par messages asynchrones. Si le systeme a controler est aussi un systeme d' automates communicants, a raison d'un automate par site, alors automates locaux et controleurs locaux agissent de facon synchrone sur chaque site, toutes les autres communications etant totalement asynchrones. L'expose est en quatre parties. La premiere partie rappelle les resultats de Ramadge et Wonham. La seconde partie adapte ces resultats aux reseaux bornes en posant pour chaque type de probleme de controle (controle exact, controle optimal, tolerance) un probleme correspondant sur les reseaux bornes (et non necessairement distribuables). Dans la troisieme partie, nous montrons qu'a toute paire de langages rationnels R et L on peut associer constructivement le plus petit langage de reseau borne N contenant R et tel que les marquages de N atteints par des mots de L soient bornes. On en deduit des procedures de decision pour les problemes precedents. La quatrieme partie de l'expose adapte tout ce qui precede aux reseaux distribuables, et fournit ainsi une technique novatrice pour la construction de superviseurs asynchrones.
L'analyse de forme (Shape Analysis) consiste à analyser la structure du tas mémoire et ses propriétés durant l'exécution d'un programme. Il permet de vérifier des propriétés du type: étant donné en entrée une liste simplement chaînée, tel algorithme de tri retourne une liste simplement chaînée. Nous présenterons une approche générale à ce problème, introduite en 2000 par Sagiv, Reps and Wilhehlm, qui consiste à représenter des ensembles de configurations mémoire par des structures logiques, et à utiliser la logique du premier ordre trivaluée avec fermeture transitive.
Nous montrerons aussi que cette approche permet l'utilisation de méthodes classiques d'analyse interprocédurale.
Les automates cheminants permettent de décrire des langages d'arbres au même titre que les automates d'arbres classiques. Un automate cheminant est une machine à état fini parcourant l'arbre à étudier en choisissant à chaque pas une transition en fonction de la configuration locale de l'arbre. Ces automates peuvent en particulier effectuer des parcours en profondeur d'abord.
Plusieurs questions concernant ce formalisme sont restées sans réponse jusqu'à présent:
- les automates cheminants peuvent-ils décrire les langages réguliers d'arbres ?
- les automates cheminants peuvent-ils être déterminisés ?
La conjecture communément admise est que la réponse à ces deux questions est négative. Dans cet exposé, nous établirons que c'est effectivement le cas pour la seconde.
Travail en collaboration avec Mikolaj Bojanczyk.
In this study, we are interested in the control of Concurrent Discrete Event Systems defined by a collection of local sub-plants that interact with each other. We investigate the computation of the supremal controllable language contained in the one of the specification. The specification is decomposed according to the structure of the plant leading to ``sub-specifications''. Further the behavior of these sub-specifications is resctricted so that they respect a new language property for discrete event systems called {\it partial controllability condition}. It is finally, shown that based on these restricted sub-specifications, a supervisor can be derived such that the behavior of the controlled plant corresponds to the supremal controllable language contained in the one of the specification. This computation is performed without having to build the whole plant, hence avoiding the state space explosion induced by the concurrent character of the plant.
A Number Decision Diagram (NDD) is an automaton that represents regular set of integer vectors encoded as strings of digit vectors (least or most) significant digit first.
In this presentation, we provide an algorithm for computing the convex hull of the set represented by a NDD. As any Presburger-definable set (a set defined in the first additive theory of the integers) can be efficiently represented by such an automaton, we deduce an algorithm for automatically computing the convex hull of any set of vectors defined by such a formula.
The convex hull is central in many applications: in the area of abstract interpretation, controller synthesis, test-generation and verification.
Example: Let X be the set defined by the following Presburger formula F: F(x,y):=\exists z. (x>y AND x+y=2.z) The convex hull is defined by x >= y+2 and not by x >= y+1. After the presentation, you should be able to compute this constraint automatically.
At the Software Composition Group we recently work on two new language constructs: traits and classboxes which two important aspects of software structuration: a trait acts as a unit of reuse and a classbox act as a unit of scoping. This talk will present both.
Traits: Composable Unit of Reuse. We have been developing a simple compositional model for structuring object-oriented programs, which we call traits. Traits are essentially groups of methods that serve as building blocks for classes and are primitive units of code reuse. In this model, classes are composed from a set of traits by specifying glue code that connects the traits together and accesses the necessary state. Unlike mixins and multiple inheritance, traits do not employ the inheritance as the composition operator. Instead, traits composition is based on set of composition operators that are complementary to inheritance and result in better composition properties. We have implemented traits in Squeak, an open-source Smalltalk dialect. We are working on a port of traits to C# via a collaboration with Microsoft Research and Perl designers decided to include traits in Perl 6 (under the name roles).
Classboxes: A Minimal Module Model Supporting Local Rebinding. Classical modules systems support well the modular development of applications but lack the ability to add or replace a method in a class that is not defined in that module. But languages that support method addition and replacement do not provide a modular view of applications, and their changes have a global impact. The result is a gap between module systems for object-oriented languages on one hand, and the very desirable feature of method addition and replacement on the other hand. To solve these problems we present classboxes, a module system for object-oriented languages that allows method addition and replacement. Moreover, the changes made by a classbox are only visible to that classbox (or classboxes that import it), a feature we call local rebinding. To validate the model, we have implemented it in the Squeak Smalltalk environment, and performed experiments modularizing code.
La sémantique d'un réseau de Petri est habituellement définie sous la forme de son graphe des marquages (ou configurations) ou bien à partir de certaines abstractions de celui-ci (obtenues par exemple par dépliage comme pour les structures d'événements). Le comportement d'un réseau est donc donné par un automate, généralement infini, dans lequel une transition du réseau est représentée par une relation binaire entre configurations.
Très tôt il est apparu utile de s'intéresser à des généralisations de ce modèle en autorisant les relations précédentes à prendre leurs valeurs non nécessairement dans l'algèbre de Boole à deux éléments (la transition existe ou non) mais plus généralement dans un demi-anneau ou une algèbre de Kleene. En particulier l'utilisation de demi-anneaux spécifiques (dioïdes) s'est avérée très utile pour l'étude qualitative de systèmes à événements discrets. De façon semblable nous avons introduit une notion paramétrique de réseaux de Petri dans laquelle les contenus de places et les relations de flot prennent leurs valeurs dans une algèbre particulière. Ces algèbres, qualifiées d'algèbres de Petri, permettent d'effectuer les opérations associées au token game des réseaux de Petri et assurent que la règle de franchissement ainsi obtenue est associative et réversible. On peut alors internaliser une séquence de tels franchissements à condition de munir l'algèbre de Petri d'une multiplication afin de décrire l'effet d'une succession de transitions. On obtient ainsi une classe de demi-anneaux qu'on peut caractérider. Le graphe de marquage d'un réseau peut alors ce décrire comme un automate à coefficient dans un tel demi-anneau.
It is well known that fast and accurate fault diagnosis is important for maintaining the high-standard performance and safety of a target system. So far there is a large volume of literature on fault diagnosis, which can be roughly categorized either from the representation aspect, e.g the degree of comprehensiveness of our knowledge on the target system in model-based or model-free approaches; or from the implementation aspect, e.g. centralized, decentralized, distributed and hierarchical approaches. In this talk I will focus on a model-based distributed approach, which has demonstrated advantages in space/time complexity and scalability issues involved in diagnosis.
I will first propose a general framework for distributed diagnosis. More specifically, each diagnosis instance consists of two phases: local estimation, and inter-component communication for consistency. For the latter phase the concepts of supremal global support (for global consistency) and supremal local support (for local consistency) will be introduced. Then I will provide a computational procedure CPGC for achieving supremal global support, and CPLC for supremal local support. The two supremal supports lead to distinct distributed diagnosis problems. It turns out that supremal global support results in better quality of diagnosis in the sense that fewer fault candidates are reported in each diagnosis instance; but supremal local support results in a computational procedure that is better scalable, although we may face a challenging problem on the termination issue. In practice the two supremal supports may be combined for a satisfactory tradeoff between quality of diagnosis and scalability of the diagnoser. An ideal case is that we can attain the quality and scalability at the same time, which leads to another interesting problem (partially solved at the moment), namely under what condition(s) global consistency is identical to local consistency. Finally, to reduce time complexity of CPGC, a hierarchical computational procedure is proposed, which is then utilized in multi-resolution diagnosis. Although high-level abstract models for hierarchical computation need extra memory, our numerical results show that the overall space complexity as measured by memory usage in storing both the models and the intermediate computational results is no worse (and in some cases better) than the space complexity in our non-hierarchical approaches.
Les réseaux de Petri T-Temporels consituent une extension temporelle des réseaux de Petri. La méthode classique d'analyse de tels réseaux est basée sur la technique du graphe des Classes (B.Berthomieu et M.Diaz) mais elle est inadaptée pour la vérification de certaines propriétés qualitatives (branchement) et quantitatives. Cet exposé décrit une méthode permettant de calculer plus efficacement l'espace d'état d'un réseau de Petri T- Temporel borné ainsi que sa traduction en automate temporisé. Cette approche permet ainsi d'envisager la vérification de propriétés quantitatives.
The application field for static analysis of Java programs is getting broader, ranging from compiler optimizations (like dynamic dispatch elimination) to security issues. Many of those analyses include type analyses. We propose a `generic' framework, which improves on previous type analyses by introducing structural information. Moreover, structural information allows us to easily extend the framework to perform many different kinds of analyses.
The framework is based on the abstract interpretation methodology. It is composed of a standard semantics, a family of abstract domains, an abstract semantics based on these domains and a post-fixpoint algorithm to compute the abstract semantics. The analysis is limited to a representative subset of Java, without concurrency.
A prototype of the framework allows us to illustrate the accuracy and the efficiency of the approach (for moderately sized programs).
We show a relationship between transition systems (2-structures), used in the study of concurrency, and orthomodular posets, related to quantum logic. We present some positive results in the field and recall a conjecture.
Model Integrated Computing (MIC) is a methodology developed over the last decade for applying modeling to systems design. MIC recasts a problem domain into a modeling problem by constructing a domain specific modeling language (DSML) for that domain. The fundamental concepts for constructing these DSMLs along with the major tools that realize these concepts will be discussed. Current research aims to extend the basic MIC concepts in several key areas including multiple aspect modeling, metamodel composition, and libraries of semantic units. The synchronous language Signal has been used as a non-trivial test bed for these advances in MIC, and the results of applying these concepts to Signal will be presented.
PowerPoint slides.
L'exposé commencera par une description du langage de spécification TLA+ et du vérificateur de modèles (model checker) associé TLC. L'expérience acquise en utilisant ces deux outils -à Compaq/HP et à Intel- pour écrire et mettre au point des spécifications de haut-niveau sera présentée et des leçons en seront tirées. (Il est important de noter que beaucoup d'idées reçues n'ont rien à voir avec les spécifications de haut-niveau.)
L'exposé sera en fait en français.
Les systèmes polygonaux à inclusions différentielles (SPDIs) sont des systèmes planaires non déterministes qui peuvent être représentés par des inclusions différentielles constantes par morceaux. Cette exposé porte sur les aspects théoriques et pratiques des SPDIs tels que le problème de l'atteignabilité et de la construction du portrait de phase. Nous montrons que le problème de l'atteignabilité est décidable pour les SPDIs. Ensuite, nous construisons le portrait de phase des SPDIs. Nous savons identifier les noyaux de viabilité des boucles simples. Il s'agit des ensembles de points initiaux de trajectoires restant dans la boucle. Nous introduisons la notion de noyau de controlabilité de boucles simples comme l'ensemble des points atteignables les uns à partir des autres par des trajectoires qui restent dans le noyau. Nous proposons un algorithme pour calculer ces deux noyaux. Enfin, nous étudions la décidabilité du problème de l'atteignabilité pour d'autres classes de systèmes hybrides à deux dimensions.
In contexts where data are replicated among different sources and copies of same data are different because of data errors, comparisons can be used to reconcile such copies. Best quality copies can be selected or constructed in order to correct other copies. Record matching algorithms can support the task of linking different copies of the same data in order to engage reconciliation activities; for instance, a periodical running of record matching algorithms can be performed in order to reconcile copies with different quality. Nevertheless, the extensive running of such algorithms is typically performed in fixed instants. This allows for periods in which the quality of data can deteriorate, while no quality improvement action is performed on data. We describe a platform for dealing with data inconsistencies in contexts where data are replicated among heterogeneous and distributed sources. The strategy underlying the proposed platform complements a periodical record matching activity with an "on-line" improvement, performed at query processing time. We experimentally show the feasibility and effectiveness of our approach by applying it to databases from the Italian public administration.
Le problème de contrôle auquel cet exposé s'intéresse est le suivant: étant donné un système fait de plusieurs processus communicants et une spécification des bons comportements du système, trouver pour chaque pocessus un contrôleur (dit local) inhibant certaines de ses actions, de telle sorte que le système contrôlé satisfasse la spécification. Ce problème se modélise en termes de jeux:système contre environnement. Trouver un contrôleur distribué revient alors à trouver une sratégie gagnante pour le système.
Plusieurs travaux antérieurs (Pnueli Rossner 89, Madhusudan Thiagarajan 02, Bernet-Janin-Walukiewicz 04) montrent que déterminer l'existence d'une stratégie gagnante est en général indécidable. Nous introduisons une nouvelle modélisation du problème de contrôle, et une nouvelle notion. de stratégie, qui diffèrent des précédentes tentatives par la notion de mémoire utilisable. Nous montrons que dans ce cadre, plusieurs problèmes deviennent décidables.
On appelle "grammaire de dépendance" (GD) toute grammaire formelle qui affecte les arbres de dépendances aux phrases engendrées. Un arbre de dépendances d'une phrase est un arbre dont les noeuds sont les mots de la phrase. Ainsi les GDs formalisent la syntaxe des langues naturelles explicitement en termes des relations binaires entre les formes. La plupart des grammaires formelles expriment les dépendances projectives (continues) au moins sous une forme implicite : les têtes de la théorie X-bar, LFG, SPSG/HPSG, TAG, etc. Or, pour exprimer les dependances discontinues on étend les grammaires formelles par des moyens très expressifs ce qui rend complexe (voire indécidable) le probleme du parsing.
Dans cet exposé je définis les GDs en forme de grammaires catégorielles du 1er ordre munies des contraintes simples sur l'ordre des mots : {\it grammaires catégorielles de dépendance} (GCD). Tout comme les grammaires catégorielles, les GCD sont complétement lexicalisées (déterminent les types des mots et non des règles de réécriture). Elles sont suffisamment expréssives pour naturellement formaliser la syntaxe de surface des langues naturelles, à plusieurs constructions exotiques et contestables près), disposent d'un algorithme polynomial du parsing et sont apprenables à partir d'exemples positifs en cas de lexiques rigides.
Le but de cet exposé est de définir et d'illustrer les GCD, de les comparer avec plusieurs autres grammaires formelles, de caractériser leur complexité et, finalement, d'ébaucher leur lien avec la sémantique linguistique formelle.
Several types of term rewriting systems can be distinguished by the way their rules overlap. In particular, we define the classes of prefix, suffix, bottom-up and top-down systems, which generalize similar classes on words. Our aim is to study the derivation relation of such systems (i.e. the reflexive and transitive closure of their rewriting relation) and, if possible, to provide a finite mechanism characterizing it. Using a notion of rational relations based on finite graph grammars, we show that the derivation of any bottom-up, top-down or suffix systems is rational, while it can be non recursive for prefix systems.
Programs, processes, resources, and storage heaps are often modelled by graphs, and correctness properties are validated on the graphs. Separation logic, developed by O'Hearn, Reynolds, and Yang, is a logic for writing compositional correctness proofs of such graphs.
In this presentation, we introduce separation logic, show how to make compositional correctness proofs, and apply the logic to programs that manipulate storage heaps and shared resources.
Les diagrammes de suites de messages (Message Sequence Charts, MSC en abrégé) constituent un formalisme graphique (recommandé par International Telecommucation Union) utilisé dans le domaine des télécommunications, notamment dans des étapes initiales de spécification de protocoles. Un formalisme étendu qui permet de combiner les MSC à l'aide de la concaténation, du choix non déterministe et de l'itération est connu sous le nom de HMSC (High-level MSC). Un HMSC peut être donc représenté par un graphe fini étiqueté par des MSC. Nous nous intéressons à des cas infinis de tels graphes, plus précisément aux "MSC infinis" qu'ils représentent. Nous étudions dans ce cadre la décidabilité du model-checking lorsque les propriétés à vérifier sont exprimées en logique monadique du second ordre.
De nombreux travaux portent actuellement sur l'étude des protocoles cryptographiques. Il y a deux raisons essentielles à cela :
- leur importance économique : il y a une demande forte de la part des industriels (France Telecom, Siemens,...) pour des méthodes permettant de garantir aux utilisateurs et aux développeurs qu'un protocole qui sera déployé sera effectivement sur ;
- la possibilité relativement récente de répondre à ces besoins de sécurité. Les méthodes formelles sont désormais suffisament matures pour pouvoir etre appliquées avec succès à ce type de problèmes.
Les langages de programmation modernes sont generalement dotes de systemes de modules. Ce sont des sous-langages dedies a la modularisation des gros programmes, c'est-a-dire leur decomposition en entites plus petites et comprehensibles individuellement. Parmi ces systemes de modules, celui de ML est l'un des plus sophistiques. En particulier, au niveau de l'abstraction de donnees, il permet de selectionner de maniere fine l'information visible dans chaque module par le reste du programme. De meme, grace aux foncteurs (fonctions d'ordre superieur sur les modules), les modules peuvent etre arbitrairement parametres par rapport a leur contexte d'utilisation.
Malgre ces points forts, le systeme presente encore au moins deux faiblesses importantes. La premiere est qu'il ne permet pas aux definitions mutuellement recursives de s'etaler sur plusieurs modules, ce qui gene souvent la modularisation. La seconde concerne la programmation incrementale, c'est-a-dire la possibilite de definir un module en le decrivant par des modifications a appliquer a des modules existants. Le systeme de modules de ML ne propose pas d'outil pour cela.
La notion de module mixin, apparue progressivement depuis les travaux de Bracha en 1992, semble a meme de resoudre ces problemes, sans pour autant abandonner les avantages mentionnes precedemment. Elle enrichit la notion habituelle de module par des constructions inspirees des langages orientes objets. Dans cet expose, nous presentons les modules mixins, ainsi que les difficultes liees a leur conception, leur typage et leur compilation.
Le calcul des Ambiants est aujourd'hui une référence en matière de modélisation des systèmes distribués et mobiles. Dans ce calcul, un ambiant représente une unité d'exécution et de migration nommée pouvant contenir elle-même d'autres ambiants. Dans ce cadre, des systèmes de types ont été développés pour assurer des polices de sécurité élémentaires exprimées indirectement via une classification des ambiants dans des "groupes". Nous présenterons une théorie alternative de "types dépendants" qui permet une plus grande flexibilité dans l'expression des polices de sécurité. Cette théorie a également l'avantage de simplifier la spécification des polices de sécurité et relègue la complexité inhérente à la vérification dans les règles de typage.
The model checking of counters systems often reduces to the effective computation of the set of predecessors pre^*(X) of a Saturated Digit Automaton (SDA) X (a.k.a Number Decision Diagram (NDD) [Boigelot, Wolper: ICALP'00]). Because there often exists an integer k>=0 such that pre^{<=k}(X)=pre^*(X) we will first look for an efficient algorithm to compute the SDA pre(X) in function of X. In general, such a computation is exponential in the size of X. In [Batziz Bultan: CAV03], the computation is proved to be polynomial for a restrictive class of deterministic counters systems. In this article we show that for any deterministic effective counters systems, the computation is polynomial. Then we describe the precise structure of the SDAs pre^{<=k}(X) in function of k. We provide two general conditions (one global and one local) for which this structure is rather a Binary Decision Diagam (BDD) than a general SDA opening the door to widening operators specialized to the SDA structure.
Once the set of finite graphs is equipped with an algebraic structure (arising from the definition of operations that generalize the concatenation of words), one can define the notion of a recognizable set of graphs in terms of finite congruences. Thus the class of recognizable sets depends on the signature of graph operations. We consider three signatures related respectively to Hyperedge Remplacement (HR) context-free graph grammars, to Vertex Replacement (VR) context-free graph grammars, and to modular decompositions of graphs. We compare the corresponding classes of recognizable sets. In the lecture, we will sketch the proof that for graphs without large complete bipartite subgraphs, HR-recognizability and VR-recognizability coincide. The same combinatorial condition equates HR-context-free and VR-context-free sets of graphs. If time permits we survey results showing that VR recognizability is a robust property in the sense that many variants of each signature yield the same notions of recognizability. This lecture is based on an article by B. Courcelle and Pascal Weil.
Résumé en ici en postscript.
The algorithmic theory of infinite games, initiated 40 years ago by Church, Büchi, Rabin, and others, attracts attention today as a framework which allows to move from verification to automatic synthesis of programs. We give a historical introduction, present the fundamentals, and discuss some challenges and perspectives.
It is well known that games with the parity winning condition of finite order admit positional determinacy: the winner can always use a positional (memoryless, history-free) strategy. Recently Grädel and Walukiewicz extended this result to suitably defined parity games over infinite alphabet. But variety of thepositionally determined games is in fact much larger.
Positional determinacy is helpful, in particular in the algorithmics of game solving. It would be nice to have some characterization of this property, e.g. in language-theoretic terms.
The starting point of our work comes from an observation that if edges rather than vertices are labeled then the parity condition (of finite order) still guarantees positional determinacy, but the other known examples loose this property. In turns out that, in fact, in the edge-labeled case the parity games of finite order are in a strong sense the only positionally determined games.
(joint work with Thomas Colcombet)
Mon exposé sera une introduction à la technique d'évaluation partielle dirigée par les types (TDPE). Je décrirai notamment une implémentation de cette technique pour le langage Objective Caml.
L'évaluation partielle désigne une transformation de programmes visant à en construire des versions spécialisées pour certains paramètres. D'un point de vue théorique, cette réduction de programme correspond à la notion de réduction forte (normalisation). La normalisation par évaluation est un algorithme particulièrement ingénieux pour réaliser cette tâche, qui a été utilisé dans plusieurs domaines (théorie des types, catégories, logique...) Un algorithme d'évaluation partielle reprenant les mêmes idées, appelé TDPE (Type Directed Partial Evaluation), a été présenté par Olivier Danvy. Cependant l'implémentation concrète de TDPE pose de nombreux problèmes, dont beaucoup ne sont pas encore résolus aujourd'hui. J'essaierai de vous montrer les différents aspects de ce problème en me basant sur mon expérience d'implémentation de TDPE pour le langage Objective Caml.
Cet exposé porte sur l'analyse statique par interprétation abstraite de spécifications temporelles. Lorsque les spécifications à vérifier sur un programme ne se limitent pas à des propriétés d'accessibilités, un analyseur classique est rapidement insuffisant même sur des exemples simples.
Nous présentons ici un formalisme d'"analyse guidée par une spécification" qui permet de déduire, d'une analyse initiale et d'une spécification, une seconde analyse qui peut être combinée avec la première pour orienter celle-ci vers la vérification de la spécification. Ce formalisme, appliqué dans la réalisation d'un analyseur-jouet, permet d'obtenir dans certains cas des résultats plus précis qu'un analyseur classique utilisant un domaine abstrait complexe.
We propose a combination of heuristic methods to prove properties of control signals for regular systems defined by means of affine recurrence equations (AREs). We benefit from the intrinsic regularity of the polyhedral model to handle parameterized systems in a symbolic way. Our techniques apply to safety properties. The general proof process consists in an iteration that alternates two heuristics. We are able to identify the cases when this iteration will stop in a finite number of steps. These heuristics apply successfully to concrete examples and led us to discover some errors in actual systems. These techniques have been implemented in a high level synthesis environment based on the polyhedral model.
In this paper we introduce the notion of weak endochrony, which extends to a synchronous setting the classical theory of Mazurkiewicz traces. The notion is useful in the synthesis of communication protocols for globally asynchronous, locally synchronous (GALS) systems. Here, the independence between various computations can be exploited to provide lighter, more flexible communication schemes that do not restrict the concurrency while still guaranteeing correctness.
Le problème du consensus est un problème fondamental auquel se trouve confronté tout concepteur d'applications ou d'intergiciel lorsque le support est un système réparti sujet à défaillances : Chaque entité propose une valeur et tous les processus non fautifs doivent se mettre d'accord sur une même valeur résultat, celle-ci devant bien sûr être l'une des valeurs d'entrées. Ce problème se trouve être un problème de base auquel se ramènent la plupart des problèmes d'accord (comme par exemple la diffusion atomique de messages ou la coordination d'actions réparties).
L'exposé visitera le problème dans le contexte des systèmes asynchrones qu'ils soient à mémoire partagée ou à passage de messages. Au cours de ses pérégrinations, la visite montrera les rapports étroits qui existent entre le consensus et les primitives de synchronisation (telles que Test&Set, Fetch&Add, ou Compare&Swap), l'universalité du consensus lorsqu'il s'agit de réaliser des objets fiables, la nécessité de réduire l'asynchronisme du système à l'aide d'oracles si l'on veut résoudre le problème en dépit des défaillances possibles des processus. Un accent particulier sera mis sur une approche nouvelle fondée sur des conditions qui restreignent les vecteur d'entrées. (Selon le temps, les questions et l'intérêt de l'auditoire on pourra également prendre le temps d'exhiber des rapports très étroits qui lient les problèmes d'accord rencontrés dans les systèmes répartis et les codes correcteurs d'erreur developpés en théorie de l'information.)
Une méthodologie qui combine vérification et test de conformité pour la validation de propriétés de sûreté de système réactifs sera présentée. Les propriétés sont d'abord vérifiées automatiquement sur la spécification du système. Des cas de test sont ensuite dérivés de la spécification et des propriétés, et exécutés sur une implémentation boîte noire du système. Les cas de tests générés cherchent à pousser l'implémentation à violer une propriété. Nous montrons qu'une implémentation est conforme à sa spécification si et seulement si elle passe tous les tests générés de cette manière.
Les canaux cachés sont des fuites d'informations non prévues dans un système, qui détournent généralement des ressources pour transférer secrètement un message. Ces canaux cachés sont une menace pour la sécurité, les performances, mais aussi la rentabilité d'un système.
Tous les standards en matière de sécurité recommandent d'appliquer des audits aux systèmes pour identifier ces canaux cachés à l'aide de méthodes "reproductibles". De nombreuses méthodes formelles s'appuyant d'une part sur un modèle des systèmes étudiés, et d'autre part sur un modèle de sécurité Bell & La Padulla ont été proposées. Le modèle de Bell & La Padulla indique quels utilisateurs sont autorisés a communiquer entre eux, et les approches basées sur ce modèle vérifient généralement qu'il n'existe pas de flots d'information (par exemple en utilisant une ressource partagée) entre deux utilisateurs qui ne sont pas autorisés à échanger de l'information.
Nous proposons une méthode pour détecter des canx cachés à partir d'un modèle de protocole défini par des scénarios. L'approche que nous proposons rompt avec la vision traditionelle Bell-La PAdulla, en supposant qu'un canal caché peut également apparaître entre deux utilisateurs qui sont autorisés à communiquer si la manière dont le protocole est utilisé est un phénomène observable.
Dans un premier temps, nous modélisons un canal caché comme un jeu, dans lequel une paire d'utilisateurs malicieux {S,R} cherche à transférer de l'information, tandis que le reste du protocole essaie de l'en empêcher. Les messages transférés sont codés par des choix de comportements à des instants précis, et décodés par des transducteurs dont le vocabulaire d'entrée est une observation du système. Nous montrons que si {S,R} possède une strategie gagnante dans ce jeu, et qu'il existe un décodeur pour le message transféré, alors il existe un canal caché dans le protocole modélisé.
Le model-checking classique consiste à vérifier qu'une propriété spécifiée dans une certaine logique est vérifiée le long de tous les chemins d'exécutions. Ici nous voulons vérifier qu'une propriété est vérifiée le long d'un chemin donné. Nous donnons différents résultats de complexité pour ce problème.
Nous considérons des réseaux de Petri dans lesquels les relations de flots et les contenus des places prennent leurs valeurs dans un monoïde résidué. Les opérations de base de ces algèbres, le produit et le résidu, qui expriment respectivement dans ce contexte la production et la consommation de ressources, permettent d'énoncer la règle de franchissement des réseaux sous sa forme habituelle. Les réseaux de Petri usuels correspondent au monoïde des entiers naturels. Le cas où le produit est non commutatif, non considéré ici, permettrait de décrire des réseaux dont les places ont par exemple des structures de file. Une algèbre de Petri est un monoïde résidué pour lequel la règle de franchissement a les propriétés attendues : associativité, réversibilité, monotonie ... Nous montrons que la classe des algèbres de Petri commutatives coïncide avec la sous-variété des treillis résidués engendrée par le monoïde des entiers naturels. Nous exhibons une algèbre dans cette variété dont la classe associée de réseaux est néanmoins strictement plus expressive que celle des réseaux de Petri.
We show how to formalise a constraint-based data flow analysis in the specification language of the Coq proof assistant. This involves defining a dependent type of lattices together with a library of lattice functors for modular construction of complex abstract domains. Constraints are expressed in an intermediate representation that allows for both efficient constraint resolution and correctness proof of the analysis with respect to an operational semantics. The proof of existence of a correct, minimal solution to the constraints is constructive which means that the extraction mechanism of Coq provides a provably correct data flow analyser in Ocaml. The library of lattices together with the intermediate representation of constraints are defined in an analysis-independent fashion that provides a basis for a generic framework for proving and extracting static analysers in Coq.
In the literature there are several CCS-like process calculi, or CCS variants, differing in the constructs for the specification of infinite behavior and in the scoping rules w.r.t. channel names. In this paper we study various representatives of these calculi based upon both their relative expressiveness and the decidability of divergence (i.e., the existence of a divergent computation). We regard any two calculi as being equally expressive iff for every process in each calculus, there exists a weakly bisimilar process in the other.
By providing weak bisimilarity preserving mappings among the various variants, we show that in the context of relabeling-free and finite summation calculi: (1) CCS with parameterless (or constant) definitions is equally expressive to the variant with parametric definitions. (2) The CCS variant with replication is equally expressive to that with recursive expressions and static scope. We also state that the divergence problem is undecidable for the calculi in (1) but decidable for those in (2). We obtain this from previous (un)decidability results by showing the relevant mappings to be computable and to preserve divergence and its negation. From (1) and the well-known fact that parametric definitions can replace injective relabelings, we show that injective relabelings are redundant (i.e., derived) in CCS (which has constant definitions only).
Les systèmes réactifs sont constitués de programmes interagissant en permanence avec leur environnements. Les débogueurs permettent généralement d'inspecter les variables et l'état du programme, après qu'on ait simulé l'environnement en lui fournissant une séquence d'entrées. Comme les programmes réactifs et leur environnement sont interdépendants (un véhicule est supposé ralentir lorsque ses freins sont activés...), simuler l'environnment peut être compliqué. Aussi, une fonctionalité très intéressante serait de procéder de manière inverse: étant donné un programme en cours de simulation et une propriété de sûreté P, demander au débogueur de fournir une séquence d'entrée qui mène le programme de son état courant à un état satisfaisant la propriété P, du moins si celle-ci existe. Ce problème est équivalent à la vérification de propriétés de sûreté et est donc notoirement indécidable en présence de variables numériques. Cependant, des procédures de semi-décision sont envisageables, qui permettent d'obtenir un résultat dans un nombre (si possible élevé) de cas.
Nous présentons donc la connexion de 3 outils, de débogage, de vérification et de test, pour résoudre ce problème. La contribution technique est la résolution efficace de ce problème pour des systèmes à variable numériques.