[Accueil bibliotech]
Accueil > Les thèses en ligne de l'INP

Vers l'utilisation des réseaux de Petri temporels étendus pour la vérification de systèmes temps-réel décrits en RT-LOTOS

Sadani, Tarek (2007) Vers l'utilisation des réseaux de Petri temporels étendus pour la vérification de systèmes temps-réel décrits en RT-LOTOS. (Using extended time Petri nets for the verification of real-time systems deescribed in RT-LOTOS.)

Texte intégral disponible au format :

PDF - Nécessite un logiciel de visualisation PDF comme GSview, Xpdf ou Adobe Acrobat Reader
2.39 Mo

Résumé

Cette thèse porte sur la vérification formelle de systèmes temps réel et procède par transformation de modèle entre l'algèbre de processus temporisée RT-LOTOS et les réseaux de Petri temporels étendus par des chronomètres et des données. Des schémas de traduction de RT-LOTOS vers ces réseaux de Petri étendus sont proposés et formellement prouvés. L'approche transformationnelle développée pour la partie "contrôle" de RT-LOTOS est étendue à la partie "données". Le langage RT-LOTOS est lui même enrichi d'un opérateur de suspension reprise qui permet de modéliser et vérifier une classe plus large de systèmes temps réel Plusieurs études de cas attestent de l'efficacité des schémas de traduction proposés par rapport à des outils LOTOS ou RT-LOTOS développés antérieurement. L'approche proposée s'avère transposable à d'autres langages de modélisation en particulier le profil UML temps réel TURTLE (Timed UML and RT-LOTOS Environment). ABSTRACT : This thesis addresses real-time systems, using a transformational approach. The timed process algebra RT-LOTOS serves as source language. Extended Petri nets with stopwatches and data serve as target language. Rt-LOTOS to extended Petri nets translation patterns are proposed and formally proved. The transformational approach developed for the control part is extended to the data part. The RT-LOTOS language is enhanced with a suspend /resume operator, thus extending the class of real-time systems that can be modelled and verified . The efficiency of the new approach is demonstrated on various case studies that include comparisons with LOTOS and RT-LOTOS tools that had been developed before. The proposed approach may be applied and extended to other modelling languages, in particular the real-time UML profile TURTLE (Timed UML and RT-LOTOS Environment).

Département ou laboratoire:Laboratoire d'Analyse et d'Architecture des Systèmes - LAAS (Toulouse, France)
Directeur de thèse:Courtiat, Jean-Pierre et Saqui-Sannes, Pierre
Mots-clés:Systèmes temps-réel - Vérification formelle – Préemption – RT-LOTOS - Réseaux de Petri temporels - UML. KEYWORDS : Real-time systems - Formal verification, Pre-emption, RT-LOTOS, Time Petri nets, UML
Sujets:Informatique > Systèmes informatiques
Déposé le:09 Juillet 2007

Administrateur seulement : modifier cet enregistrement


Contacts | Infos légales | Plan du site | Intranet

(c)INP de Toulouse 2012 - Tous droits réservés. -  INP Communication