Cette thèse a pour objectif de concevoir un nouveau paradigme de navigation Web, permettant à un ensemble d'utilisateurs de naviguer de manière coopérative sur le Web. Ces utilisateurs, selon des règles de synchronisation simples mises à jour de manière dynamique, peuvent synchroniser l'affichage de pages Web dans leur navigateur. Nous avons modélisé les différentes primitives de synchronisation proposées au moyen d'automates étendus et avons formalisé le modèle global de synchronisation par des réseaux de Petri. Une vérification formelle de ce modèle, grâce aux outils TINA et ALDEBARAN, a montré que les primitives de synchronisation rendaient effectivement le service attendu. Partant d'une description informelle et intuitive de l'architecture du système de navigation coopérative, nous avons proposé une méthode pour la formaliser au moyen du profil UML/SDL supporté par l'outil TAU G2 de Telelogic. Nous avons détaillé l'architecture au moyen de différents diagrammes UML de ce profil et l'avons validé en comparant les traces de simulation obtenues avec les scénarios (diagrammes de séquences) élaborés au début de la phase de conception de notre système. Nous avons développé une implémentation du système de navigation coopérative en Java, appelée CoLab, qui est à ce jour opérationnelle et qui supporte les principales primitives de synchronisation. Cette implémentation s'appuie sur la présence d'un serveur Proxy centralisé qui synchronise les utilisateurs selon les relations de synchronisation établies entre eux. Elle s'appuie également sur une technique originale de traduction des pages Web qui permet de rendre les actions de navigation détectables par le serveur Proxy. Nous avons réalisé des campagnes de mesure du temps moyen de rapatriement de ressources Web, en fonction du nombre d'utilisateurs enregistrés dans une session et de la taille des ressources, qui ont montré les bonnes performances de la plate-forme jusqu'à plus d'une centaine d'utilisateurs par sessio n. S'appuyant sur ces résultats, nous avons proposé une solution pour répartir CoLab sur plusieurs serveurs Proxy. Finalement, nous avons montré comment rendre disponible le service de navigation coopérative sous la forme d'un service Web.

Cette thèse concerne une nouvelle méthode de réduction des réseaux de Petri. Le problème de la réduction des réseaux a d'abord été considéré comme le moyen de réduire l'espace des états sans modifier un certain nombre de propriétés (telles que "être borne", "être vivant", etc) afin de faciliter leur étude. Nous nous placons ici dans une toute autre optique, puisque nous allons chercher une méthode de réduction non pas en voulant conserver un ensemble de propriétés, mais préservant le comportement du réseau. Dans les premières parties, nous recherchons la relation la plus grande possible qui soit une équivalence sur les places du réseaux nous permettant de les fusionner et telle que le réseau réduit soit bisimilaire au réseau original. Nous montrons que la bisimulation de places vérifie ces contraintes et qu'il existe des algorithmes efficaces (polynomiaux) pour la calculer. Dans la suite, des cas d'extensions classiques des réseaux (arcs inhibiteurs) comme des équivalences (bisimulations "observationnelle") sont abordés. La dernière partie de la thèse s'intéresse à l'équivalence de propriétés entre le réseau initial et le réseau quotient. Ce travail se termine par la présentation succincte du logiciel Petris qui met en oeuvre les différents algorithmes.

Cette thèse a été réalisée dans le cadre du projet " Gestion et Optimisation de la Chaîne Documentaire ", projet labellisé par le Pôle de compétitivité des Industries du Commerce. Le projet a pour but de concevoir et de développer un nouveau workflow et un outil d'aide à la décision. Ce système doit être capable de gérer et d'optimiser le flux complet dématérialisé de contrats reçus à COFIDIS.Nous présentons d'abord le framework retenu dans le cadre du projet pour modéliser et implémenter le workflow. En phase de conception BPMN a été choisi. Pour la partie développement, l'utilisation de BPEL a été préconisée pour implémenter et exécuter l'application finale (services web).Cependant la flexibilité offerte par BPMN peut conduire à des propriétés indésirables du processus telles que blocage et inaccessibilité. De plus, BPMN a été conçu pour fournir des modèles Orientés Process. Les données ou les ressources y sont donc peu représentées. En conséquence, l'analyse de performance sur un modèle BPMN est quasi inexistante.Afin de surmonter ces problèmes nous proposons d'insérer dans le framework deux nouvelles phases. Ces deux phases sont appliquées au modèle BPMN. La première est une phase de vérification et de validation et la deuxième une phase d'optimisation. Ces deux phases sont réalisées en transformant le modèle BPMN vers un langage formel. Notre choix dans ce travail a été d'utiliser les réseaux de Petri. Ce qui nous a permis de vérifier et de valider de bonnes propriétés du process. Quant à l'optimisation, nous avons défini une nouvelle variante du problème d'affectation (bin packing problem) et proposé une résolution à intégrer dans le processus d'aide à la décision

