Ce mémoire de thèse propose une approche pour l'obtention des bornes des performances temporelles d'une Architecture d'Automatisation en Réseau par preuves itératives de propriétés d'atteignabilité sur un modèle formel de l'architecture. Ces propriétés d'atteignabilité sont définies grâce à un automate observateur temporisé et paramétré, dont les gardes de certaines transitions sont fonction d'un paramètre temporel. A chaque itération, les résultats de preuves permettent de déterminer la valeur de ce paramètre pour la prochaine itération ; un algorithme de recherche par dichotomie assure la convergence des itérations. La mise en œuvre de cette approche sur des architectures de taille non triviale a nécessité le développement d'une méthode d'abstraction qui comporte deux étapes : simplification de la structure et modification des modèles formels des composants figurant dans la structure simplifiée, ceci afin de prendre en compte les phénomènes de concurrence entre requêtes émises par différents composants. Ces contributions formelles et méthodologiques ont été validées expérimentalement par le traitement de plusieurs cas de taille et complexité croissantes, basés sur le protocole Modbus TCP/IP.

Nous évaluons dans cette thèse deux performances temporelles des architectures d automatisation distribuées sur Ethernet commuté et utilisant un modèle de coopération client/serveur : Le temps de réponse entre une occurrence d un événement d entrée et l occurrence de l événement de sortie correspondant ; Le temps de cycle réeseau pour la scrutation par un contrôleur de l ensemble de ses modules d entrées / sorties déportées. La conjonction de trois mécanismes de consommation de temps rend ces deux performances variables et difficiles à déterminer de manière analytique. Par conséquent, la méthode proposée se base sur la simulation d un modèle en réseau de Petri temporisé et coloré du comportement dynamique de l architecture complète. Les résultats obtenus sur six architectures test permettent de : Montrer que les architectures multi-contrôleurs utilisant le modèle de coopération client / serveur donnent des temps de cycle réseau plus rapide que celles basées sur les modèles maître / esclave et producteur / consommateur ; Quantifier l influence du réseau et des mécanismes de consommation du temps.