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 description technique, which is a formalism suited for applications where concurrency, complex synchronization patterns, asynchronous interactions and timing constraints have to be dealt with together. The paper does not emphasize the details of the RT-LOTOS formal semantics, but intends to explain and illustrate its main features, as well as the main capabilities of its associated software tool rtl. Last, but not least, the paper reports on different applications and case studies that have recently been developed at LAAS-CNRS, some of them in cooperation with the industry. Key words: Formal Specification and Verification, LOTOS, RT-LOTOS, Timed Automata, Temporal consistency

• Type: Journal
• Year: 2000
• Where: COMCOM
• Authors: Jean-Pierre Courtiat, C. A. S. Santos, Christophe Lohr, B. Outtaj
• Keywords: COMCOM 2000, Complex Synchronization Patterns, Formal Description Technique, RT-LOTOS Formal Semantics