Groupe OLC
Outils et Logiciels pour la Communication

Projet
de
Recherche









Distribution de
RT-LOTOS
Real Time Language Of Temporal Ordering Specification

Table des matières

Le logiciel rtl est une implémentation du langage de description formelle de contraintes temps-réel RT-LOTOS. Cette implémentation a été développée au LAAS (Laboratoire d'Analyse et d'Architectures des Systèmes) unité propre du CNRS (Centre National de la Recherche Scientifique) au sein du groupe OLC (Outils Logiciels pour la Communication) par l'équipe SFP (Spécification Formelle de Protocoles).

1  Version

2  Installation

Le logiciel rtl et l'ensemble de ses composants s'installent par défaut dans le répertoire RT-LOTOS créé dans le répertoire courant de l'utilisateur.
Remarques
pour compiler rtl :

3  Description

Attention :
il s'agit d'une pré-version, et non d'une distribution finalisée. Certains éléments sont encore en développement et susceptibles d'être modifiés dans des versions ultérieures.

Le répertoire de rtl est organisé ainsi : 
             .
             |
             +--bin
             |
             +--class
             |
             +--doc
             |
             +--exemples
             |   |
             |   +--FSPj
             |   |
             |   +--LipSynchro-2
             |   |
             |   +--stop&wait
             |
             +--include
             |
             +--lib
             |
             +--src
             |   |
             |   +--lib
             |   |
             |   +--rtl
             |
             +--users-types
                 |
                 +--c++
                 |
                 +--java
bin :
le code binaire des programmes liés à RT-LOTOS
rtlfig :
utilitaire permettant de générer des chronogrames (graphiques au format xfig) à partir des traces de simulation (fichiers .sim)
figall :
script exécutant rtlfig sur tous les signaux d'une spécification


class :
les classes java nécessaires à l'exécution de rtl avec des types implémentés en java

doc :
quelques explications pour appréhender l'outil rtl
README.[txt|tex] :
ce que vous lisez en ce moment
options-rtl.[txt|tex] :
les différentes options supportées par rtl
librtl-doc.tex :
documentation explicitant l'art et la manière de créer ses propres types.
Faites make pour compiler les documents latex (fichiers .tex).

exemples :
quelques exemples d'utilisation de rtl
stop&wait
: exemple basique du langage RT-LOTOS
LipSynchro-2
: exemple complet avec utilisation de types implémentés en c++
Faites make cclib pour créer les types c++, puis make.
FSPj :
exemple complet avec utilisation de types implémentés en java
Faites make jlib pour créer les types java, puis make.


include :
les includes nécessaires à l'écriture de types en c++

lib :
les librairies utilisées par rtl
libRJInterfaceSocket.so :
pour la machine java communiquant par socket
libRJInterfaceShMem.so :
pour la machine java communiquant par mémoire partagée
librtlsys.so :
pour la vérification de l'automate


src :
les sources de rtl et des librairies (disponibles uniquement dans la version avec sources)
lib :
sources des librairies pour les types c++ et java
rtl :
sources de rtl


users-types :
ensembles de types utilisateurs classiques en c++ et en java
HOW_TO_USE.txt :
l'art et la manière d'utiliser les types proposés
README.txt :
description des types proposés
c++ :
sources des types écrits en c++
c++/librtltypes.a :
librairie statique contenant tous ces types déjà compilés et prêts à l'emploi
java :
sources et classes des types écrits en java

4  Documentation

5  Variables d'environnement

Le futur utilisateur de rtl va être amené à ajouter le chemin d'accès aux composants de rtl à certaines variables de son environnement :

6  Utilisation

La commande de base est rtl (RT-LOTOS/bin/rtl).
L'ensemble des options disponibles peut être affiché par rtl -help.
Typiquement la simulation d'une spécification Lotos se fait par la commande :
 $ rtl specifcation.lot
où ``specifcation.lot'' est le nom du fichier contenant la spécification RT-LOTOS des processus à simuler. Ce fichier DOIT avoir l'extension ``.lot''.

rtl effectue alors la simulation et génère un fichier de trace de la simulation portant le nom specification.lot.sim.
Chaque ligne de ce fichier de trace comprend 3 champs :
  1. le temps interne de rtl
  2. le signal ou la porte sur laquelle se sont synchronisés deux processus
  3. le numéro de l'état de l'automate
Il est ensuite possible de visualiser l'occurrence de certains signaux par la commande rtlfig, ou encore d'appliquer des filtres awk, perl,... pour réaliser des mesures sur la simulation (regardez dans les répertoires RT-LOTOS/exemples/*/Plot).

7  Assistance

Pour tout problème lié à l'utilisation de cette version de rtl, contactez Christophe Lohr.

 Retour au projet RT-LOTOS

Ce document a été traduit de LATEX par HEVEA.