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