OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

From RT-LOTOS to Time Petri Nets new foundations for a verification platform

Sadani, Tarek and Courtiat, Jean-Pierre and Saqui-Sannes, Pierre de From RT-LOTOS to Time Petri Nets new foundations for a verification platform. (2005) In: SEFM'05 - 3rd IEEE International Conference on Software Engineering and Formal Methods, 05-09 Sept 2005, Koblenz, Germany .

(Document in English)

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

Official URL: http://dx.doi.org/10.1109/SEFM.2005.22


The formal description technique RT-LOTOS has been selected as intermediate language to add formality to a real-time UML profile named TURTLE. For this sake, an RT-LOTOS verification platform has been developed for early detection of design errors in real-time system models. The paper discusses an extension of the platform by inclusion of verification tools developed for Time Petri Nets. The starting point is the definition of RT-LOTOS to TPN translation patterns. In particular, we introduce the concept of components embedding Time Petri Nets. The translation patterns are implemented in a prototype tool which takes as input an RT-LOTOS specification and outputs a TPN in the format admitted by the TINA tool. The efficiency of the proposed solution has been demonstrated on various case studies.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to the Institute of Electrical and Electronics Engineers (IEEE). The original PDF can be found on the IEEE website: http://ieeexplore.ieee.org/search/selected.jsp
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:40

Repository Staff Only: item control page