Uma ferramenta para auxílio no processo de verificação de especificações em RT-LOTOS - Martins, Ricardo Ferreira; Camargo, Murilo Silva de; Farines, Jean-Marie (Anais do Simpósio Brasileiro de Engenharia de Software (SBES); 1996: Anais do X Simpósio Brasileiro de Engenharia de Software, 1996)
In this paper, we present a methodology and tools for verifying specifications of real-time systems, written in RT-LOTOS, a timed extension of the LOTOS specification language. From the model in RT-LOTOS, it is generated the related Timed Automata, over which the verification can be done, by using formulas written in the TCTL Real-Time Temporal Logic. The translator of RT-LOTOS specifications into Timed Automata that was built is described in this work. His integration with existing tools that allow the verification is also shown. Finally, case-studies allow to analyze the use of this method and the tools presented.