OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

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. 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. PhD, Institut National Polytechnique de Toulouse, 2007

[img]
Preview
(Document in French)

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
2449Kb

Official URL: http://ethesis.inp-toulouse.fr/archive/00000460/

Abstract

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).

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut National Polytechnique de Toulouse - INPT
Laboratory name:
Research Director:
Courtiat, Jean-Pierre and Saqui-Sannes, Pierre
Statistics:download
Deposited By:admin admin

Repository Staff Only: item control page