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]](https://oatao.univ-toulouse.fr/style/images/fileicons/application_pdf.png) |
(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-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 |
| Statistics: | download |
| Deposited On: | 11 Mar 2009 14:25 |
Repository Staff Only: item control page
