Outils et Logiciels pour la Communication
Projet
de
Recherche
de
Recherche
|
|
Outils et Logiciels pour la Communication |
de Recherche |
|
|
| rtl |
Simulation : interprétation des actions sémantiques de la
spécification RT-LOTOS; Vérification par analyse d'accessibilité : traduction de la spécification RT-LOTOS en automate temporisé DTA, puis construction d'un graphe de régions (graphe minimal d'accessibilité). |
|---|---|
| dtasim | Simulation : exécution de l'automate temporisé DTA. |
| dta2kronos | Vérification par model-checking : traduction de l'automate temporisé DTA en un automate temporisé exploitable par le model-checker Kronos. |
| Principe de la synthèse | Chaine d'outils pour la synthèse avec filtrage | Chaine d'outils pour la synthèse avec minimisation & filtrage |
|---|---|---|
 |
 |
 |
| dtacut | Filtrage : selection sur le graphe de régions des configurations jugées cohérentes selon les critères de l'utilisateur. |
|---|---|
| rg2tlsa | Synthèse : contruction de l'automate d'ordonnancement TLSA depuis le graphe de régions (cohérent). |
| bcg_min | Minimisation : minimisation du graphe de régions (outil CADP). |
