We consider testing based on input/output transition systems, also known as input/output automata. We show that tests derived in an existing (synchronous) testing framework may not be sound if the tester cannot block outputs and we propose an asynchronous framework based on the idea of decomposing the tester into two test processes, one applying inputs via a finite queue to an IUT and the other reading outputs from a finite queue until it detects the quiescence of the IUT. The proposed test derivation procedures are based on a fault model.

In the early eighties, several extensions of CTL have been proposed (mostly by Emerson and Halpern) with the aim of repairing some deficiencies in the expressive power of CTL, but without going all the way to CTL* where model checking is PSPACE-complete. For these logics lying between CTL and CTL*, the precise complexity of the model checking problem has only been recently characterized. We present these recent results. The model checking problems for these branching-time logics share a similar structure, and their solution involve bounded invocations of NP oracles, with different logics requiring different bounds. The main difficulty with this work is that it requires investigating complexity classes that are very rarely encountered in computer science.

Homepage http://www.lsv.ens-cachan.fr/~phs
Papiers présentés FOSSACS 2001, ICALP 2003

Lors de l'analyse d'une phrase on souhaite synthétiser une représentation de la structure logique de la phrase, qui grosso modo dit "qui fait quoi" - par exemple en vue de sa traduction, qui concentre toutes les difficultés du traitement automatique des langues. On tâchera d'étendre la correspondance limpide entre structure syntaxique et structure sémantique qui existe dans les grammaires catégorielles à des grammaires qui modélisent des fragments plus conséquents de la langue. Les grammaires utilisées seront les grammaires minimalistes qui, techniquement, sont des grammaires d'arbres avec déplacements de sous-arbres et qui formalisent le récent programme minimaliste de Chomsky

http://www.labri.fr/Recherche/LLA/signes

Timed automata are a widely used and studied model. Since 8 years now, tools implementing this model are available and are successfully used on real-life examples. However, we recently proved that one of the technics used for checking reachability properties, namely the forward analysis, is algorithmically not correct: indeed, there exist timed automata for which the implemented forward analysis does not give the right answer to the question "is a given state reachable in this system?". We will present this result and explain what are precisely the problems.

http://www.lsv.ens-cachan.fr/~bouyer/bug.php

Les grammaires catégorielles sont surtout connues dans le domaine du traitement automatique de la langue. Des résultats d'apprenabilité (au sens de Gold) ont été démontrés récemment pour des classes particulières de telles grammaires. Dans cet exposé, nous présenterons certains de ces résultats, notamment ceux qui utilisent comme données d'entrée de l'algorithme d'apprentissage des suites de mots associés à des informations sémantiques lexicalisées.

http://www.grappa.univ-lille3.fr/~tellier

New application domains, such as e-commerce, require flexible approaches to meeting the to develop high quality software cheaply and rapidly. This talk will give an overview of innovative and still ongoing work on integrating two development approaches. UML-based approaches emphasize the modeling of software in a variety of views. Agile development methods de-emphasize software modeling, while emphasizing disciplined coding and testing.

The integrated approach is based on the use of an adapted version of the UML as a modeling, coding and test notation. The talk will examine how the UML can be applied to support rapid development. In particular the evolution of the UML models according to changing requirements or technology through systematic adaptation ("refactoring") steps will be discussed, its underlying theory explored, and demonstrated using a running example. For quality management automated tests are derived from UML-models and used for regression testing after each refactoring. At last, the talk will address the relationship between refactoring of models and code generation, automated tests and common ownership of models.

Who is Prof. Dr. Bernhard Rumpe?

We study languages of infinite two-dimensional words ($\omega$-pictures) in the automata theoretic setting of tiling systems. A hierarchy of acceptance conditions as known from the theory of $\omega$-languages can be established over pictures. Since the usual pumping arguments fail, new proof techniques are necessary.
We also show that (unlike the case of $\omega$-languages) none of the considered acceptance conditions leads to a class of infinitary picture languages which is closed under complementation.

We present a general model for the construction of real-time systems from components. The latter are modeled as transition systems with priority functions. A commutative and associative composition operator enables an incremental construction of the system. Two kinds of integration constraints are described by the interaction model, and the execution model. The interaction model describes the topology and types of interactions (blocking, non blocking) between the components. The execution model specifies constraints related to scheduling. We present compositionality and composability results for guaranteeing both safety and deadlock freedom properties of the composed system. (Joint work with Joseph Sifakis)

