Outils et Logiciels pour la Communication
Projet
de
Recherche
de
Recherche
|
|
Outils et Logiciels pour la Communication |
de Recherche |
 Version Française |
 English Version |
|
|
Le projet RT-LOTOS (Real-Time LOTOS)
Responsable: Jean-Pierre COURTIAT (e-mail: courtiat@laas.fr)
Membres du projet (anciens et actuels) :
Le langage RT-LOTOS est un langage permettant de décrire formellement les systèmes contraints par le temps. Il s'agit d'un langage de type algèbre de processus. Il étend le langage Lotos par des opérateurs temporels (délai, latence, offre limitée dans le temps).
L'article Computer Communication 23 (PDF) en donne une description globale.
L'article FTRTFT'02 (PDF) décrit le TLSA (Time Labeled Scheduling Automaton).
Une spécification RT-LOTOS peut être exploitée à des fins de validation (simulation/vérification), ou encore à des fins d'ordonnancement.
Le projet RT-LOTOS est supporté essentiellement par l'outil rtl. Cet outil permet les opérations suivantes sur une spécification RT-LOTOS :
- implémenter en Java ou en C++ les types de données définis par l'utilisateur
- simuler une exécution de la spécification
- compiler la spécification en un automate temporisé de type Dynamic Timed Automaton
- produire un graphe de régions de type Minimal Reachability Graph, éventuellement à la volée
Options de rtl (Postscript) (PDF)
Définir ses propres types RT-LOTOS (Postscript) (PDF)
Note : Les codes sources proposés ici ont été testés avec le compilateur gcc version 2.95.3. Il semble que les versions 3.0 et suivantes ne conviennent pas.
Manipulation de graphes
- conseils d'utilisation (Postscript) (PDF)
- dta2dot : pour convertir les graphes (DTA et graphes d'accessibilité) au format .dot
- bcg2dot : pour convertir les graphes du format .bcg au format .dot
Manipulation du DTA
- dtasim : exécute la simulation à partir du DTA
- dta2kronos : convertit le DTA au format Kronos
- dta2rg : construit le graphe (minimal) d'accessibilité (RG) depuis le DTA
Manipulation du graphe d'accessibilité (RG)
- rgrename : renomme les états du graphe d'accessibilité en fonction des numéros d'état du DTA. (lorsque le graphe d'accessibilité est généré à la volée (option -TG2), les numéros d'états ne correspondent pas à ceux du DTA; le problème ne se pose pas avec l'option -TG3)
- dtargmerge : rajoute sur les actions Lotos du graphe d'accessibilité les fonctions C et theta du DTA
- rgstrap : fusionne les noeuds ponctuels dans les noeuds-classe auxquels ils appartiennent, et ce, en consultant les équations des régions
- dtacut : extrait d'un graphe (DTA ou RG) les chemins allant jusqu'aux actions ou états choisis
- rgbcg : convertit le graphe (minimal) d'accessibilité depuis/vers le format .bcg
- rg2tlsa : construit le TLSA depuis le graphe (minimal) (cohérent) d'accessibilité
Divers
- rtl_out_split : découpe la sortie de "rtl -TG3 -p1 ..." pour placer le DTA et le RG dans des fichiers séparés
Download : binaires minimum pour débuter avec RT-LOTOS (pour PC Linux, pour Sun Solaris, et pour PC Windows sous Cygwin)
Présentation des outils
Compréhension d'une spécification
Réalisation d'une spécification
Quizz RT-LOTOS
Exemple académique : croisement ferroviaire
Bugs connus (Postscript) (PDF)
Attention avec les mots réservés
Sous-ensemble du langage reconnu par l'option -cray
Multimédia et Hypermédia
Protocoles de synchronisation Multimédia
Méthodes formelles (applicatif)
Méthodes formelles (théorique)
