Le modèle réseaux de Petri temporisés stochastiques: extensions et applications

This thesis is submitted within the framework of formal description techniques used during the design process of real-time distributed systems. More precisely, it concerns the extension of the expression and analysis powers of the Stochastic Timed Petri Nets model (STPN). This model associates to each transition of a Petri Net a time interval and a density probability function on this interval (a lot of time characteristics can thus be represented and, in particular, time constraints). The expression power improvement concerns the introduction, on the one hand, of the age memory concept (which allows to study preemption mechanisms and is very useful in scheduling algorithms and dependability analysis) and, on the other hand, of several transition firing rules (in particular, MIN and MAX rules which allows o study worst cases, very important aspect in real-time systems). The different graphs which are obtained with this rules have been situated with respect to the behavioural reference which is the state class graph (considering only time intervals). The analysis power improvement concerns the definition of the Quantified Abstract Quotient Automaton concept (based on the Milner equivalence relation and Beizer rules) : it provides abstract models which are both qualitative and quantitative; il allows to control the size of the models to consider when modelling multilayer communication architectures. This model has been applied to the study of the communication protocol ARINC 629 CP (for plane systems). This study has demonstrated the real-time and fault tolerance properties of the protocol.Cette thèse s'inscrit dans le cadre général de l'utilisation des techniques formelles lors de la phase conceptuelle des systèmes distribués temps-réel, et concerne plus précisément l'extension des pouvoirs d'expression et d'analyse du modèle Réseaux de Petri Temporisés Stochastiques. Ce modèle, qui appartient à la classe des Réseaux de Petri Stochastiques, associe à chaque transition un intervalle de temps, et une distribution de probabilité sur cet intervalle (ceci permet de représenter des caractéristiques temporelles variées et en particulier des contraintes) En ce qui concerne le pouvoir d'expression, nous avons introduit, d'une part, la notion de mémoire temporelle de toutes les sensibilisations (ceci est important pour l'étude des phénomènes de préemption que l'on rencontre dans des algorithmes d'ordonnancement et dans des problèmes de sûreté de fonctionnement) et, d'autre part, plusieurs règles de tir de transitions (en particulier les règles MIN et MAX qui permettent des études des cas pires, aspect important dans les systèmes temps-réels). Les graphes ainsi obtenus ont été également situés par rapport à la référence comportementale que constitue le graphe des classes d'états (obtenu à partir des Réseaux de Petri Temporels). En ce qui concerne le pouvoir d'analyse, nous avons défini le concept d'automate quotient quantifié (concept basé, à la fois, sur la relation d'équivalence de Milner et les règles de réduction de Beizer), qui a deux qualités importantes : il permet, d'une part, d'obtenir des modèles, à la fois qualitatifs et quantitatifs de services de communication ; et, d'autre part, de contrôler les dimensions des modèles à traiter lors de la modélisation d'architectures de communication multicouches. Ce modèle a été appliqué à un exemple industriel, le protocole embarqué temps-réel ARINC 629 CP. L'étude faite a mis en évidence les propriétés temps-réel et de tolérance aux pannes de ce protocole