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 448kB |
Official URL: http://dx.doi.org/10.1007/11888116
Abstract
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: | Département de Mathématiques, Informatique, Automatique - DMIA (Toulouse, France) - Modelisation et Architecture des Systèmes - MARS Institut de Recherche en Informatique de Toulouse - IRIT (Toulouse, France) Laboratoire d'Analyse et d'Architecture des Systèmes - LAAS (Toulouse, France) - Outils Logiciels pour la Communication - OLC |
| Statistics: | download |
| Deposited On: | 11 Mar 2009 14:40 |
Repository Staff Only: item control page
