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)
- 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.
(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.
- 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 :
- Djamel-Eddine Saidouni [saidounid@hotmail.com]
- Nabil Belala [belala@umc.edu.dz]
- Adel Benamira [benamira.adel@caramail.com]
- Abdenadir Delimi [delimi_nad@yahoo.fr]
- Mohamed Nassim Seghir [seghir@mpi-sb.mpg.de]