OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Validation de spécifications RT-LOTOS : une interface vers l'outil TINA

Sadani, Tarek and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre Validation de spécifications RT-LOTOS : une interface vers l'outil TINA. (2005) In: MSR'05 - Modélisation des Systèmes Réactifs, 05-07 Oct 2005, Autrans, France .

[img] (Document in French)

PDF (Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
406kB

Official URL: http://jesa.revuesonline.com/article.jsp?articleId=6917

Abstract

RT-LOTOS est une algèbre de processus temporisée supportée par RTL, outil de validation formelle utilisant l'analyse d'accessibilité. La recherche de meilleures performances en termes d'exploration de l'espace d'états et le besoin d'étendre les classes de propriétés vérifiées, ont motivé le développement d'une interface entre RTL et l'analyseur de réseaux de Petri temporels TINA. Cette interface repose sur des schémas de traduction de RT-LOTOS vers les RdPT. Ces schémas ont fait l'objet d'une preuve. Cet article met l'accent sur les premiers résultats expérimentaux obtenus avec RTL2TPN, un traducteur qui a vocation à intégrer la chaîne d'outils développés pour le profil UML temps réel TURTLE (Timed UML and RT-LOTOS Environment).

Item Type:Conference or Workshop Item (Paper)
Additional Information:Actes publiés dans N° spécial du Journal Européen des Systèmes Automatisés (JESA), vol. 39 (n° 1-3). pp. 271-286. ISSN 1269-6935
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE
French research institutions > Centre National de la Recherche Scientifique - CNRS
Laboratory name:
Statistics:download
Deposited By: Pierre de Saqui-Sannes
Deposited On:12 Mar 2009 10:55

Repository Staff Only: item control page