1998-1999

Groupe de travail

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

Le jeudi de 10h30 à 12h
Salle G.T. 2, LaBRI, Rez-de-chaussée


Programme du jeudi 10 juin 1999


Prévisions

Le groupe de travail

La petite école pour la vérification


Réunions précédentes

10 juin (11 heures). Christophe Mauras (IRCyN Nantes)
Simulation symbolique de programmes relationnels synchrones.
Nos travaux, dans le cadre de la programmation synchrone, concernent la "simulation symbolique" de programmes synchrones, eventuellement non deterministes. On definira tout d'abord ce qu'on entend par simulation symbolique, a savoir le calcul pas a pas, ou jusqu'a point fixe des relations caracterisant le comportement d'un programme pour un ensemble donné d'entrees. On prend en compte a la fois les variables booleennes et les variables numeriques liees par des contraintes lineaires.
On presentera YoYo, notre outil de simulation symbolique realise pour DC (le format declaratif commun aux langages synchrones Lustre Esterel et Signal). On presentera les diagrammes de decision a contraintes, une structure de donnees derivée des Bdd, adaptee a la manipulation de contraintes.
On situera nos travaux par rapport a ceux sur la verification de programmes synchrones (en particulier ceux de Halbwachs), l'interpretation abstraite, et la programmation logique avec contraintes (Chip, Toupie...) pour laquelle nous avons propose une traduction vers CLP(R) permettant d'effectuer une analyse statique.
Nous concluerons sur la "fertilisation croisée" (que Rauzy évoquait deja en 1993) entre la verification et la programmation par contraintes en tentant de montrer les rapprochements possibles entre nos travaux et ceux sur AltaRica.
3 juin. Jean-Michel Couvreur (LaBRI)
Vérification automatique de formules LTL sur des systèmes finis. (première partie)
20 mai. Davy Rouillard (LaBRI)
Le projet ROBUSTA.
7 mai. Jørn Lind-Nielsen (DTU, Danemark)
la vérification de grands systèmes State/Event.
15 avril. Gérard Cécé (Post Doc à Liège)
Les réseaux en anneau sont plus facile à analyser.
1 avril. André Arnold (LaBRI)
Logiques temporelles, mu-calcul et jeux (deuxième partie).
11 mars. Anne Bergeron (UQAM Montréal)
Synthèse de contrôleurs avec contraintes temporelles.
Un processus est souvent spécifié sous forme d'un automate dont les transitions représentent des événements externes et des actions qui peuvent être déclenchées. Etant donné n contraintes temporelles paramétrées par (d1, ... , dn) sur un tel processus, nous dérivons des conditions sur les paramètres de sorte que le processus soit implantable.
En exemple, nous présenterons une spécification d'un service téléphonique de Nortel, le Call-Monitor-and-Intercept Feature, où quelques erreurs ont été détectées et corrigées avec cette approche.
25 février. Paul-Yves Gloess (LaBRI)
PVS : Quelques rappels logiques et un exemple d'utilisation autour de la logique LTL.
18 février. Jean-Pierre Jouannaud (LRI)
A propos du projet (CNET, qui vient en accompagnement du projet RNRT) de future version Coq integrant des procedures de decision.
11 février 1999. Serge Chaumette (LaBRI)
Présentation de CORBA.
4 février 1999. André Arnold (LaBRI)
Logiques temporelles, mu-calcul et jeux (première partie).
14 janvier 1999. Patrice Laurençot (LaBRI)
Integration du temps dans les tests de protocoles de communication (Répétition soutenance de thèse).
7 janvier 1999, Réunion de rentrée (de l'année civile)
L'organisation de l'équipe dans la nouvelle structuration du LaBRI.
10 décembre 1998, Davy Rouillard (LaBRI)
Premières preuves sur des automates paramétrés.
3 décembre. Patrick Félix (LaBRI)
Bilan de l'action FORMA.
26 novembre. Poul Frederick Williams (Technical University of Danemark)
Boolean Expression Diagrams.
19 novembre. Antoine Rauzy (LaBRI)
PVS + SMV + Aralia : un exemple d'analyse de circuits.
22 octobre 1998. Alain Griffault, André Arnold & Antoine Rauzy (LaBRI)
Un exemple de description en AltaRica pour comprendre les différences entre priorités, synchronisation et flux de données.
8 octobre 1998. Alain Griffault & Gérald Point (LaBRI)
AltaRica : projet, langage, problèmes...
1 octobre 1998. Réunion de rentrée.
Constitution du programme des séances suivantes.

Années précédentes


Navigation

  • Equipe Modélisation, Vérification et Test des systèmes informatisés