OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Recherche d’efficacité en vérification de modèles UML temps réel traduits en RT-LOTOS

Sadani, Tarek and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre Recherche d’efficacité en vérification de modèles UML temps réel traduits en RT-LOTOS. (2006) In: AFADL'06 - Approches Formelles dans l'Assistance au Développement de Logiciels, 15-17 march 2006, Paris, 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
641kB

Official URL: http://cedric.cnam.fr/AFADL06/index.php

Abstract

Le fait de doter le profil UML temps réel TURTLE d'une sémantique formelle par traduction vers l'algèbre de processus temporisée RT-LOTOS a permis de réutiliser en contexte UML l'outil de validation formelle RTL développé pour RT-LOTOS. Cet article montre comment le profil TURTLE bénéficie maintenant des travaux les plus récents sur la traduction de spécifications RT-LOTOS vers les réseaux de Petri temporels supportés par l'outil TINA. Des schémas de traduction ont été prouvés et implantés. L'on profite ainsi des performances à l'exécution de TINA et des constructions que cet outil implante en fonction des classes de propriétés à vérifier.

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
French research institutions > Centre National de la Recherche Scientifique - CNRS
Laboratory name:
Statistics:download
Deposited By: Pierre de Saqui-Sannes
Deposited On:11 Mar 2009 14:25

Repository Staff Only: item control page