Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique

This paper is devoted to the presentation of the RT-LOTOS formal descriptio n technique, which is a formalism suited for applications where: concurrenc y, complex synchronization patterns, asynchronous interactions and timing c onstraints have to be dealt with together. The paper does not emphasize the details of the RT-LOTOS formal semantics, but intends to explain and illus trate its main features, as well as the main capabilities of its associated software tool rtl. Finally, this paper reports on different applications a nd case studies that have recently been developed at LAAS-CNRS, some of the m in cooperation with the industry. (C) 2000 Elsevier Science B.V. All righ ts reserved.