Université de Rennes 1 Robustness of timed automata : computing the maximally-permissive strategies Robustesse des automates temporisés : calculer les stratégies les plus permissives Vérification de modèlesOptimisationRobustesseAutomates temporisés Model checkingOptimisationRobustnessTimed automata Commande robuste Vérification de modèles (informatique) Automates temporisés Les systèmes temps-réels nécessitent parfois d’être prouvés formellement, en particulier les systèmes temps-réels contenant des parties critiques, comme les avions, les voitures... Les automates temporisés constituent un modèle mathématique commode pour cela. Cependant, même s’ils fournissent une représentation des aspects temporels de ces systèmes, les automates temporisés supposent une précision arbitraire et des actions immédiates. C’est pourquoi même si un état est déclaré atteignable dans un automate temporisé, il est parfois impossible de l’atteindre dans le système physique qu’il modélise. Le but de cette thèse est de modéliser un type de perturbations, sur des délais, pour les automates temporisés et de calculer les stratégies les plus permissives afin de régler ce problème d’imprécision. Ces stratégies élargiront les délais uniques habituellement proposés en des intervalles de délais et chercheront à atteindre un des états finaux de l’automate quel que soit le délai dans l’intervalle proposé qui a eu lieu. Real-time systems sometimes need to be formally proven, especially realtime systems containing critical component, as planes, cars etc. Timed automata provide a convenient mathematical model for this. However, although they provide a representation of the temporal aspects of these systems, timed automata assume arbitrary precision and zero-delays actions. Therefore, even if a state is declared reachable in a timed automaton, it is sometimes impossible to reach it in the physical system it models. The aim of this thesis is to model a type of perturbation, on delays, for timed automata and to compute the most permissive strategies to solve this imprecision problem. These strategies propose intervals of delays instead of the usually proposed single delays. These strategies seek to reach one of the final states of the automaton regardless of the delay, in the proposed interval, that has occurred. Electronic Thesis or DissertationText en application/pdf1 : 1871 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/70a2b5cb-5b57-47e5-ad01-03adb56c7e3f Clément Emily 1994-03-07 FR 262354896 clement.mily@gmail.com 2022REN1S006 http://www.theses.fr/2022REN1S006 2022-03-11 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiJéronThierryintervenant_1095612777MarkeyNicolasintervenant_2073426482ReynierPierre-Alainintervenant_319709340XBérardBéatriceintervenant_6029892740ChatainThomasintervenant_7095210210MentréDavidintervenant_805850317XDimaCatalinintervenant_4060908580CassezFranckintervenant_5066875927 MATHSTICecoleDoctorale_1 204770424 INRIA-RENNES partenaireRecherche_1 133175863 ddc:004 JéronThierryMarkeyNicolasReynierPierre-AlainDimaCatalinCassezFranckBérardBéatriceChatainThomasMentréDavidUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes) INRIA-RENNES ASCII PDF 1916083