Data-flow programming languages use clocks as powerful control structures to manipulate data, and clocks are a form of temporal types. The clock of a flow defines the sequence of logical instants where the flow bears a value. This is the case of the synchronous data-flow programming language Lustre. We propose a solution for distributing automatically Lustre programs, such that the distribution is driven by the clocks of the source program. The motivation is to take into account long duration tasks inside Lustre programs: these are tasks whose execution time is long compared to the other computations in the application, and whose maximal execution rate is known and bounded. In a Lustre program, such a long duration task could be given a slow clock, but this violates the synchrony hypothesis. Distributing Lustre programs can solve this problem: the user gives a partition of the set of clocks into as as many subsets as he desires computing locations, and our distribution algorithm produces one program for each such computing location. Each program only computes the flows whose clock belongs to it, therefore giving time to each long duration task to complete.
http://www.inrialpes.fr/pop-art/people/girault
ftp://ftp.inrialpes.fr/pub/bip/pub/girault/Presentations/clock.pdf.gz

Dans le cadre de la synthèse de contrôleur à la Ramadge et Wonham, nous proposons une logique quantifiée pour la spécification formelle et la synthèse d'une large classe de contrôleurs. Nous étendons les résultats obtenus précédemment (http://www.inria.fr/rrrt/rr-4793.html) au cas de l'observation partielle.
Nous verrons la limite de décidabilité des problèmes en exhibant un critère syntaxique nécessaire et suffisant pour décider les solutions. En particulier, la synthèse d'un contrôleur maximal permissif parmi les contrôleurs sous observation partielle est décidable.
http://www.inria.fr/rrrt/rr-4793.html

Nous avons développés TOM : un compilateur permettant de programmer par filtrage dans les langages C, Java et Eiffel. Le premier objectif était de concevoir une brique de base permettant de simplifier la compilation des langages à base de règles. Une utilisation naturelle consiste ainsi à utiliser TOM comme back-end du compilateur ELAN par exemple.
Afin de tester et d'utiliser rapidement le compilateur TOM, celui-ci a été bootstrappé dès le début de son développement. De ce fait, le langage a évolué et est devenu agréable à utiliser (par un humain). Ce qui était un résultat inattendu départ.
Au cours de cette présentation, j'expliquerai les principes et les constructions de base du langage TOM. J'essaierai ensuite de montrer comment cette extension des langages C, Java et Eiffel peut être utilisée pour décrire facilement des algorithmes de compilation, de transformations de programmes et plus généralement des processus de transformations d'arbres ou de termes. http://www.loria.fr/~moreau

voir titre

Nous nous intéressons à la vérification interprocédurale de programmes impératifs, avec prise en compte des valeurs des variables (locales et globales).

