A Reachability Analysis of RT-LOTOS Specifications

The paper deals with the verification of RT-LOTOS specifications, RT-LOTOS being an acronym of Real-Time LOTOS, a temporal extension of the LOTOS FDT. Verification is performed by reachability analysis of a timed automaton model into which a RT-LOTOS specification may be automatically translated. Two main contributions are brought by this paper: the definition of a new timed automaton model, the dynamic timed automaton model which is particularly suitable for taking into account non regular RT-LOTOS processes, and the elaboration of a new method for translating a temporal process algebra into a timed automaton model, the so-called structural induction method. The main advantage of the proposed approach, with respect to others methods presented in the literature, is that the reachability analysis may be performed on the fly when generating the timed automaton model. The proposed approach has been fully implemented in the RTL tool (RT-LOTOS Laboratory) and several verification results ar..