L'être humain fait des erreurs, en particulier dans la réalisation de taches complexes comme la construction des systèmes informatiques modernes. Nous nous intéresserons dans cette thèse à la vérification assistée par ordinateur du bon fonctionnement des systèmes informatiques. Les systèmes informatiques actuels sont de grande complexité. Afin de garantir leur fiabilité, la vérification automatique est une alternative au 'testing' et à la simulation. Elle propose d'utiliser des ordinateurs pour explorer exhaustivement l'ensemble des états du système, ce qui est problématique: même des systèmes assez simples peuvent atteindre un grand nombre d'états. L'utilisation des bonnes représentations des espaces d'états est essentielle pour surmonter la complexité des problèmes posés en vérification automatique. La vérification des systèmes concurrents amène des difficultés additionnelles, car l'analyse doit, en principe, examiner tous les ordres possibles d'exécution des actions concurrentes. Le dépliage des réseaux de Petri est une technique largement étudiée pour la vérification des systèmes concurrents. Il représentent l'espace d'états du système par un ordre partiel, ce qui se révèle aussi naturel qu'efficace pour la vérification automatique. Nous nous intéressons à la vérification des systèmes concurrents modélisés par des réseaux de Petri, en étudiant deux techniques remarquables de vérification: le 'model checking' et le diagnostic. Nous étudions les dépliages des réseaux de Petri étendus avec des arcs de lecture. Ces dépliages, aussi appelés dépliages contextuels, semblent être une meilleure représentation des systèmes contenant des actions concurrentes qui lisent des ressources partagées : ils peuvent être exponentiellement plus compacts dans ces cas. Ce travail contient des contributions théoriques et pratiques. Dans un premier temps, nous étudions la construction des dépliages contextuels, en proposant des algorithmes et des structures de données pour leur construction efficace. Nous combinons les dépliages contextuels avec les 'merged process', une autre représentation des systèmes concurrents qui contourne l'explosion d'états dérivée du non-déterminisme. Cette nouvelle structure, appelée 'contextual merged process', est souvent exponentiellement plus compacte, ce que nous montrons expérimentalement. Ensuite, nous nous intéressons à la vérification à l'aide des dépliages contextuels. Nous traduisons vers SAT le problème d'atteignabilité des dépliages contextuels, en abordant les problèmes issus des cycles de conflit asymétrique. Nous introduisons également une méthode de diagnostic avec des hypothèses d'équité, cette fois pour des dépliages ordinaires. Enfin, nous implémentons ces algorithmes dans le but de produire un outil de vérification compétitif et robuste. L'évaluation de nos méthodes sur un ensemble d'exemples standards, et leur comparaison avec des techniques issues des dépliages ordinaires, montrent que la vérification avec des dépliages contextuels est plus efficace que les techniques existantes dans de nombreux cas. Ceci suggère que les dépliages contextuels, et les structures d'évènements asymétriques en général, méritent une place légitime dans la recherche en concurrence, également du point de vu de leur efficacité. / Humans make mistakes, especially when faced to complex tasks, such as the construction of modern hardware or software. This thesis focuses on machine-assisted techniques to guarantee that computers behave correctly. Modern computer systems are large and complex. Automated formal verification stands as an alternative to testing or simulation to ensuring their reliability. It essentially proposes to employ computers to exhaustively check the system behavior. Unfortunately, automated verification suffers from the state-space explosion problem: even relatively small systems can reach a huge number of states. Using the right representation for the system behavior seems to be a key step to tackle the inherent complexity of the problems that automated verification solves. The verification of concurrent systems poses additional issues, as their analysis requires to evaluate, conceptually, all possible execution orders of their concurrent actions. Petri net unfoldings are a well-established verification technique for concurrent systems. They represent behavior by partial orders, which not only is natural but also efficient for automatic verification. This dissertation focuses on the verification of concurrent systems, employing Petri nets to formalize them, and studies two prominent verification techniques: model checking and fault diagnosis. We investigate the unfoldings of Petri nets extended with read arcs. The unfoldings of these so-called contextual nets seem to be a better representation for systems exhibiting concurrent read access to shared resources: they can be exponentially smaller than conventional unfoldings on these cases. Theoretical and practical contributions are made. We first study the construction of contextual unfoldings, introducing algorithms and data structures that enable their efficient computation. We integrate contextual unfoldings with merged processes, another representation of concurrent behavior that alleviates the explosion caused by non-determinism. The resulting structure, called contextual merged processes, is often orders of magnitude smaller than unfoldings, as we experimentally demonstrate. Next, we develop verification techniques based on unfoldings. We define SAT encodings for the reachability problem in contextual unfoldings, thus solving the problem of detecting cycles of asymmetric conflict. Also, an unfolding-based decision procedure for fault diagnosis under fairness constraints is presented, in this case only for conventional unfoldings. Finally, we implement our verification algorithms, aiming at producing a competitive model checker intended to handle realistic benchmarks. We subsequently evaluate our methods over a standard set of benchmarks and compare them with existing unfolding-based techniques. The experiments demonstrate that reachability checking based on contextual unfoldings outperforms existing techniques on a wide number of cases. This suggests that contextual unfoldings, and asymmetric event structures in general, have a rightful place in research on concurrency, also from an efficiency point of view.

