Étude sur l'exécution des stratégies UppaaL-TIGA pour Dala

Matthieu Gallien

Description

Étude surl’exécution desstratégiesUppaaL TIGA pourDalaMatthieu GallienIntroductionÉtude sur l’exécution des stratégies PrésentationTravail en coursUppaaL TIGA pour Dala Le modèleL’exécutionPerspectivesComparaisonIxTeT/Uppaal tigaMatthieu Gallien Validation de modèle IxTeTConclusionLaboratoire d’Analyse et d’Architecture des SystèmesRéunion Toulouse 10 janvier 2007Étude surIntroduction l’exécution desstratégiesUppaaL TIGA pourDalaMatthieu GallienI Comparer l’approche actuelle du planificateur IxTeTIntroductionà une approche jeu d’automate temporisé.PrésentationTravail en coursLe modèleI L’exécutionProduire des plans robustesPerspectivesComparaisonIxTeT/Uppaal tigaValidation de modèle IxTeTI Produire des plans de bonne qualité (comparé auxConclusionplans IxTeT)I Utilise l’outil UppaaL tiga pour résoudre les jeux(limitations due à la fermeture du code)Étude surPlan l’exécution desstratégiesUppaaL TIGA pourDalaMatthieu GallienPrésentationIntroductionPrésentationTravail en coursTravail en coursLe modèleL’exécutionLe modèlePerspectivesL’exécutionComparaisonIxTeT/Uppaal tigaValidation de modèle IxTeTConclusionPerspectivesComparaison IxTeT/Uppaal tigaValidation de modèle IxTeTConclusionÉtude surSchéma général l’exécution desstratégiesUppaaL TIGA pourDalaMatthieu GallienIntroductionUppaaL-tiga PrésentationTravail en coursLe modèleL’exécutionGUI verifytgaPerspectivesComparaisonDala IxTeT/Uppaal tigaValidation ...

Informations

• Publié par: Unyu
• Nombre de lectures: 93
• Langue: Français

Extrait

Étudesur l’exécuitnoed s s rttagéei pp s UL-aaGATIurpo alaD ttaMueihllaG ntro ien Iion P duct tntaéres arav oi T n urcoenil èlodem s L ucéxe’L e sreP noit oCpmraia eptcvise /Uppaal- son IxTeT itadedno agit ilaVTTedèmoIxle

Réunion Toulouse 10 janvier 2007

Matthieu Gallien

Laboratoire d’Analyse et d’Architecture des Systèmes

Étude sur l’exécution des stratégies UppaaL-TIGA pour Dala

Conclusion

edusÉut éxucl r e’ GATIurpopp s UL-aa tarteigé noit s sed duction P ien Intro ihueaGll aDal aMtt èlodem s L urcoenilavarT noitatnesér araiComp ivespectePsr itnoéxucL e e’ Ixledèmo clon T C Te noisu xTeT son Iaal-/Upp aVil itag noedadit

I Utilise l’outil UppaaL-tiga pour résoudre les jeux (limitationsdue à la fermeture du code)

I Comparer l’approche actuelle du planificateur IxTeT à une approche jeu d’automate temporisé.

Introduction

I des plans de bonne qualité (comparé auxProduire plans IxTeT)

I Produire des plans robustes

tiga Vali /Uppaal- omèdelxIaditnoedTTe

Conclusion

Introduction

Présentation

Travail en cours Le modèle L’exécution

Conclusion

Perspectives Comparaison IxTeT/Uppaal-tiga Validation de modèle IxTeT

Travail en cours Le modèle L’exécution

Plan

Présentation

l r e’éxucitnoed s s Étudesu einaGllihuettMa laDa urpoGATI-LaappU seigétart son IxTeT Comparai eptcviseePsr

Schéma

général

l’e É x t é u c d u e it s o u n r eds

stratégies UppaaL-TIGA pour Dala

Matthieu Gallien

Introduction

Présentation

Travail en cours

Le modèle

L’exécution

Perspectives

Comparaison IxTeT/Uppaal-tiga

Validation de modèle IxTeT

Conclusion

avTrleai taenonti èdom ’L el uocn eL sr uGallien a Matthie itno rPsé nIrtdocu Up esgitérast esnd laD ruopAGIT-Laap Ét tuoixecé ru ’l duse lèIeTxTe oCcnulison pU/TeTxIgit-laap atidal a Vodemndio tuoixecé psceP n res Com tive isonpara

I Une stratégie (ou police d’exécution) UppaaL-tiga : unplan particulier

I Exécution du type : exécution/replanification

