ISBN-13: 9783838171975 / Francuski / Miękka / 2018 / 144 str.
Les systA]mes dynamiques hybrides sont des systA]mes dynamiques faisant intervenir explicitement et simultanA(c)ment des phA(c)nomA]nes ou des modA]les de type dynamique continu et A(c)vA(c)nementiel. Dans cette thA]se, nous proposons des techniques algorithmiques de vA(c)rification formelle de propriA(c)tA(c)s pour ces systA]mes. Ces techniques de vA(c)rification se basent sur le calcul de l'espace atteignable A partir d'une rA(c)gion initiale pour dA(c)terminer si l'intersection de cet espace avec le domaine A A(c)viter est bien vide. Notre mA(c)thode consiste A partitionner l'espace d'A(c)tat du systA]me complexe en rA(c)gions et A approximer pour chacune de ces rA(c)gions la dynamique du systA]me A(c)tudiA(c) par une dynamique plus simple. Nous prA(c)sentons des extensions A une proposition prA(c)cA(c)dente afin de prendre en compte des incertitudes dans les dynamiques affines. Dans un premier temps cette incertitude est considA(c)rA(c)e comme invariante. Dans un second temps nous la considA(c)rons variante. Cette deuxiA]me extension permet de considA(c)rer l'atteignabilitA(c) des systA]mes non-linA(c)aires.
Les systèmes dynamiques hybrides sont des systèmes dynamiques faisant intervenir explicitement et simultanément des phénomènes ou des modèles de type dynamique continu et événementiel. Dans cette thèse, nous proposons des techniques algorithmiques de vérification formelle de propriétés pour ces systèmes. Ces techniques de vérification se basent sur le calcul de lespace atteignable à partir dune région initiale pour déterminer si lintersection de cet espace avec le domaine à éviter est bien vide. Notre méthode consiste à partitionner lespace détat du système complexe en régions et à approximer pour chacune de ces régions la dynamique du système étudié par une dynamique plus simple. Nous présentons des extensions à une proposition précédente afin de prendre en compte des incertitudes dans les dynamiques affines. Dans un premier temps cette incertitude est considérée comme invariante. Dans un second temps nous la considérons variante. Cette deuxième extension permet de considérer latteignabilité des systèmes non-linéaires.