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