I Intégration dans l’architecture LAAS à la place d’IxTeT

I Un plan IxTeT : unepolice d’exécution particulière

I Plan robuste : cas d’échecs prévus et anticipés

Schéma général

aison IxT es Compar sreptcvi ucitno eP modeledèdalionti it-l aV agU/Teaapp oinlcsuC T no xIeT us l r e’éxucitnoed Étude IT-LopAG aD ru aM al tr s ségats U ie aapp tcoiorud estnP n ér euGatthin Int llie domeL sru éxe’L elè ra n T ioat coenilva

I Possibilité de modéliser de nouveaux domaines efficacement (tâche d’observation)

I Moteur d’exécution en cours d’implémentation

État des lieux

I Toujours des limitations sur la forme des tâches modélisables

I Pas de gestion des ressources numériques

I Prise en compte d’échecs modélisés à priori (plus fort que les incertitudes temporelles)

onisrapaom s C veticepsreP noitucéxe le L’ modè rs Le ncouiaelrTva itnoneat IelèTeTxiondemod a Validat aplat-gixIeT/TpU ’l rusedu oitucéxe Ét rtnIcudonoit sérP at a MiethaluGenli apLaT-GIpAuo D r la ndes stratégies Up

< t e m p l a t e ><name>MOVE< / name> < d e c l a r a t i o n > . . . < / d e c l a r a t i o n > < l o c a t i o n . . . > <name . . . > q_RB_STATUS_RECOV< / name> . . . < / l o c a t i o n > . . . < t r a n s i t i o n c o n t r o l l a b l e = " f a l s e " > . . . < / t r a n s i t i o n > < t r a n s i t i o n > . . . < / t r a n s i t i o n > . . . < / t e m p l a t e >

Exemple

Conclusion

Exemple

Étude sur l’exécution des stratégies UppaaL-TIGA pour Dala

Matthieu Gallien

Introduction

Présentation

Travail en cours

Le modèle

L’exécution

Perspectives

Comparaison IxTeT/Uppaal-tiga

Validation de modèle IxTeT

Conclusion

sreP noit sevitcep aiarmpCo eTxT n I so aa-lU/pp aVil itag ondedatileIxmodè ueihllaG I nei ortnctdun P io seréatntoi T n aravlineocrus Lemodèle L’exécu sudetuÉ s sednoitucéxe’l r aaL- s Upp égietrat aMtt aDal opruITAG nusiooncl TeT C

State: ( MOVE.q_ _ _ RB STATUS STL MOVE_PAN_TILT_UNI q_PAN_ _ T. TILT STRG TAKE_PICTURE1.q PIC NONE ... _ _ VISIBILITY_WINDOW_W2.q_VW OUT ) _ v MOVEPTU USEFULL=1 v AT RBT X=5 _ _ _ _ _ _ _ _ _ _ v AT RBT Y=-5 v MOVE USEFULL=1 v CAMERA=1 ... _ When you are in (t<40) || (40<=t && t<100) || (100<=t && t<=110), take transition MOVE.q_RB_ _ .q_R _ _ STATUS STL->MOVE B STATUS MOVE {... }

Exemple

M a tahteiG r u e l P ai c l e n p e sveti om s Crapaonis sedn artsigét pU se aLpaIG-TouAp al r D TeTxIelè tÉur l’ udes utioexéc /TpUxIeTt-giapla idat a Valemodiond

Présentation

Introduction

Travail en cours Le modèle L’exécution

Présentation

Conclusion

Perspectives Comparaison IxTeT/Uppaal-tiga Validation de modèle IxTeT

Travail en cours Le modèle L’exécution

Plan

Conclusion

Étudesur l’exé n Int llie ctiorodu al aM ru aD ueaGttih aapp s U ie poGATIL- ednoituc gétarts s se oCpmra sreptcvi cution Pe èle L’exé L sru dome liavocne ioat ra n T ré n Pntse oinlcsu T Con IxTedèledemonoitadilaV agit-laapp/UeTxT n I soai

I Possibilité qu’un déplacement de la platine PAN&TILT puisse emmener ailleurs (valeur spéciale reprise d’IxTeT)

I Expérimentation sur le MOVE et le MOVEPTU.

I Possibilité qu’un déplacement du robot finisse nulle part (valeur spéciale)

I Nécessité de limiter les aspects combinatoires

I Le prochain déplacement de la même durée réussira (forte approximation)

Prise en compte d’effets non nominaux

I Compromis raisonnable entre robustesse et qualité de la solution (à confirmer)