| Laboratoire |
LIFC
: Laboratoire d'Informatique de l'Université de Franche-Comté |
| Nom
de l'équipe ou du projet |
Equipe
Technique Formelles et à Contraintes |
| Responsable |
Françoise
Bellegarde (responsable par intérim : Bruno Legeard) |
| Effectifs
(chercheurs, enseignants-chercheurs, thésards, ingénieurs, techniciens) |
13
enseignants-chercheurs, 13 doctorants, 2 ingénieurs contractuels.Parmi
les 13 doctorants, 2 sont chez France-Télécom R&D, 1 chez PSA sur
contrat, 1 est financé sur le projet ANVAR, 1 est en mobilité internationale
à l'OGI (Portland, USA) |
| Axes
de recherche (liste de mots-clefs) |
3 axes:
- Raffinement,
vérification algorithmique et compositionnelle
- V érification
symboliques de systèmes de nature infinie
- Résolution
de contraintes pour la vérification
|
| Relations
industrielles ( liste de partenaires industriels) |
4 contrats
en cours:
- PSA et
Schlumberger :- définition d'une méthode de formalisation et
de vérification des propriétés des systèmes embarqués (PSA)
- Modélisation
du système de transaction de la Java Card pour la génération
de jeux de tests (SchlumbergerSema/Smart Card)
- Génération
de jeux de tests pour la validation de ticket Métro/RER (SchlumbergerSema/e-City)
- Génération
de jeux de test pour la fonction visibilité (PSA)
|
| Participation
à des programmes nationaux (ex. RNTL, RNRT) (liste de projets) |
- 3 projets
RNTL : Gemplus et ClearSy (projet BOM), THALES et Axlog (INKA
et DANOCOPS)
- INKA :
Génération automatique déterministe de donnée de test selon
des critères de couverture structurelle
- DANOCOPS
: Détection Automatique de NOn COnformité en un Programme et
sa Spécification
- BOM : Traduction
du langage B optimisant la consommation mémoire
- 1 projet
d'aide à l'innovation ANVAR sur BZ-testing tools- Outils pour
le tests de logiciels fondés sur les méthodes de spécification
formelle B et Z.
|
| Participation
à des programmes européens (ex. IST) (liste de projets) |
|
| Plates-formes |
|
| Suggestions |
|