2000 - 2001

Groupe de travail

Modélisation, Vérification et Tests des systèmes informatisés
&
Petite école pour la vérification


Programme de l'année 2000-2001

le 5 Octobre Réunion de rentrée

Prévisions

Mois de Novembre

le 2 Novembre.Relâche
Titre: Vacances
le 9 Novembre. Intervenant: François Dufour (LaBRI)
Titre: Un Point de vue en Automatique
le 16 Novembre. Relâche
le 23 Novembre. Intervenant: Philippe Thomas (LaBRI)
Titre: Hévéa : Gestionnaire d'arbre de défaillances couplé à Aralia.
Résumé: De l'utilité de la réécriture et des meta heuristiques pour le traitement par les BDDs de formules booléennes "dites" industrielles
le 30 Novembre: Petite école: Intervenant: André Arnold (LaBRI)
Titre: Synthèse de Contrôleur (2 ère partie)

Mois de Décembre

le 14 Decembre Intervenant: Anne Dicky (LaBRI)
Titre: Automates Quantiques.
le 21 Decembre. David Sherman (LaBRI)
Titre: Réseaux d'Interaction dans la Bioinformatique

Mois de Janvier

le 11 Janvier. Intervenant: Patrick Félix (LaBRI)
Titre: Autour de CALIFE
le 18 Janvier. Intervenant: Rodolphe Pueyo
Titre:Formalisation en PVS d'une sémantique pour un sous-ensemble du langage de spécification de types de données ASN.1.
le 25 Janvier. Intervenant: Patricia Bouyer
Titre:Automates temporisés avec assignations

Mois de Février

le 1 février. Relâche
le 8 février.Relâche
le 15 février. Intervenant: Jean-Michel Couvreur
Titre: DDD

Mois de Mars

le 8 mars. Intervenant:Remi MORIN (Institut fuer Algebra Technische Universitaet Dresden)
Titre : Sur la verification de specifications en HMSC: quelques resultats recents.
Résumé:
          Hierarchical Message Sequence Charts are a well-established formalism to
specify telecommunication protocols. 
  In this model, numerous undecidability results were obtained recently through
algebraic approaches or relationships to 
  Mazurkiewicz trace theory. We show how to check whether a rational language
of MSCs requires only channels of 
  finite capacity. In that case, we also provide an upper bound for the size of the
channels. This enables us to prove 
  our second result: one can decide whether the iteration of a given regular
language of MSCs is regular if, and only if, 
  the Star Problem in trace monoids (over some restricted independence
alphabets) is decidable too. This well-known 
  question remains open and justifies the recent restriction to locally synchronized
HMSCs since they describe (all 
  finitely generated) regular languages. We also show here how this useful
representation can actually be infered from 
  Ochmanski's Theorem. 
    
le 15 Mars. Intervenant: Yves Dutuit
Titre:
le 8 Mars. Petite école: Intervenant: Kaninda Musumbu (LaBRI)
Titre: Interprétation Abstraite et Vérification de Système temporisé.

Mois d'Octobre

le 12 Octobre. Intervenant:
Titre: RELACHE
le 19 Octobre. Intervenant:Aymeric Vincent (LaBRI)
Titre:
le 26 Octobre Petite école: Intervenant: André Arnold (LaBRI)
Titre: Synthèse de Contrôleur (1 ère partie)