OLC Group Outils et Logiciels pour la Communication Software and Tools for Communicating Systems

Research Project

Version Française

English Version

The RT-LOTOS (Real-Time LOTOS) Project

Leader: Jean-Pierre COURTIAT (e-mail: courtiat@laas.fr )

Team members (former and current):

• Roberto Cruz de Oliveira Universidade Federal Fluminense, Niteroi, Brazil
• Djamel Saidouni Université de Constantine, Constantine, Algeria
• Murilo Silva de Camargo Universidade de Brasilia, Brasilia, Brazil
• Rosvelter Coelho da Costa Universidade Federal de Santa Catarina, Florianópolis, Brazil
• Laurent Andriantsiferana Cisco, San Jose, USA
• Celso Saibel Santos Universidade Unifacs, Salvador, Brazil
• Christophe Lohr LAAS-CNRS
• Paulo Sampaio Universidade Unisantos, Santos, Brazil

Presentation of the project

The RT-LOTOS language makes it possible to formally describe systems subject to time constraints. It is a process algebra language. It extends the LOTOS language by temporal operators (time, latency, time limited offering).

The paper Computer Communication 23 (PDF) provide a global description of RT-LOTOS.
The paper FTRTFT'02 (PDF) describe the TLSA (Time Labeled Scheduling Automaton).

An RT-LOTOS specification may be used for validation (simulation/verification) or scheduling purpose.
The RT-LOTOS project is supported mainly by the rtl tool. This tool allows the following operations on a LOTOS specification:

• to implement in Java or C++ the data types defined by the user
• to simulate an execution of the specification
• to compile the specification in a timed automaton (called type Dynamic Timed Automaton)
• to produce a region graph (called Minimal Reachability Graph), possibly on the fly

How to use rtl tool?

rtl options (Postscript) (PDF)
To define his/her own types in RT-LOTOS (Postscript) (PDF)

How to install rtl tool?

• Distribution content (Postscript) (PDF)
• Sources distribution

Note: The sources here were tested with gcc version 2.95.3. It seems that versions 3.0 and following are not appropriate.

Complementary tools

Handling of graphs

• Guidelines (Postscript) (PDF)
• dta2dot: it converts graphs (DTA and reachability graphs) to the .dot format
• bcg2dot: it converts graphs from the .bcg format to the .dot format

Handling of the DTA

• dtasim: it carries out a simulation starting from the DTA
• dta2kronos: it translates DTA into the Kronos format
• dta2rg: it built the (minimal) reachability graph (RG) starting from the DTA

Handling of the reachability graph (RG)

• rgrename: it renames nodes of the reachability graph according to the corresponding DTA states numbers. (when the reachability graph is generated on the fly (option -TG2), states numbers do not correspond to those of the DTA; the problem does not arise with the option -TG3)
• dtargmerge: it adds to the LOTOS actions of the reachability graph the C and theta functions coming from the DTA
• rgstrap : it merges the ponctual nodes in the reachability graph to the region they belong, and this, taking into accound the equations defining the bounding regions
• dtacut: it extract from a graph (DTA or RG) the paths going to the selected actions or states
• rgbcg: it translates (minimal) reachability graph from/to the .bcg format
• rg2tlsa: it builds the TLSA starting from the (consistent) (minimal) reachability graph

Others

• rtl_out_split: it splits output of "rtl -TG3 -p1 ..." to store DTA and RG in separate files

Tutorial

Download: minimal binaries to begin with RT-LOTOS (for PC Linux, Sun Solaris, and PC Windows under Cygwin)
Tool presentation
Reading a specification
Writing a specification
RT-LOTO quizz
An academic example: railway crossing

Some experiments

Known bugs (Postscript) (PDF)
Pay attention to reserved words
Subset of the language recognized by option -cray

Main publications

Multi-media and Hypermedia
Multi-media synchronization protocols
Formal methods (applications)
Formal methods (theoretical)

Back to OLC group