OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Effective representation of RT-LOTOS terms by finite time petri nets

Sadani, Tarek and Boyer, Marc and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre Effective representation of RT-LOTOS terms by finite time petri nets. (2006) In: FORTE'06 - 26th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems, 26-29 Sept 2006, Paris, France .

(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.1007/11888116


The paper describes a transformational approach for the specification and formal verification of concurrent and real-time systems. At upper level, one system is specified using the timed process algebra RT-LOTOS. The output of the proposed transformation is a Time Petri net (TPN). The paper particularly shows how a TPN can be automatically constructed from an RT-LOTOS specification using a compositionally defined mapping. The proof of the translation consistency is sketched in the paper and developed in [1]. The RT-LOTOS to TPN translation patterns formalized in the paper are being implemented. in a prototype tool. This enables reusing TPNs verification techniques and tools for the profit of RT-LOTOS.

Item Type:Conference or Workshop Item (Paper)
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:11 Mar 2009 14:40

Repository Staff Only: item control page