Database of Research Tools Developed Using CADP

Analysis of Real-Time Systems Described in RT-LOTOS

Organisation: LAAS-CNRS (Toulouse, FRANCE)

Functionality: Real-Time Systems.

Tools used: rtl (Real-Time LOTOS Laboratory)
CADP (Construction and Analysis of Distributed Processes)

Period: 2002

Description: RT-LOTOS (Real-Time LOTOS) is an extension of the LOTOS formal description technique dedicated to the description of dense time behavioural aspects. The extensions consist of three timing operators:

  • A deterministic delay operator delay (d) expressing that a process must wait an amount of time d before proceeding.
  • A non-deterministic delay operator latency (l) expressing that a process must wait an amount of time chosen non-deterministically in the latency interval [0, l].
  • A time restriction operator g{t} limiting the amount of time during which an observable action g may be offered to the environment.
RT-LOTOS allows to express, at a high abstraction level, a real-time system as the composition of real-time constraints. An interesting problem in this context is to exhibit the set of system behaviours which are coherent w.r.t. a given application domain (e.g., multimedia documents). This can be achieved by synthesizing a TLSA (Time Labelled Scheduling Automaton), which is a new kind of timed automaton allowing to capture all temporal constraints of a system using a single clock.

The synthesis procedure of a TLSA from an RT-LOTOS specification consists in generating the corresponding region graph (RG) using the rtl tool, followed by several transformations of the RG (projection, minimisation, etc.) and by the effective synthesis of a TLSA. The minimisation step is performed using the bcg_min tool of CADP. To achieve this, two new tools named rg2bcg and bcg2rg have been developed for translating a RG into a BCG file and vice-versa. The regions of the RG are identified in the resulting BCG file by adding to states special looping transitions that carry region information generated by rtl.

Conclusions: A method for analysing real-time systems specified in RT-LOTOS has been presented. The method is based on the construction of a TLSA expressing all coherent system behaviours. The preliminary phases of the construction method use the rtl tool for generating the region graph associated to a RT-LOTOS specification, and (by means of two new tools rg2bcg and bcg2rg implementing translations between region graphs to BCG files) the bcg_min tool of CADP for minimizing the region graph. The method was successfully applied to the analysis and presentation of multimedia systems.

Publications: [Lohr-02] "Contribution to the Design of Real-Time Systems Based on the RT-LOTOS Formal Description Technique". PhD thesis (in French), Institut National Polytechnique de Toulouse, December 2002.
Available on-line at: http://www.laas.fr/~lohr/bibliography/these_lohr_2002-12-19.pdf
or from our FTP site in PDF or PostScript
Contact:
Christophe Lohr
LAAS-CNRS, OLC Group
7, avenue du Colonel Roche
F-31077 Toulouse Cedex 4
France
Tel: +33 (0)5 61 33 69 07
Fax: +33 (0)5 61 33 64 11
E-mail: lohr@laas.fr



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page