EXPOSES
1999-2000
Retour à la page du séminaire
Jeudi 31 août 2000 à 14h en salle Les Minquiers
Runge-Kutta methods and practical computation
Exposé introductif
John BUTCHER (University of Auckland,
invité par Aladin)
This year marks the centenary of the paper by Heun which came between those of Runge in 1895 and Kutta in 1901. To celebrate the anniversary of Heun's paper, a survey of Runge-Kutta methods in the twentieth century will be given from the points of view of interesting mathematics and efficient algorithms. The seminar will be non-technical and will use only elementary algebra and calculus with ideas from graph theory, combinatorics and group theory introduced only where they are needed.
Les spécifications formelles des logiciels sont souvent représentées sous la forme de systèmes de transitions étendus avec des données symboliques (variables, paramètres). De telles spécifications sont couramment utilisées pour écrire des cas de tests, qui sont également des systèmes de transitions étendus. La génération de tests est un problème de synthèse de programme : à partir de la spécification d'un objectif de test qui décrit certains comportements à tester, dériver un programme qui observe les sorties de l'implémentation du système pour détecter des comportements incorrects, tout en essayant de contrôler l'implémentation afin de satisfaire l'objectif de test. Ecrire ces cas de test à la main est une tàche compliquée et peut mener à des erreurs. Dans cet expose je présenterai l'ébauche d'une méthode pour y parvenir de manière semi-automatique.
Nous sommes demandeurs de techniques symboliques de résolution de contraintes. Les collègues travaillant sur ce thème sont tout particulièrement invités...
Dans cette présentation je vais montrer comment nous avons utilisé l'approche de type diagnostiqueur (présentée par S. Lafortune la semaine dernière) pour effectuer de la supervision de systèmes dynamiques et plus exactement pour de réseaux de télécommunications. L'exposé, après une présentation de la notion de diagnostiqueur et de ces extensions, se focalisera sur les méthodes étudiées pour résoudre le problème lié à la taille du système : le diagnostiqueur générique et le diagnostiqueur décentralisé.
Mardi 20 Juin 2000 à 16h15 en salle Les Minquiers
Circuits, automates, preuves et objets mathématiques présentent des symétries similaires. On a developpé un langage basé sur les graphes pour en parler et les relier à certaines questions de complexité.
Mardi 13 juin à 16h15 en salle Les Minquiers
Sur les graphes rationels
Exposé Avancé
Christophe MORVAN (IRISA)
Dans cet exposé, nous allons définir une famille de graphes infinis : les graphes rationnels. Nous allons donner un certain nombre de leurs propriétés, et donner des indications de preuves. Nous nous intéresserons aussi à leurs traces.
Mardi 6 juin à 16h15 en salle Les Minquiers
Inférence grammaticale
Exposé Général
François COSTE (Aïda)
L'inférence grammaticale consiste en l'apprentissage automatique de modèles de langages (grammaires, automates) à partir d'exemples et, éventuellement, de contre-exemples, d'un langage inconnu. Ce type d'apprentissage permet d'envisager l'apprentissage de concepts intégrant la notion de séquentialité.
Parmi les applications concernées par cet apprentissage, on peut par exemple citer des tâches aussi différentes que : la constitution automatique de la grammaire formelle d'une langue, l'analyse d'une séquence d'ADN, la planification d'un enchaînement d'actions, la conception d'un circuit logique séquentiel, la reconnaissance d'écriture manuscrite ou la détection d'intrusion dans un système informatique.
L'exposé tentera de donner un aperçu de l'état de l'art des techniques d'inférence grammaticale par la présentation des principaux résultats d'apprenabilité obtenus ainsi que la présentation d'exemples d'algorithmes d'apprentissage utilisés.
Mardi 30 mai à 16h15 en salle Les Minquiers
Résultats d'indécidabilité
sur les Messages Sequence Charts
Exposé Avancé
Gilles LESVENTES (Paragraphe)
Les Message Sequence Charts (MSC) sont une forme moderne des bons vieux diagrammes temporels, adaptés à la description de scénarios où les agents d'un système distribué communiquent par messages. Les High Level MSC (HMSC) sont des générateurs finis de MSC que l'on peut voir comme des automates étiquetés par des MSC.
Les HMSC sont présentés dans la littérature comme un outil de spécification. Cet exposé préliminaire, démontrant une série de résultats d'indécidabilité sur les HMSCs, décrit les limitations d'un tel point de vue. Un second exposé serait nécessaire pour présenter une vue optimiste des HMSCs en tant que spécifications partielles réalisées par des réseaux de Petri.
Dans ce premier exposé, on rappelle le modèle des HMSCs ainsi que des résultats classiques de théorie des langages sur les reconnaissables et rationnels dans un produit de monoïdes. L'exposé sera technique plus que philosophique et peut servir de petite introduction pour ceux qui ont toujours pensé que, quel que soit un monoïde M, Rat(M)=Rec(M).
Mardi 23 mai à 16h15 en salle Les Minquiers
HPTS : un certain nombre de paradigmes de
programmation en un modèle
Exposé Avancé
Stéphane DONIKIAN (SIAMES)
HPTS (Hierarchical Parallel Transition Systems) est un modèle formel qui a été conçu pour la programmation du comportement humain. Il intègre pour ce faire un certain nombre de paradigmes : flot de données, réactivité, non déterminisme, gestion du temps, concurrence, hiérarchie, préemption. Un langage de programmation lui est associé, ainsi qu'un générateur de code C++. L'objectif de cet exposé est de présenter l'ensemble des fonctionnalités du modèle, ainsi que son utilisation pour la spécification de comportements et de scénarios. Dans ce second cas une sémantique proche de la sémantique Superstep de Statecharts est utilisée
The following problem is considered: given a specification of a concurrent behaviour, represented as a transition system, find maximally concurrent safe Petri net which realizes this behaviour. In my talk I plan to provide motivations and suggest a solution in which labelled Petri nets are used. Ideally, the construction should work not only on specifications, but on morphisms between specifications as well.
Mardi 9 mai à 16h15 en salle Les Minquiers
Modélisation de Design Patterns en UML
Exposé Introductif
Gerson SUNYE (Pampa)
Les Design Patterns caractérisent des problèmes récurrents de conception et spécifient des solutions claires et élégantes à ces problèmes. Ils représentent des connaissances relatives à la conception d'applications.
Cependant, ces connaissances sont insuffisantes pour aboutir à leur mise en œuvre. En effet, il reste à effectuer un certain nombre de choix d'implémentation, fortement liés à la spécificité de l'environnement choisi pour réaliser la solution. De plus, suivant le contexte dans lequel la mise en œuvre du pattern doit être intégrée, un certain nombre de contraintes doivent être respectées. La combinaison de ces choix d'implémentation et de ces contraintes entraîne la possibilité d'un grand nombre d'implémentations différentes pour un même pattern. D'autre part, chacune de ces implémentations est trop spécifique pour être réutilisée dans des situations similaires, d'où la difficulté de leur automatisation.
Dans cet exposé, je ferai une introduction aux Design Patterns et je présenterai les bénéfices et difficultés de leur intégration à un outil de modélisation UML. Cette intégration concerne mes travaux de recherche au sein de l'équipe PAMPA.
Mardi 18 Avril à 16h15 en salle Les Minquiers
Modelisation des regions dans un pi-calcul
avec groupes
Exposé Avancé
Silvano DAL-ZILIO (Microsoft Cambridge,
invité par EP-ATR)
Dans cet exposé, nous portons un nouveau regard sur le calcul des régions de Tofte et Talpin en nous aidant d'un codage dans un pi-calcul typé avec groupes.
Dans un langage fonctionnel avec régions, les valeurs sont allouées dans des segments mémoires déterminées à la compilation. Ces segments sont contrôlés suivant une politique de pile qui améliore sensiblement la gestion de la mémoire. Ainsi, le calcul des régions a été utilisé avec succès comme langage intermédiaire dans l'implantation de MLKit, un compilateur sans ramasse-miettes pour Standard ML.
La notion de groupes a été introduite dans le calcul des ambients typé de Cardelli, Ghelli, et Gordon. Dans ce calcul, comme dans le pi-calcul que nous nous proposons d'utiliser, chaque nom appartient à un groupe statiquement déterminé. Utilisé dans un système de types avec effets, les groupes permettent la vérification de certaines propriétés liées à la mobilité.
Notre codage précise la correspondance intuitive entre régions et groupes. Nous proposons, entre autre, une nouvelle formulation de la propriété de conservation du typage pour le calcul des régions. Notre codage nous permet aussi de prouver la correction de la gestion des régions. Ce résultat est prouvé à l'aide d'une nouvelle loi d'équivalence comportementale pour notre pi-calcul.
articles sur les groupes dans le pi-calcul
@Article{TalpinJ94, title={The Type and Effect Discipline},author={Jean-Pierre Talpin and Pierre Jouvelot},pages={245--296},journal={Information and Computation}, month=jun,year=1994,volume=111,number=2}
Cet exposé présente une tentative d'étude de l'expressivité de
différentes familles dopérateurs de préemption. La contribution principale de ce travail est :
(1) une proposition de définitions précises pour la classe des opérateurs
"préemptifs" mais aussi pour les sous-classes des opérateurs "suspensifs"
(le ^Z d'Unix) et "abortifs" (le ^C d'Unix).
(2) la preuve que les suspensifs sont strictement plus expressifs que
les abortifs.
Le cadre mathématique utilisé pour établir la classification est celui
des spécifications SOS (pour "Structured Operational Semantics"). Dans
ce cadre, on pourra définir un critère d'équivalences sur les
opérateurs pour mesurer leur pouvoir d'expressivité.
Enfin, nous terminerons par une discussion "critique" de cette approche.
Je compte repasser en revue les résultats obtenus collectivement sur la désynchronisation, en vue du déploiement de spécifications synchrones sur des architectures distribuées asynchrones. Plusieurs d'entre vous les connaissent déjà (les ont même entendus plusieurs fois); j'irai plus ou moins vite selon l'assistance, sur ces rappels.
La suite sera plus informelle. Je compte indiquer comment on peut tirer avantage de ces résultats pour la conception objet à la UML (formalisme BDL), en offrant un certain type de création dynamique d'instances.
Dans une autre direction, je vous indiquerai également comment on peut imaginer déployer du code synchrone sur des bus de terrain pour l'automatique, de type OSEK.
De nombreuses théories logiques ont été utilisées pour prouver qu'un système informatique, matériel ou logiciel, satisfait des propriétés de sécurité données. Etrangement la théorie de la programmation linéaire n'a pas été utilisée dans ce but alors qu'elle possède de belles propriétés de complétude ainsi qu'une panoplie d'algorithmes de décision très efficaces.
Dans cet exposé, nous montrerons comment le fonctionnement d'un système informatique, matériel ou logiciel, peut être modélisé avec la programmation linéaire. Puis nous montrerons que grâce au théorème de la dualité, on obtient un moteur de preuve par inférences à la fois puissant et efficace.
Le problème de la synthèse de contrôleur sur des systèmes à événements discrets consiste, à partir d'une spécification du système et d'un ensemble de propriétés (objectif de contrôle) attendues de celui-ci, à dériver/synthétiser un contrôleur qui, une fois placé dans son environnement, va contraindre le comportement du système de manière à garantir l'ensemble des propriétés.
Dans cet exposé, nous ferons une présentation introductive des méthodes de synthèse de contrôleur telles qu'elles furent introduites par Ramadge et Wohnam (RW) dans les années 80. Dans cette approche, l'idée de base est de modéliser le système par un automate. Les changements d'états se font de manière asynchrone sous l'action d'événements. L'ensemble de toutes les séquences possibles d'événements pouvant se produire dans le système est défini comme le langage du système. Toutefois, il peut arriver que le système ne correspondent pas aux langage désiré (ie au comportement désiré). La théorie de RW peut alors être utilisée pour synthétiser un superviseur qui va inhiber certains événements du système (appelés événements contrôlables) de manière à ce que le langage du système rebouclé (système + superviseur) soit conforme au langage de spécification. Basé sur cette théorie, nous montrerons également comment l'introduction de fonctions de coût peut permettre de prendre en compte des objectifs de contrôle d'ordre qualitatif.
Les Message Sequence Charts sont un formalisme graphique qui permet de spécifier des scénarios. Ils sont bien adaptés pour capturer les exigences, mais leur traduction en un autre modèle plus opérationnel est difficile, et souvent impossible. Les limites des méthodes de synthèse à partir de MSCs sont encore mal connues. Dans cet exposé, nous ferons une rapide présentation des MSCs et de leur puissance d'expression, puis nous présenterons des conditions nécessaires pour que la synthèse d'automates communiquants preserve les comportements décrits par des MSCs.
Vous trouverez sur cette page une compilation d'articles en ligne concernant les Message Sequence Charts.
Et sur cette autre page un résumé du travail effectué sur les MSCs dans l'équipe PAMPA
This presentation discusses the tool "TorX", which was developed
based on the formal IOCO testing theory (see presentations about
formal testing of 28/01/99 and 31/01/99). Moreover, the application
of TorX to testing a simple "Conference Protocol" is discussed,
together with some comparable expreriments with other tools. The
automation of test derivation and test execution in the area of
conformance testing is discussed. A central theme of this study
is the usability of batch-oriented and on-the-fly testing approaches.
The test scenarios are derived from multiple specification languages
and using different tools:
LOTOS, Promela, SDL and FSM. To facilitate the derivation from different
formal description techniques and the different test execution approaches,
TorX has an open and generic architecture, which enables plugging
in existing or dedicated tools. We have carried out several experiments
in testing the Conference Protocol, resulting in requirements on
automated testing and benchmarking criteria.
Comme dans la plupart des travaux traitant de vérification
de protocoles cryptographiques il ne sera quasiment pas question
de cryptographie! En effet, la première hypothèse
de travail pour vérifier de tels protocoles est généralement
de considérer que les clés de cryptage sont "incassables".
Cependant, malgré cette hypothèse très forte
sur la cryptographie, il subsiste souvent des failles logiques remettant
en question la sûreté d'un protocole. A l'inverse,
lorsque plus aucune faille n'est découverte, il reste à
se convaincre que
le protocole est sûr dans tous les contextes d'utilisation.
Je passerai rapidement en revue quatre grandes classes d'outils
utilisés
pour la vérification des protocoles cryptographiques:
- les logiques BAN (logiques modales de croyance),
- le model-checking,
- la démonstration automatique
- l'interprétation abstraite.
Je tenterai de montrer leur spécificités
et leurs limites pour ce type de vérification.
This presentation deals with the
use of formal methods in testing of concurrent systems. A framework
for conformance testing based on formal specifications is presented:
what is conformance; what is testing; what is test execution; what
is test generation; and what are the requirements they should satisfy.
These testing concepts will be elaborated for labelled transition
systems, a mathematical model which underlies many formal specification
languages, especially in the area of concurrent systems. For one
particular notion of conformance on transition systems, viz. the
implementation relation IOCO,
a test generation algorithm will be presented which is shown to
be correct.
Nous nous intéresserons aux
relations entre synchronisme et asynchronisme. Des modèles
simples de ces deux paradigmes seront détaillés ainsi
qu'un ensemble de théorèmes permettant de garantir
la correction de la désynchronisation d'un programme synchrone
isolé
ou bien d'un réseau de programmes synchrones. Ces théorèmes
sont assortis d'hypothèses qui constituent des obligations
de preuves vérifiables sur la composition synchrone des programmes
considérés.
Si ces conditions ne sont pas vérifiées, il est possible
d'adjoindre à chacun des programmes synchrones, un nouveau
programme synchrone permettant d'assurer la correction de la désynchronisation.
Ceci peut être considéré comme étant
une méthode de génération
de protocoles de synchronisation en environnement asynchrone.
De nombreux formalismes utilisés dans le domaine du raisonnement temporel et du raisonnement spatial qualitatif partagent des caractéristiques communes ; suivant en cela l'exemple des travaux d'Allen sur les intervalles, ces approches se caractérisent en particulier par :
- l'utilisation d'un ensemble fini de relations binaires
symboliques entre entités temporelles ou spatiales ;
- des propriétés algébriques et géométriques
qui reflètent
la structure du temps ou de l'espace ;
- l'emploi de méthodes de propagation de contraintes.
Ces dernières années ont vu un progrès important de la connaissance des propriétés de complexité de ces formalismes. Nous exposerons quelques uns des résultats correspondants pour les principaux formalismes concernés : intervalles, intervalles généralisés, directions cardinales, rectangles, etc.
La page web du conférencier :
http://www.limsi.fr/Individu/ligozat/
Page web du module de DEA RaTS (raisonnement temporel et spatial)
http://www.irisa.fr/aida/Pages_Pros/quiniou/enseignement/rats.htm
L'inférence grammaticale consiste à construire une
représentation d'un langage dont on ne connaît qu'un
sous-ensemble de mots
ainsi éventuellement qu'un ensemble de mots n'appartenant
pas au langage. Nous évoquons dans cet exposé quelques
résultats du domaine, en développant particulièrement
le cas de l'apprentissage de langages réguliers. La seconde
partie de l'exposé illustre les capacités des techniques
de l'inférence grammaticale dans le domaine de la bio-informatique.
Les langages modélisent alors la reconnaissance de structures
ou de sites actifs à l'intérieur de macro-molécules
biologiques.
Une multitude de problèmes d'informatique peuvent s'interpréter comme des problèmes d'accessibilité dans des graphes dirigés. On montrera que ces problèmes d'accessibilité peuvent se ramener au calcul des composantes fortements connexes et on présentera l'algorithme de Tarjan permettant de résoudre le problème. On illustrera l'exposé par des exemples de tels problèmes et des adpatations/modifications de l'algorithme de base pour le model checking, la récupération mémoire, la génération de test, le calcul de stratégies d'intégration.
Tarjan 72, Depth-first search and linear graph algorithms,
SIAM J. Comput., vol 1, no 2, pp 146--160, June 72.
Je vais parler:
- soit du cube de Barendregt (introduction) et de
ce qu'on peut en tirer pour la programmation (prospection),
- soit des systèmes d'information logiques (prospection)
et des théories que nous utilisons dans ce cadre (introduction).
[Il a parlé du second point.]
J'expliquerai ce qu'est le model-checking
dans pour le
cas des automates finis et de la logique temporelle CTL.
Puis, j'introduirai les Binary Decision Diagrams (BDD) comme
représentation efficace du type ensemble et montrerai
leur utilisation en model-checking.
Un très bon livre récent, disponible à l'IRISA
qui
constitue ma base de cours de DEA (Filère 2 module A2R
"Analyse comportementale de systèmes réactifs et répartis").
Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie,
and A. Petit. Vérification de logiciels : Techniques et outils
du
model-checking. Vuibert, 1999.
TRANSPARENTS
(FICHIERS POSTSCRIPT .gz)
Présentation de la logique linéaire à partir
des grammaires formelles
et du calcul de Lambek. Codage standard des réseaux de Petri
en logique linéaire. Si j'ai le temps de préparer:
codage de l'exécution des réseaux de Petri dans la
logique linéaire mixte (commutative/ non commutative). Sinon,
ce sera pour une prochaine fois.
TRANSPARENTS
(FICHIER POSTSCRIPT .gz)