OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Mapping RT-LOTOS specifications into Time Petri Nets

Sadani, Tarek and Boyer, Marc and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre Mapping RT-LOTOS specifications into Time Petri Nets. (2006) In: ICFEM'06 - 8th International Conference on Formal Engineering Methods, 01-03 Nov 2006, Macao, China .

(Document in English)

PDF ( Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/11901433_20


RT-LOTOS is a timed process algebra which enables compact and abstract specification of real-time systems. This paper proposes and illustrates a structural translation of RT-LOTOS terms into behaviorally equivalent (timed bisimilar) finite Time Petri nets. It is therefore possible to apply Time Petri nets verification techniques to the profit of RT-LOTOS. Our approach has been implemented in RTL2TPN, a prototype tool which takes as input an RT-LOTOS specification and outputs a TPN. The latter is verified using TINA, a TPN analyzer developed by LAAS-CNRS. The toolkit made of RTL2TPN and TINA has been positively benchmarked against previously developed RT-LOTOS verification tool.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. The definitive version is available at http://www.springerlink.com The original PDF of the article can be found at Lecture Notes in Computer Science website http://dx.doi.org/10.1007/11901433
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Laboratory name:
Deposited On:12 Mar 2009 09:18

Repository Staff Only: item control page