La difficulté principale que nous traitons est l'abstraction de la pile d'appel de tels programmes, qui contient des informations portant non seulement sur les points de contrôle (sites d'appel) mais aussi sur les valeurs des variables locales. La structure de l'espace d'état d'un programme est donc assez complexe.

Afin de pouvoir appliquer les techniques standards d'interprétation abstraite, nous proposons d'utiliser une sémantique non standard, plus abstraite mais qui garde cependant des informations substantielles sur la pile d'appel.

Nous présenterons cette sémantique abstraite ainsi que ses propriétés, et nous comparerons nos résultats aux travaux existants.

We consider reachability problems over transition graphs of ground term rewriting systems. The vertices of these graphs are terms over a finite ranked alphabet and the edges are generated by a finite set of ground term rewriting rules. The simple reachability problem on these graphs can be stated as: given a term t and a regular set T of terms, does there exist a path from t to a term in T? This problem is known to be decidable for a long time. In this talk we analyze two different reachability problems. We show that the universal reachability problem, where the question is whether all paths from t lead to T, is undecidable. The recurrence problem, i.e., the question whether there is a path from t that visits T infinitely often, is shown to be decidable in polynomial time.

In the literature, we find several formulations of the control problem for timed and hybrid systems. We argue that formulations where a controller can cause an action at any oint in dense (rational or real) time are problematic, by presenting an example where the controller must act faster and faster, yet causes no Zeno effects (say, the control actions are at times 0,(1)/(2),1,1(1)/(4),2,2(1)/(8),3,3(1)/(16),...). Such a controller is, of course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well-understood if the time unit, or ``sampling rate'' of the controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We prove that this problem is undecidable even in the special case of timed automata.

http://www.irccyn.ec-nantes.fr

Nous nous intéressons ici au contrôle de systèmes à événements discrets modélisés par des HFSMs (Hierarchical Finite State Machines). Il est bien connu que l'efficacité des algorithmes de synthèse de contrôleurs dépend fortement du nombre d'états du système à contrôler. Les systèmes de grande taille étant la plupart du temps obtenus à partir de sous-systèmes (composés et hiérarchisés), on s'intéresse ici aux méthodes pouvant directement être appliquées sur les HFSMs). L'enjeu consiste ici à utiliser l'information donnée par la structure du modèle pour synthétiser un contrôleur, et ceci sans avoir à construire l'automate étendu correspondant (ce qui provoquerait une explosion de l'espace d'états). On s'attachera dans cet exposé à résoudre des problèmes d'invariance et de commande optimale sur ce nouveau modèle.

A distributed real-time control system has a time-triggered nature, just because the physical system for control is bound to physics. Loosely Time-Triggered Architectures (LTTA) are a weaker form of the strictly synchronous Time-Triggered Architecture proposed by Kopetz, in which the different periodic clocks are not synchronized, and thus may suffer from relative offset or jitter.
We propose a protocol that ensures a coherent system of logical clocks on the top of LTTA, and we provide several proofs for it, both manual and automatic, based on synchronous languages and associated model checkers. We briefly discuss how this can be used for correct deployment of synchronous designs on an LTTA.

http://www.irisa.fr/sigma2/benveniste/pub/emsoft_2002_ltta.html

We present a simple protocol for private authentication and its analysis in the applied pi calculus. We treat authenticity and secrecy properties of the protocol. Although such properties are fairly standard, their formulation makes an original use of process equivalence. In addition, we treat identity-protection properties, which are a delicate concern in several recent protocol designs.

(joint work with Martin Abadi)

Deux activités principales d'une preuve formelle sont la déduction et le calcul. La déduction nécessite souvent des interventions d'utilisateur tandis que le calcul peut être automatisé. Pour les assistants de preuve tels que Coq, le calcul doit être effectué de manière sûre et efficace. Nous proposons dans ce travail, une approche pour intégrer le calcul par réécriture en Coq en le combinant avec un système externe (ELAN). Nous avons obtenu des bons résultats de performance tout en assurant la sûreté du calcul. Par ailleurs, notre approche permet aussi de considérer la réécriture modulo AC ou bien conditionnelle. La première application de ce travail consiste à automatiser le raisonnement équationnel en Coq. En outre, la recherche de preuve non-déterministes effectuée par ELAN peut également être transférée à Coq de manière sûre. D'autres techniques de preuve par réécriture telles que la preuve par récurrence sont en train d'être étudiées. Aucune connaissance de Coq et ELAN n'est pré-requise et une démo est prévue si le temps le permet.

http://www.loria.fr/~nguyenqh/

We show the various definitions of Petri nets morphisms and study the problem of the completeness of resulting categories. The construction of equalizers happens to be not obvious. Proofs requires some work on monoid theory.

http://www.ipipan.gda.pl/~andrzej/

In Petri nets all events/transitions are potentially concurrent, with concurrency depending on the resources available in the current marking. Moreover, firing of an event is asynchronous with respect to the firing of another concurrent event. Thus, it seems, there is no place to discuss synchronous executions within the framework of Petri nets and similar models.

We plan to show that, contrary to the above intuition, important operations underlying the modular approaches to system construction rely on tight synchronisation of actions. This synchronisation results, one can argue, from a restriction of their natural ability to act asynchronously.

The exposition is intended to be rather informal. Nevertheless, a unifying categorical explanation of the various, seemingly different constructions will nevertheless be revealed.

http://www.ipipan.gda.pl/~marek/

L'approche synchrone est dédiée à la conception des systèmes réactifs. Grâce à leur sémantique forte, des langages synchrones comme Esterel, Lustre et Signal permettent de spécifier le comportement des systèmes de manière abstraite et rendent possible leur validation formelle, cruciale dans le cas des systèmes critiques.

La validation formelle des systèmes est un domaine de recherche en pleine expansion, spécialement en ce qui concerne les systèmes à espace d'état infini et les aspects numériques. L'application de ces méthodes aux programmes synchrones est fondamentale, mais plus ou moins directe. En particulier, dans le cas de Signal l'absence des variables est explicitée par une valeur spéciale, ce qui empèche l'interfaçage direct des outils aux techniques existantes.

Cette thèse traite de la manipulation de l'absence des variables synchrones, plus particulièrement dans les langages flot de données. Après un état de l'art du traitement de l'absence dans les sémantiques et les analyses synchrones, on présente un langage d'horloges appelé CL, basé sur une extension par des aspects numériques des horloges booléennes utilisées dans le contexte de la compilation Signal. On montre que CL permet d'interfacer naturellement les modèles étendus avec l'absence explicite à des théories standard, de plusieurs manières.

Nous étudions la logique NLTL, une logique du temps linéaire avec passe "oubliable". Nous montrons que NLTL peut être exponentiellement plus succincte que le logique LTL+Passé, qui elle même peut être exponentiellement plus succincte que LTL. Nous donnons ensuite un algorithme a base d'automates pour la vérification de cette logique. Cet algorithme s'exécute en EXPSPACE, et nous montrons qu'il est optimal.

http://www.lsv.ens-cachan.fr/~markey/download/Papers/2002/nltl.ps.gz http://www.lsv.ens-cachan.fr/~markey/download/Talks/slides/2002/LIAFA.pdf

Un protocole cryptographique est un protocole d'échange de messages entre plusieurs participants. Ces protocoles ont pour but, par exemple, de distribuer une clef secrète entre chacun des participants et/ou d'authentifier les participants. Ces protocoles sont en général décrits de manière simple et succincte. Pourtant ils sont souvent faux et certaines attaques ne sont parfois trouvées qu'une quinzaine d'années plus tard. D'où l'intérêt de prouver formellement leur correction. Pour cela, il existe deux principaux angles d'attaque : le développement d'outils de preuves pour des classes générales (et indécidables) de protocoles cryptographiques et la recherche de classes décidables plus restreintes. Nous montrerons un résultat de réduction qui peut être utile dans les deux cas : deux participants suffisent pour trouver une attaque. Nous présenterons ensuite quelques résultats de décision relatifs aux protocoles cryptographiques.

http://www.lsv.ens-cachan.fr/~cortier/
TRANSPARENTS (FICHIER PDF)

Les automates temporisés (AT) constituent un modèle adéquat pour décrire des systèmes à événements discrets (SED) temps-réel. D'un autre côté, les automates à états finis (AEF) sont un modèle adéquat pour étudier des SEDs. Une des approches qui a alors été utilisée pour étudier un SED temps-réel est de : 1) transformer les ATs décrivant le SED en des AEFs, et 2) faire l'étude du SED à partir des AEFs obtenus.

Nous adopterons l'approche ci-dessus en proposant une nouvelle méthode de transformation d'AT en AEF. Par rapport aux méthodes de transformations précédentes, celle que nous proposons est particulièrement adaptée pour le test et le contrôle des SEDs temps-réel. Après une description de la méthode de transformation, nous illustrerons son application pour le test et pour le contrôle de SEDs temps-réel.

http://www.gel.usherb.ca/khoumsi/

Nous proposons un modèle de calcul qui intègre la programmation concurrente et déclarative. Nous suggérons de modéliser un système par un ensemble de composants. Chacun de ces composants comporte un programme déclaratif, appelé store, et un ensemble de processus interagissant par l'exécution d'actions. L'interaction entre composants est fondée sur le même principe, c.-à.-d. un processus peut exécuter des actions sur les stores des autres composants. Nous présentons également une analyse de la confidentialité pour les processus d'un composant.

Exposé de thèse ftp://ftp.imag.fr/pub/bibliotheque/theses/2002/Serwe.Wendelin/notice-francais.html

La ré-ingénièrie des applications est devenue une activité vitale pour l'industrie dans un contexte où les changements d'emplois appauvrissent les applications en détruisant la connaissance orale détenue par les développeurs et où les applications doivent constamment évoluer afin de satisfaire de nouveaux besoins. Cette présentation résume un effort de recherche sur la rétro-conception et la ré-ingénièrie des applications orientée objets.
Il présente la problématique, puis décrit (1) la définition d'un méta-modèle adapté à la ré-ingénièrie, FAMIX. Ce méta-modèle permet non seulement des opérations de rétro-conception mais aussi l'expression de transformation de code (refactorings), (2) la présentation d'une plate-forme de ré-ingénièrie, Moose, qui sert de base à un grand nombre de nos travaux, (3) l'évaluation de métriques logicielles pour la ré-ingénièrie, (4) la définition de techniques visuelles pour la compréhension de très grandes applications et de classes, (5) l'identification de code dupliqué de manière indépendante des langages et des solutions pour le traiter, (6) le mélange d'information dynamiques et statiques pour la génération de vues composables et d'information de collaboration et (7) l'identification de patterns de ré-ingénièrie.

http://www.iam.unibe.ch/~ducasse/

Pour générer du code séquentiel à partir d'Esterel, il existe aujourd'hui trois grandes classes de techniques: celles à base d'automates explicites, les techniques à base de circuits logiques, et finalement celles basées sur une simulation plus directe de la sémantique opérationnelle. Les deux premières, implémentées dans les compilateurs CMA/INRIA, peuvent en théorie traiter tout programme correct, mais ont des problèmes de performance. Les techniques du troisième type génèrent du code performant en planifiant statiquement les opérations réactives du programme initial et rejettent donc les programmes "cycliques".
Nous proposons une méthode de compilation basée sur un modèle intermédiaire qui tente de de réconcilier l'approche formelle des deux premières classes de méthodes avec la performance des techniques de simulation.