La surveillance d'entrepôts de produits chimiques est une opération délicate dans le sens où elle passe par une connaissance de la nature de chaque produit stocké, sur leur localisation, sur leur possible interaction et sur les actions à mettre en œuvre en cas d'alerte. Pour faciliter cette gestion de stockage, cette thèse propose d'utiliser le concept de l'ambiant où le produit possède son propre système d'information et de communication sans fil de façon à le rendre intelligent et autonome. Cette thèse propose et développe un modèle de comportement interne de produit actif permettant une approche distribuée de sécurité active. Celui-ci permet d'aboutir à un protocole de communication de niveau applicatif à embarquer dans les produits actifs. Ce protocole est évalué de façon formelle en utilisant les Réseaux de Petri colorés hiérarchiques. Finalement, ce protocole est implémenté dans le simulateur Castalia/Omnet++ pour l'analyser dans plusieurs scénarii et aussi pour l'éprouver lors du passage à l'échelle. Les résultats montrent l'intérêt et la faisabilité du concept de produit actif.

La surveillance d'entrepôts de produits chimiques est une opération délicate dans le sens où elle passe par une connaissance de la nature de chaque produit stocké, sur leur localisation, sur leur possible interaction et sur les actions à mettre en œuvre en cas d'alerte. Pour faciliter cette gestion de stockage, cette thèse propose d'utiliser le concept de l'ambiant où le produit possède son propre système d'information et de communication sans fil de façon à le rendre intelligent et autonome. Cette thèse propose et développe un modèle de comportement interne de produit actif permettant une approche distribuée de sécurité active. Celui-ci permet d'aboutir à un protocole de communication de niveau applicatif à embarquer dans les produits actifs. Ce protocole est évalué de façon formelle en utilisant les Réseaux de Petri colorés hiérarchiques. Finalement, ce protocole est implémenté dans le simulateur Castalia/Omnet++ pour l'analyser dans plusieurs scénarii et aussi pour l'éprouver lors du passage à l'échelle. Les résultats montrent l'intérêt et la faisabilité du concept de produit actif.

L'accession à l'éducation d'un nombre toujours plus grand d'individus a conduit à considérer la performance des systèmes de formation comme un véritable facteur de développement économique. C'est dans ce contexte que s'inscrivent nos travaux de thèse qui ont visé au développement de méthodes et outils pour l'aide à la conception de la partie opérationnelle d'un système de formation et notamment tout le système de transformation permettant l'accroissements de compétences chez les apprenants.<br />Après avoir présenté un bilan des systèmes de formation en définissant leur périmètre puis leur fonctionnement et résultats, nous précisons alors les facteurs qui nous ont conduits à nous préoccuper des processus opérationnels des systèmes de formation.<br />Dans un deuxième chapitre, nous précisons la démarche que nous avons choisi d'adopter et déclinons ainsi l'ensemble de notre méthode, associée à des outils spécifiques, qui vise à l'aide à la conception et la mise en œuvre des formations. Nous nous éloignons de la logique de l'offre pour migrer vers une logique de la demande. Nous proposons une identification contraintes subies par un système de formation (ressources à capacité finie, cohérence pédagogique, indisponibilité de ressources, compétences et aptitudes des ressources, etc.)<br />Dans une troisième partie, nous illustrons notre propos en appliquant les méthodes et outils développés à un cas pratique.<br />Enfin, nous concluons sur l'apport scientifique constitué par ces travaux et ouvrons la voie vers de nombreuses perspectives, le domaine de l'ingénierie de la formation étant encore à ses balbutiements.

Cette thèse porte sur l'étude des systèmes complexes tels que les systèmes mécatroniques, en tenant compte de leur aspect dynamique, hybride, reconfigurable et multitechnologies. Le premier chapitre est consacré au contexte actuel des systèmes mécatroniques et la nécessité qu'ils soient conçus et développés de manière collaborative afin d'obtenir des systèmes sûrs de fonctionnement. La démarche systémique aide à l'étude de ces systèmes complexes. Le second chapitre expose les différentes méthodes utilisées dans l'analyse qualitative ainsi que dans l'analyse quantitative. Le choix se porte alors sur les méthodes SADT et SA-RT pour l'analyse fonctionnelle, l'AMDE et l'AEEL pour l'analyse dysfonctionnelle et sur les réseaux de Petri pour l'analyse quantitative. Le dernier chapitre expose la méthodologie proposée pour l'estimation de la fiabilité des systèmes mécatroniques ainsi que l'application de cette méthodologie sur un système ABS. Finalement, les conclusions et les perspectives de l'approche proposée sont émises.

