Retour à l'accueil Retour à l'accueil Société des ingénieurs de l'automobile Français - English
  RECHERCHE  
 
  Recherche avancée Recherche  
     
     
 
La SIA
Présentation
Vie de la SIA
Adhésion
Annuaire des membres
Partenaires
Sections Techniques
Sections Régionales
Sections Étudiants
 
 
Panier
Contactez-nous
Plan d'accès
Mentions légales
Plan du site
 
 
centralweb-référencement
 
Détail de la publication


 
Catégorie : SIA/Articles techniques
Titre :Formal and efficient verification techniques for Real-Time UML models
Edition :SIA
Date :25/01/2006
Auteur :Tarek SADANI, Pierre de SAQUI-SANNES – ENSICA and LAAS- CNRS, France
Jean-Pierre COURTIAT – LAAS-CNRS, France
Langue :English
Format :Fichier PDF
( livraison exclusivement par télechargement)
Nbre de pages :8
Code :R-2006-01-3B1

The real-time UML profile TURTLE has a formal semantics expressed by translation into a timed process algebra: RT-LOTOS. RTL, the formal verification tool developed for RT-LOTOS, was first used to check TURTLE models against design errors. This paper opens new avenues for TURTLE model verification. It shows how recent work on translating RT-LOTOS specifications into Time Petri net model may be applied to TURTLE. RT-LOTOS to TPN translation patterns are presented. Their formal proof is the subject of another paper. These patterns have been implemented in a RT-LOTOS to TPN translator which has been interfaced with TINA, a Time Petri Net Analyzer which implements several reachability analysis procedures depending on the class of property to be verified. The paper illustrates the benefits of the TURTLE-

>RT-LOTOS->TPN transformation chain on an avionic case study.

 



Ajouter au panier

Retour Articles techniques



Société des Ingénieurs de l’Automobile - 79 rue Jean-Jacques Rousseau - 92158 SURESNES Cedex - Tel : 01 41 44 93 70 | info@sia.fr © 2006 SIA