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 the CADP Web 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

Back to the CADP research tools page