<p>Les travaux présentés portent sur l'étude de méthodes de vérification paramétrée des systèmes temps réels. La motivation pour ces recherches est de proposer des méthodes formelles à appliquer sur des systèmes dont les spécifications ne sont pas encore complètes. Des paramètres sont donc introduits dans les modèles utilisés afin de donner des degrés de liberté à la modélisation. Le but est alors de guider la conception du système en déterminant des valeurs satisfaisantes pour les paramètres.</p> <p>Nous nous sommes focalisé sur les paramètres temporels qui sont en général parmi les plus complexes à définir. Nous avons ainsi défini le modèle des réseaux de Petri à chronomètres paramétrés.</p> <p>Dans une première approche, nous étendons les méthodes d'analyse classiquement utilisées dans les réseaux de Petri temporels. L'espace d'états du modèle paramétré est ainsi représenté par le graphe des classes d'états paramétrées. Cela nous permet de proposer des semi-algorithmes de model-checking paramétré avec lesquels nous vérifions des formules de logique TCTL paramétrées.</p> <p>Dans une seconde approche, nous étudions les méthodes qui préservent le parallélisme des réseaux de Petri. L'intérêt est de limiter l'explosion combinatoire qui apparaît lors de l'analyse de systèmes distribués, en particulier avec des modèles paramétrés. Nous proposons pour cela une méthode de dépliage temporel paramétré. Ce dépliage est a priori infini, mais nous proposons de l'utiliser pour résoudre un problème de supervision. La construction du dépliage est alors guidée par des observations finies, et nous extrayons les explications de ces observations, ainsi que les contraintes sur les paramètres qu'elles induisent.</p>

Dans ce travail, nous proposons une méthode systématique et facile de mise en œuvre pour la synthèse du contrôle des systèmes à événements discrets. Nous modélisons les systèmes par des modèles RdP saufs. Deux idées distinctes sont utilisées : 1) ajout de places de contrôle pour empêcher l'atteignabilité des états interdits, et 2) ajout de conditions pour les transitions contrôlables. Nous avons alors été confrontés au problème des transitions incontrôlables pour garantir l'optimalité et à la complexité apportée par le nombre des places de contrôles qui peut être très grand. <br />Dans la première idée, nous avons utilisé le théorème introduit par Guia, qui permet de passer d'un ensemble d'états interdits vers un ensemble de contraintes linéaires. Nous avons proposé des méthodes originales de simplification des contraintes. Il est alors possible de réduire le nombre et la borne des contraintes et ainsi de construire un modèle contrôlé simple. Les méthodes de simplification présentées sont applicables sur les RdP saufs. Nous avons déterminé les conditions nécessaires et suffisantes pour avoir un contrôleur maximal permissif. L'avantage principal de ces méthodes de synthèse de contrôleurs est que le modèle RdP contrôlé est très proche du modèle initial. <br />La deuxième idée qui a été utilisée pour la synthèse est l'utilisation des conditions pour le franchissement des transitions contrôlables. Les méthodes qui utilisent cette technique, ont en général besoin d'un calcul long en temps réel. En appliquant notre méthode de simplification, nous arrivons à un contrôleur simple.

Ce travail s'inscrit dans le domaine du diagnostic des systèmes hybrides et est basé sur l'utilisation d'un modèle. Il a pour objectif de diagnostiquer les fautes à partir de la connaissance structurelle, comportementale ou fonctionnelle du système en représentant ces connaissances (modèle du système) séparément de la connaissance sur la tâche de diagnostic. Les systèmes hybrides incluent à la fois des variables continues et discrètes. La dynamique continue est généralement fournie par des équations différentielles et algébriques alors que la partie discrète est modélisée par des automates ou des systèmes à transition. Le formalisme adopté dans ce travail pour modéliser ces systèmes s'appuie sur le modèle " Réseau de Petri Différentiel à Objet " (RdPDO) qui est intégré dans la plate forme de simulation PrODHyS (Process Object Dynamic Hybrid Simulator). Il possède l'avantage de prendre en compte le comportement hybride d'une part, en associant les variables continues aux jetons et d'autre part, en associant un système algébro-différentiel aux places permettant de faire évoluer les variables d'état continues. La méthodologie de diagnostic proposée s'effectue en deux étapes. La première étape consiste à détecter à l'aide d'une classification floue, des fautes qui présentent les mêmes symptômes - à partir d'une connaissance préalable des états de défaillance obtenue par apprentissage - afin de réduire les chemins ou les scénarios à explorer lors de la seconde phase. Cette dernière sert à diagnostiquer la faute parmi celles détectées à l'étape précédente en levant l'ambiguïté. Pour ce faire, deux raisonnements ont été suivis. Le premier, qualifié de raisonnement avant, consiste à former pour chaque faute incriminée, un critère d'écarts entre les mesures effectuées sur le système et celles émanant du modèle avec la faute simulée, sur une fenêtre temporelle et d'isoler ainsi la faute aboutissant au critère le plus faible. Le second raisonnement qualifié de raisonne ment arrière, effectue des calculs similaires mais sur l'évolution temporelle passée du système par une simulation arrière effectuée avec PrODHys, offrant la possibilité supplémentaire par rapport au premier raisonnement de remonter à l'instant de la défaillance. La méthodologie développée est illustrée sur un système hydraulique souvent utilisé comme " benchmark ". Comme nous ne disposons pas d'un système réel, celui-ci est simulé à l'aide d'un modèle de simulation de type RdPDO qui cette fois-ci contient les états de défaillances et des différences (bruits, erreurs de modélisation) par rapport au modèle utilisé pour le diagnostic.