Abstract FR:

Cette these s'inscrit dans le cadre general de l'utilisation des techniques formelles lors de la phase conceptuelle des systemes distribues temps-reel, et concerne plus precisement l'extension des pouvoirs d'expression et d'analyse du modele reseaux de petri temporises stochastiques. Ce modele, qui appartient a la classe des reseaux de petri stochastiques, associe a chaque transition un intervalle de temps, et une distribution de probabilite sur cet intervalle (ceci permet de representer des caracteristiques temporelles variees et en particulier des contraintes) en ce qui concerne le pouvoir d'expression, nous avons introduit, d'une part, la notion de memoire temporelle de toutes les sensibilisations (ceci est important pour l'etude des phenomenes de preemption que l'on rencontre dans des algorithmes d'ordonnancement et dans des problemes de surete de fonctionnement) et d'autre part, plusieurs regles de tir de transitions (en particulier les regles min et max qui permettent des etudes des cas pires, aspect important dans les systemes temps-reels). Les graphes ainsi obtenus ont ete egalement situes par rapport a la reference comportementale que constitue le graphe des classes d'etats (obtenu a partir des reseaux de petri temporels). En ce qui concerne le pouvoir d'analyse, nous avons defini le concept d'automate quotient quantifie (concept base, a la fois, sur la relation d'equivalence de milner et les regles de reduction de beizer), qui a deux qualites importantes : il permet, d'une part, d'obtenir des modeles, a la fois qualitatifs et quantitatifs de services de communication ; et, d'autre part, de controler les dimensions des modeles a traiter lors de la modelisation d'architectures de communication multicouches. Ce modele a ete applique a un exemple industriel, le protocole embarque temps-reel arinc 629 cp. L'etude faite a mis en evidence les proprietes temps-reel et de tolerance aux pannes de ce protocole.