Le développement rapide des systèmes embarqués et les exigences croissantes auxquelles ils sont soumis créent un besoin de techniques innovantes en terme de conception, de vérification et de validation. Les méthodes formelles fournissent des approches intéressantes à la conception de ces systèmes, notamment pour des études de sûreté de fonctionnement (SdF). Le formalisme choisi est basé sur les Réseaux de Petri Colorés (RdPC). L'avantage de ces modèles, en plus d'être très expressifs et formels, est qu'ils permettent d'exprimer le double caractère des systèmes étudiés : statique et dynamique. Le défi relevé par cette thèse est d'utiliser des modèles établis, décrivant l'architecture et/ou le comportement de systèmes, pour en extraire des informations de SdF en général et de diagnostic de défaillances en particulier. L'approche proposée est une analyse structurelle par accessibilité arrière de RdPC. Elle peut être décomposée en deux parties. La première consiste en la proposition d'un outil pour réaliser cette analyse : le RdPC inverse. Il est obtenu grâce à l'application de transformations structurelles sur le RdPC original. La seconde partie est la mise en \oe uvre de l'analyse. Cette partie requiert des mécanismes complémentaires dont le plus important est l'enrichissement du marquage. L'approche proposée est étudiée de deux points de vue complémentaires : algorithmique et théorique. Le point de vue algorithmique consiste à proposer des modèles de transformations pour l'inversion des RdPC et la mise en \oe uvre de l'analyse. L'aspect théorique vise à offrir une base formelle à l'approche en appliquant deux méthodes (l'algèbre linéaire et la logique linéaire) pour prouver notre approche.

La première partie de ce travail est consacrée à l'introduction d'un nouvel outil de modélisation - les Réseaux de Petri à Intervalles - pour répondre à un besoin de spécification, validation et évaluation des systèmes de production intégrant des contraintes d'intervalles de validité sur une qualité donnée. Le premier chapitre situe la contribution applicative par rapport à l'état de l'art en la restreignant à la régulation sur la commande locale pour les ateliers en fonctionnements répétitifs. Ensuite, L'extension de certaines propriétés structurelles des réseaux de Petri P-temporels à des problématiques non temporelles est alors étudiée avec ce nouvel outil.<br /> La deuxième partie de ce travail développe une validation applicative sur une manufacture de tabac. Une construction systématique du modèle Réseaux de Petri à Intervalles est proposée. La méthodologie s'appuie sur les statistiques de production de l'atelier. En s'appuyant sur ce modèle, un réglage est analytiquement calculé en prenant en compte les spécifications de robustesse. Ensuite, une commande réactive est proposée pour faire face aux dérives lentes du procédé. Enfin, l'efficacité de la conduite est démontrée en la simulant sur un ensemble de données de production différent de celui qui a été utilisé pour la construction du modèle.<br />Le présent travail a donc introduit un outil de modélisation dont la pertinence est avérée, au moins sur ce type d'application. Reste que l'abstraction fonctionnelle de l'outil ouvre des champs applicatifs qui restent à explorer, tant d'un point de vue analyse que d'un point de vue mise en œuvre.

Le travail présenté dans cette thèse constitue une contribution à la modélisation et à l'analyse de performances des systèmes logistiques à l'aide d'un nouveau modèle de réseaux de Petri stochastiques. Il s'agit d'une problématique au centre des préoccupations actuelles des entreprises industrielles mais très peu abordée par la communauté des réseaux de Petri. Dans ce travail, nous développons un nouveau modèle de réseaux de Petri dits réseaux de Petri lots déterministes et stochastiques (BDSPNs) capable de supporter les caractéristiques essentielles des systèmes logistiques et plus généralement des systèmes à événements discrets. Ils sont particulièrement adaptés pour la modélisation de flux évoluant en quantités discrètes (lots de différentes tailles et variables) et ils permettent de prendre en compte des activités plus spécifiques telles que les commandes des clients, l'approvisionnement des stocks, la production et la livraison en mode lot. Les BDSPNs permettent par leur formalisme graphique et mathématique de capturer pertinemment et simplement cet aspect lot omniprésent dans différentes locations de ces systèmes et qui s'implique très considérablement dans leur comportement et par conséquent dans leur analyse. Nos travaux portent à la fois sur la théorie du nouveau modèle, sur ses techniques d'analyse et sur ses applications aux systèmes logistiques. Ainsi, les résultats obtenus et les applications effectuées font des BDSPNs un outil de modélisation performant aussi bien pour l'analyse que pour la simulation.

Ce mémoire de thèse prèsente une approche pour la surveillance des systèmes à événements discrets commandés. L'étude se restreint aux défauts interruptibles : intermittents et permanents. Le comportement acceptable de ces systèmes est introduit afin d'accroître la disponibilité des systèmes commandés. Ce comportement présente une tolérance aux défauts intermittents. Une démarche de construction du système de surveillance est présentée. Nous modélisons, dans un premier temps, le comportement du système sujet aux défauts interruptibles par un automateà chronomètres. Nous appliquons, dans un deuxième temps, une procédure de synthèse à cet automate. Cette procédure est basée aux opérateurs d'analyse en avant et en arriérer de l'automate. Un nouveau modèle appelé réseaux de Petri à chronomètres post- et Pré-initialisés est également présenté. Ce modèle général du RdP a été utilisé, dans le cadre de ce mémoire, pour modéliser le comportement des systèmes sujets aux défauts interruptibles. L'implémentation de notre méthode de surveillance se fait par un automate programmable industriel. Pour ce faire, le système de surveillance étant sous la forme d'un automate àchronomètres est traduit structurellement en programme SFC.

Le corps de ce travail concerne la modélisation des systèmes à événements discrets. Il s'intéresse par ailleurs en quasi exclusivité à la gestion des contraintes de temps de séjour. Mes travaux de thèse ont comporté la constitution du cahier des charges en amont et les applications en aval d'un outil de modélisation des exigences temporelles : Les Réseaux de Petri P-temporels. L'ensemble de mes travaux de recherche a été développé dans le but d'asseoir l'utilisation de cet outil. Un premier axe a été de positionner l'outil par rapport à ceux de l'état de l'art. Une deuxième tâche a été de prouver un certains nombre de propriétés mathématiques dans l'optique de permettre des applications industrielles efficaces. Au delà de la stricte recherche de propriété, l'extension du champ applicatif, vers le domaine du ferroviaire par exemple, a pris une part très importante. Une troisième activité a débouché sur la caractérisation des limites du modèle et la proposition d'extension fonctionnelle ou de rapprochement de l'outil de modélisation vers des modèles existants. Ce modèle concerne donc les Systèmes à Evénements Discrets où l'on rencontre des contraintes de temps de séjour maximum dans un état donné. C'est le cas de la galvanoplastie qui a été le premier support applicatif. Très rapidement, le champ des applications potentielles de l'outil a été élargi par des publications dans les domaines de l'industrie alimentaire. Les travaux se sont par ailleurs concentrés sur la partie commande, en supposant que la séquence des opérations avait déjà été fixée. Ils ont été appuyés par le travail de master de recherche de M.F. Karoui en 2004 (deux conférences ont été publiées dans la suite de son mémoire). Par ailleurs, l'expertise en supervision qui se trouvait au sein de l'équipe Système à Evénement Discret a été valorisée par le stage de master de T. Lecuru sur la supervision des ateliers automobiles en 2003. Ce travail a pris une autre ampleur avec la thèse de Jerbi Nabil sur la commande des ateliers à contraintes de temps soutenue en 2006 (3 publications de revue). Il se poursuit avec la thèse de Annis Mhalla. En 2006, F. Defossez soutient un master dans le domaine ferroviaire sur la gestion des exigences temporelles de sécurité. Ce dernier va s'inscrire en troisième année de thèse et a déjà publié 5 conférences. Ce travail ouvre un champ très important pour l'outil de modélisation que je porte. Par exmple, cela a amné la participation à un projet Européen. Ce projet SELCAT qui s'intéresse au passage à niveau et qui s'est terminé en juin 2008. Il se prolongera dans un projet national ANR accepté qui débutera autour de janvier 2009. En parallèle, un projet spécifique ayant trait aux outils de modélisation sur les chantiers est en cours avec la SNCF. Enfin, la thèse de Hedi Dhouibi a été l'occasion de proposer un nouveau modèle capable de généraliser certaines propriétés des Réseaux de Pétri P-temporels à des systèmes où le paramètre critique est différent du temps. Une validation industrielle sur des données réelles a pu être effectuée (soutenance en 2005). Elle fait l'objet de trois publications de revues internationales (acceptation en 2008).

L'objectif de cette thèse est la modélisation et la commande du trafic. Je considère des modèles microscopiques du trafic pour dériver des relations entre des variables macroscopiques du trafic. Plus précisément, il s'agit de dériver le diagramme fondamental du trafic 2D, qui donne la relation entre la densité et le flot des véhicules. Ce diagramme est utilisé, par exemple, pour déterminer la densité des véhicules qui maximise le flot. Cette information peut aussi être utilisée pour la commande du trafic 2D. Les modèles mathématiques sont basés sur la commande optimale déterministe ou stochastique.<br /><br />La première partie de la thèse est sur le trafic 1D. Il s'agit de généraliser un modèle déterministe de trafic basé sur l'algèbre minplus, qui donne le diagramme fondamental du trafic sur une route. La généralisation permet de réaliser une large classe de diagrammes fondamentaux.<br /><br />Dans la deuxième partie, j'étudie les systèmes dynamiques additivement homogènes de degré 1. En effet, tous les systèmes dynamiques donnés dans ce travail sont additivement homogènes de degré 1. Je m'intéresse dans cette partie à l'existence et à l'unicité de taux de croissance et de valeurs propres additives associées à ces systèmes. Je parts du cas général où zéro, un ou plus de taux de croissance et de valeurs propres peuvent exister, et où des comportement chaotiques peuvent apparaître. Je rappelle les résultats existants dans le cas où on suppose que le systèmes dynamique est, en plus, monotone, et dans le cas ou il est aussi convexe. A la fin de cette partie, je caractérise une classe de systèmes dynamiques additivement homogène de degré 1, non nécessairement monotone, mais dont le comportement asymptotique peut être décrit.<br /><br />La troisième partie consiste à généraliser un modèle de trafic 1D basé sur les réseaux de Petri et l'algèbre minplus, dans le but de modéliser des intersections, et puis dériver le diagramme fondamental du trafic 2D. Une intersection peut être gérée de plusieurs façons, et peut être considérée avec ou sans possibilité de tourner (pour les véhicules). Plusieurs modèles tenant en compte ses hypothèses sont donnés dans cette partie.<br /><br />Le modèle le plus exploré ici est celui de deux routes circulaires avec une intersection gérée par la priorité à droite, et avec possibilité de tourner. Dans ce cas, et sous certaines conditions, le problème de valeur propre additive associé au système dynamique peut être résolu. Le taux de croissance du système dynamique, qui correspond au flot moyen des véhicules est obtenu numériquement. En comparant la valeur propre obtenue théoriquement et le flot moyen donné numériquement, j'ai conclus que les deux quantités, qui sont données en fonction de la densité des véhicules, sont très proches, et sont égales en plusieurs valeurs de la densité. Ainsi, la valeur propre représente une bonne approximation du diagramme fondamental du trafic 2D.<br /><br />D'autres approches de gestion d'intersections consiste à les commander moyennant des feux de signalisation. Une évaluation de la commande de l'intersection peut se baser sur le diagramme fondamental obtenue pour chacune des approches considérées. Une comparaison des différentes approches est donnée. <br /><br />Dans la quatrième partie j'ai développé un code en Scilab qui facilite la construction informatique de grands réseaux de trafic routier. Il s'agit de définir des systèmes élémentaires et des opérateurs sur l'ensemble de ces systèmes, et puis de combiner des systèmes basique pour construire de grands systèmes.<br /><br />La dernière partie est sur la commande du trafic à deux modes: trafic des véhicules particulier, et trafic des véhicules de transport en commun. L'idée est de déterminer un plan de feux de signalisation qui favorise le trafic des véhicules de transport en commun.

Le système CESAR proposé dans cette thèse est un système d'aide à la conception des applications reparties. Il permet de décrire l'application étudiée dans un langage algorithmique en termes de processus communiquant par rendez-vous; de spécifier les propriétés de comportement souhaitées au moyen d'une logique temporelle. Le modèle sur lequel ces formules sont analysées est un réseau de Petri interprété généré automatiquement à partir de la description fournie. L'analyse repose sur une évaluation des opérateurs temporels comme points fixes de transformateurs de prédicats sur l'espace d'états du modèle.

L'un des problèmes majeurs rencontrés par la robotique est celui du développement d'architectures logicielles de contrôle des robots. Ceci s'explique par la complexité sans cesse croissante de ces architectures, qui doivent intégrer toujours plus de fonctionnalités de divers niveaux d'abstraction (de planification, d'asservissement, de perception, de gestion des modes de fonctionnement, etc.) et qui nécessitent la prise en compte du caractère temps-réel du contrôle. Par ailleurs, les fonctionnalités s'appuyant, directement ou non, sur un ensemble d'éléments matériels embarqués sur le robot, une architecture doit pouvoir être adaptée en fonction de l'évolution technologique (nouveaux capteurs et actionneurs, remplacement d'éléments de la partie opérative, etc.). L'enjeu actuel est donc de définir et intégrer des fonctionnalités sous forme de briques logicielles réutilisables au sein d'architectures de contrôle évolutives, de manière à simplifier le développement. Après avoir fait un tour d'horizon des propositions actuelles, le manuel présente CoSARC, une méthodologie originale couvrant l'intégralité du processus de développement d'un contrôleur de robot. La méthodologie est basée sur un modèle d'architecture et sur un langage à composants. Inspré des propositions historiques d'architectures hybrides, le modèle d'architecture constitue la base du processus de développement. Il définit une organisation générique intégrant une vision hiérarchique du contrôle et il s'appuie sur des concepts abstraits indépendants de tout domaine d'application, tel que celui de ressource . La construction d'une architecture est réalisée en fonction du modèle et à l'aide des éléments d'un langage à composants. Ces éléments correspondent à différentes catégories de composants : composants de représentation dédiés à la description des connaissances sur le monde du robot, composants de contrôle dédiés à la description des activités du robot, composants connecteurs dédiés à la description des protocoles régissant les interactions entre composants de contrôle, composants de configuration dédiés à la description d'une architecture et de son déploiement. Un des aspects essentiels de certains de ces composants réside dans le fait que leur comportement est exprimé sous la forme d'un réseau de Petri à Objets. L'expressivité et la pertinence de la méthodologie sont démontrés sur un exemple traitant du développement d'un robot manipulateur mobile.

Si certains conservent un objectif scientifique et expérimental, la plupart des projets spatiaux visent maintenant à développer des systèmes profitables soumis à de fortes contraintes opérationnelles. Dimensionner ces systèmes, "ni trop, ni trop peu", est donc un objectif majeur qui conditionne leur viabilité économique. Si trop de risques sont pris les investisseurs se feront rares, et si le système est surdimensionné son coût peut être également rapidement dissuasif. Dans ce contexte, l'étude de la Disponibilité Opérationnelle en phases d'avant-projet donne certains critères précieux pour évaluer le compromis coût / prise de risque et permet ainsi de guider très tôt certains choix de conception. Cependant la complexité et la taille croissante de ces systèmes ont rapidement mis en évidence certaines limites des méthodes classiques d'évaluation de cette grandeur. La théorie des réseaux de Petri, riche d'une trentaine d'années de recherche et principalement appliquée à l'analyse, l'évaluation et la commande des systèmes distribués, offre des perspectives intéressantes pour dépasser ces limites. La principale contribution de ce travail mené au sein de l'Agence française de l'Espace et d'un industriel du spatial a été de favoriser son utilisation pour l'étude de la Disponibilité Opérationnelle de système spatiaux complexes et dans le cadre très concret des phases d'avant-projets. On a tout d'abord justifié l'intérêt que les réseaux de Petri présentent tant pour la modélisation que pour l'évaluation de tels systèmes par comparaison aux approches classiques. Puis on a illustré leur utilisation sur des programmes bien réels et dans le cadre d'un travail intégré avec les équipes projets. Enfin, on a proposé les bases d'une démarche de modélisation orientée application dont le but est d'aider des non spécialistes à concevoir aisément des modèles de systèmes complexes. Ce sont ces trois grandes étapes qui sont ici présentées.