Robustness of timed automata : computing the maximally-permissive strategies
Robustesse des automates temporisés : calculer les stratégies les plus permissives
Résumé
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.
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.
Origine : Version validée par le jury (STAR)