ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne

APPEL À
CONTRIBUTION

Le comité de rédaction du JESA lance un appel à proposition de numéros spéciaux.

En savoir plus >>
Autres revues >>

Journal Européen des Systèmes Automatisés

1269-6935
Revues des Systèmes
 

 ARTICLE VOL 39/1-3 - 2005  - pp.271-286  - doi:10.3166/jesa.39.271-286
TITRE
Validation de spécifications RT-LOTOS. Une interface vers l'outil TINA

RÉSUMÉ
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).


ABSTRACT
RT-LOTOS is a timed process algebra supported by RTL, a formal validation tool using reachability analysis. The need for improving performances in terms of state space exploration and for extending the class of verified properties, has convinced us to develop an interface between RTL and TINA (Time Petri Net Analyzer). That interface relies on RTLOTOS to TPN translation patterns. The latter have been given a formal proof. The paper emphasizes on first experimental results in using RTL2TPN, a translator that we expect to integrate to the toolkit developed for the TURTLE real-time UML profile (Timed UML and RT-LOTOS Environment).


AUTEUR(S)
Tarek SADANI, Pierre DE SAQUI-SANNES, Jean-Pierre COURTIAT

MOTS-CLÉS
RT-LOTOS, réseaux de Petri temporels, analyse d'accessibilité.

KEYWORDS
RT-LOTOS, Time Petri Nets, Reachability Analysis.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (532 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier