FOCOVE 1 - 2001

La première version de FOCOVE a vu le jour en juin 2001, où deux outils ont été développés :

1. Equipe LOTOS: (Bourekab Med Tahar, Boulkera Samir et Berdoudi Cherif)
  • Compilateur LOTOS ILC (Interleaving LOTOS Compiler)
  • Vérification par Bissimulation Forte
  • Representation Graphique (LTSVIEW)
2. Equipe CCS: (Benamira Adel et Bouziane Toufik)
  • Compilateur CCS ICC (Interleaving CCS Compiler)
  • Vérification par Bissimulation Forte et Faible

FOCOVE 2 - 2002-2006

La version 2 de FOCOVE comprend plusieurs outils:

1. LotoStem: (Nabil Belala, Adel Benamira, Abdenadir Delimi et Mohamed Nassim Seghir)
Outil de vérification formelle basé sur la sémantique de maximalité. Il contient un compilateur pour Basic LOTOS qui permet de générer un système de transitions étiquetées basé sur la maximalité (STEM), un model-checker qui permet de vérifier des propriétés exprimées en CTL sur le STEM généré, et un module de visualisation graphique du STEM.

2. FOCOVE 2.0: (Abdelghani Alidra, Nabil Belala, Adel Benamira, Abdenadir Delimi, Afifa Ghenaï et Seghir Mohamed Nassim)
Environnement intégrant LotoStem 1.2 et des modules de génération de STEMs alpha-réduits et de graphes de pas maximaux. L'intégration des graphes de refus mixtes est prévue dans la prochaine version.

3. MSMC: (Labbani Ouassila)
(Maximality based Symbolic Model Checking), c'est un outil qui permet la vérification symbolique des propriétés sur les systèmes parallèles, il prend comme arguments une spécification de système à vérifier modélisé par un système de transitions étiquetées maximal (STEM), et une spécification des propriétés à vérifiées exprimées en logique temporelle arborescente (CTL). L’implémentation de cet outil est basée sur l’utilisation des diagrammes de décision binaire (BDDs) qui permettent d’éviter la construction explicite du graphe d’états.

4. DBRE: (Belguidoum Meriem)
(Decidable Bisimulation Relational Equivalence), Cet outil permet :
- la génération d'un système de transitions étiquetées à partir d'une spécification LOTOS.
- la sauvegarde des systèmes de transitions étiquetées sous forme d'un fichier externe.
- la comparaison entre les systèmes de transitions étiquetées (STE) modulo la relation de bisimulation forte.
- l'étude de l'équivalence comportementale des spécifications écrites en LOTOS avec le respect de la relation de bisimulation forte en utilisant deux méthodes de comparaison: la méthode classique et la méthode à la volée.
- la comparaison entre ces deux méthodes de vérification.

5. TEST: (Deraredj Linda et Ghenai Afifa)
Outil de mise en oeuvre de l'approche test, apportant une certitude mathématique par génération de tests de conformité sous forme d'une structure appelée: graphe de refus, et par extension et adaptation du calcul de bisimulation pour la vérification des relations de conformité d'une implémentation par rapport à sa spécification.



Contactez quelques participants au projet :