Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal.

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.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérificationdes systèmes temporisés. La première partie concerne une méthode de spécification enutilisant les diagrammes états-transitions pour modéliser un système donné en partant d’unedescription textuelle. Cette méthode guide l’utilisateur pour le développement de la modélisation.Elle comporte plusieurs étapes et utilise des observateurs d’états et des événements afind’engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de laméthode de spécification pour une application semi-automatique est présenté. La seconde partieconcerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, cequi permet d’utiliser les méthodes de vérification. Nous prenons en considération dans cette traductionun ensemble important des éléments syntaxiques des diagrammes états-transitions, telsque la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passageautomatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.La dernière partie concerne l’intégration des contraintes temporelles dans les deuxapproches précédentes. Nous définissons des annotations pour les diagrammes états-transitionsdont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dansla méthode de spécification et la traduction. Le but est de proposer des annotations faciles àcomprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plusutilisées. / In order to specify and verify timed systems, we present in this thesis approaches using UMLstate machines and coloured Petri nets. Our first approach is a specification method that takesinto account a textual description of the system and generates the corresponding state machinediagram. This method helps a non-expert user to model a system in a structural way. We presenta tool that implements the specification method. Our second approach is the translation of UMLstate machine diagrams to coloured Petri nets diagrams. In this approach we take into account animportant set of UML state machine elements that allows the modelling of concurrent systems,etc. A tool that implements the approach and allows us to automate the translation is beingdeveloped. Finally, the last approach is the integration of time constraints in our specificationmethod and in our translation. We propose a set of annotations to model time in state machinediagrams, and we define the corresponding syntax and semantics.

Les performances temporelles d'une architecture de contrôle-commande conditionnent fortement celles du système automatisé de production commandé. Pour maîtriser ces performances temporelles, l'architecte automaticien doit pouvoir les évaluer à chaque phase du cycle de développement : de l'étude d'avant-projet à la conception détaillée ainsi que lors de la mise au point. Il n'a cependant pas les mêmes attentes concernant les performances estimées. Des résultats approximatifs, obtenus rapidement à partir de données encore imprécises, lui suffisent en début de cycle de développement, alors que des prévisions fiables, même si elles sont plus difficiles à obtenir, lui sont nécessaires en conception détaillée. L'approche que nous présentons prend en compte ces différents besoins et contraintes. Elle consiste en une méthode d'évaluation des performances temporelles d'architectures de commande complexes distribuées en réseaux, destinée à accompagner l'architecte tout au long du cycle de développement. Cette méthode est basée sur une modélisation modulaire du comportement temporel de la commande par réseaux de Petri Colorés Temporisés. Pour ce faire, trois temps sont nécessaires dans la modélisation. La modélisation de l'architecture fonctionnelle consiste à représenter les fonctions de commande, et leurs interactions. La modélisation de l'architecture matérielle permet de traduire la topologie et les connexions entre équipements de commandes (automates programmables, réseaux de communication, ...). L'affectation des fonctions de commande aux équipements ainsi que la prise en compte des communications entre ces fonctions via des réseaux de communication constitue le modèle de l'architecture opérationnelle. Une fois le modèle de comportement de l'ensemble de l'architecture opérationnelle constitué, l'évaluation des performances temporelles est réalisée par simulation du réseau de Petri obtenu. Pour valider notre approche, nous traitons un exemple significatif à l'aide de la plate forme logicielle Design CPN. Cette étude de cas nous permet de présenter une série d'études portant sur la convergence de nos modèles, sur la sensibilité des résultats de simulation aux erreurs de paramétrages et sur la précision des performances obtenues par simulation en les confrontant à celles mesurées sur le système réel.

Les travaux exposés dans ce mémoire portent sur la conception de l'architecture de conduite des systèmes automatisés de production. Ils ont été développés au sein du Laboratoire Universitaire de Recherche en Production Automatisée (LURPA - EA 1385). Il s'agit de travaux prospectifs dont l'objectif est de construire un cadre méthodologique formel de conception et d'évaluation d'architectures.<br /><br />La première partie est consacrée à l'exposé du cadre méthodologique retenu et comporte quatre chapitres dans lesquels sont successivement abordés :<br /><br /> * la problématique générale de la conception d'architectures de conduite, ainsi qu'une revue des \travaux scientifiques dans le domaine,<br /> * la présentation générale de la méthode proposée avec le point de vue des activités de conception, d'évaluation et de choix d'architecture,<br /> * la présentation détaillée de la construction d'architecture avec cette fois le point de vue des différents modèles produits,<br /> * la présentation détaillée d'évaluation et de choix de l'architecture retenue avec encore une fois le point de vue des modèles d'évaluation. <br /><br />La seconde partie du mémoire est destinée à préciser et à valider par l'exemple la méthode proposée. Pour ce faire, nous l'avons appliquée à la conception de l'architecture de conduite d'un poste de lance ment d'un transfert libre. Le plan de cette étude suit de manière ordonnée la démarche que nous avons présenté dans la première partie.

Cette thèse traite le problème de la modélisation des patrons de workflow sémantiquement riche et propose un processus pour développer des patrons de workflow. L'objectif est de transformer un processus métier en un patron de workflow métier basé sur les flux de contrôle qui garantit la vérification syntaxique et sémantique. Les défis majeurs sont : (i) de définir un formalisme permettant de représenter les processus métiers; (ii) d'établir des mécanismes de contrôle automatiques pour assurer la conformité des patrons de workflow métier basés sur un modèle formel et un ensemble de contraintes sémantiques; et (iii) d’organiser la base de patrons de workflow métier pour le développement de patrons de workflow. Nous proposons un formalisme qui combine les flux de contrôle (basés sur les Réseaux de Petri Colorés (CPNs)) avec des contraintes sémantiques pour représenter les processus métiers. L'avantage de ce formalisme est qu'il permet de vérifier non seulement la conformité syntaxique basée sur le modèle de CPNs mais aussi la conformité sémantique basée sur les technologies du Web sémantique. Nous commençons par une phase de conception d'une ontologie OWL appelée l’ontologie CPN pour représenter les concepts de patrons de workflow métier basés sur CPN. La phase de conception est suivie par une étude approfondie des propriétés de ces patrons pour les transformer en un ensemble d'axiomes pour l'ontologie. Ainsi, dans ce formalisme, un processus métier est syntaxiquement transformé en une instance de l’ontologie. / This thesis tackles the problem of modelling semantically rich business workflow templates and proposes a process for developing workflow templates. The objective of the thesis is to transform a business process into a control flow-based business workflow template that guarantees syntactic and semantic validity. The main challenges are: (i) to define formalism for representing business processes; (ii) to establish automatic control mechanisms to ensure the correctness of a business workflow template based on a formal model and a set of semantic constraints; and (iii) to organize the knowledge base of workflow templates for a workflow development process. We propose a formalism which combines control flow (based on Coloured Petri Nets (CPNs)) with semantic constraints to represent business processes. The advantage of this formalism is that it allows not only syntactic checks based on the model of CPNs, but also semantic checks based on Semantic Web technologies. We start by designing an OWL ontology called the CPN ontology to represent the concepts of CPN-based business workflow templates. The design phase is followed by a thorough study of the properties of these templates in order to transform them into a set of axioms for the CPN ontology. In this formalism, a business process is syntactically transformed into an instance of the CPN ontology. Therefore, syntactic checking of a business process becomes simply verification by inference, by concepts and by axioms of the CPN ontology on the corresponding instance.

Ce mémoire, réalisé dans le cadre d’une thèse sous convention CIFRE avec la société Schneider-Electric et l’Université de Lorraine à travers le laboratoire du CRAN, porte sur l’évaluation des performances temporelles des architectures de contrôle-commande distribuées sur un réseau de communication. Le besoin industriel s’exprime sous la forme d’un outil d’aide au dimensionnement des architectures en phase d’avant-vente caractérisée par une connaissance partielle de ces dernières. Le problème scientifique sous-jacent est relatif à la génération automatique des modèles servant de support à l’évaluation. En effet, l’évaluation des performances doit être réalisée pour un ensemble important d’architectures, dans un temps court, difficilement compatible avec une construction manuelle des modèles. Notre contribution porte sur la définition formelle, à l’aide de réseaux de Petri colorés et temporisés, d’un modèle « constructeur » d’architectures embarquant des mécanismes de configuration, d’instanciation et de paramétrage. Plusieurs algorithmes sont proposés pour, d’une part, construire automatiquement le modèle d’une architecture donnée, à partir d’une description formelle de sa topologie et d’une librairie de modèles d’équipements de contrôle-commande, et, d’autre part, pour générer les observateurs requis à partir d’une description formelle des performances à évaluer. Ces différents algorithmes ont été implantés dans un outil interfacé, d’une part avec l’outil Schneider de description des architectures, et, d’autre part avec le simulateur de l’outil CPN Tools qui fournit une estimation des performances via des simulations de Monte-Carlo. L’intérêt de cette approche a été illustrée sur la base de quelques architectures types fournies par la société Schneider-Electric / This PhD dissertation, supported by CIFRE convention between the company Schneider-Electric and the University of Lorraine through the CRAN laboratory, deals with the assessment of temporal performances for a networked distributed control system. The industrial need was the development of a quotation and sizing tool of industrial control architecture during pre-sales stage. This stage is characterized by limited information about the process and the customers’ needs. The underlying scientific problematic was the ability to generate automatically models serving as support for the evaluation. In fact, performance assessment is realized for a wide range of architecture during a small amount of time, which is not compliant with a manual definition of the models. Our contribution is mainly based on a formal definition of a “builder” model with Colored and Timed Petri Nets which embeds mechanisms for configuration, instantiation and parameters setting of the architecture models. Several algorithms have been proposed for firstly build automatically the architecture Petri Nets model from a formal description of the topology and from a component model library and, secondly, for generating performance observers. Theses algorithms have been implemented on a tool gathering a user interface developed by Schneider –Electric and the Petri Nets simulator called CPN Tools which provides the performance assessment through Monte-Carlo simulation. The added value of this approach has been illustrated through case studies provided by Schneider-Electric

Notre propos est la conception assistée par ordinateur des scénarios comprenant des contenus multimédia qui interagissent avec les actions extérieures, notamment celles de l’interprète (e.g., spectacles vivants, installations muséales interactives et jeux vidéo). Le contenu multimédia est structuré dans un ordre spatial et temporel selon les exigences de l’auteur. Par conséquent, la complexité potentiellement élevée de ces scénarios nécessite des langages de spécification adéquats pour leur complète description et vérification.Partitions Interactives est un formalisme qui a été proposé comme un modèle pour la composition et l’exécution des scénarios multimédias interactifs. En outre, un séquenceur inter-médias, appelé ISCORE,a été élaboré à partir de la sémantique Petri net proposée par ce formalisme. Au cours des dernières années, I-SCORE a été utilisé avec succès pour la composition et l’exécution des spectacles et des expositions interactives. Néanmoins, ces applications et les applications émergentes telles queles jeux vidéo et les installations muséales interactives, de plus en plus exigent deux caractéristiques que la version stable actuelle de I-SCORE ainsi que son modèle sous-jacent ne supportent pas : (1)des structures de contrôle flexibles comme des conditionnelles et des boucles ; et (2) des mécanismes pour la vérification automatique de scénarios.Dans cette thèse, nous présentons deux modèles formels pour la composition et la vérification automatique de scénarios interactifs multimédia avec des choix interactifs, i.e., des scénarios où l’interprète ou le système peut prendre des décisions au sujet de leur état d’exécution avec un certain degré de liberté définie par le compositeur.Dans notre première approche, nous définissons un nouveau langage de programmation appelé REACTIVEIS dont les programmes sont définis comme des arbres représentant l’aspect hiérarchique des scénarios interactifs et dont les noeuds contiennent les conditions nécessaires pour démarrer et arrêter les objets temporels (TOS). En outre, nous définissons une sémantique opérationnelle basé sur des arbres marqués, contenant dans leurs noeuds, les informations sur le début et la fin de chaque TO. Nous définissons également une interprétation déclarative de REACTIVEIS comme formules de la logique linéaire intuitionniste avec sous exponentiels (SELL). Nous montrons que cette interprétation est adéquate : les dérivations dans la logique correspondent à des traces du programme et vice-versa.Dans notre deuxième approche, nous présentons un système basé sur des Automates Temporisés.Dans le système proposé, nous modélisons des scénarios interactifs comme un réseau d’automates temporisés et les étendons avec des points interactifs gardés par des conditions, permettant ainsi la spécification de comportements avec branchements. Par ailleurs, nous profitons des outils matures et efficaces pour simuler et vérifier automatiquement des scénarios modélisés comme des automates temporisés. Dans notre système, les scénarios peuvent être synthétisés dans un matériel reconfigurable afin de fournir une faible latence et l’exécution en temps réel.Dans cette thèse, nous explorons également une nouvelle façon de définir et mettre en oeuvre des scénarios interactifs, visant à un modèle plus dynamique en utilisant le langage réactif REACTIVEML.Enfin, nous présentons une extension des scénarios interactifs utilisant des réseaux de Petri colorés(CPN) qui vise à traiter des données complexes, en particulier, les données statiques et dynamiques de flux audio. / Interactive multimedia deals with the computer-based design of scenarios consisting of multimediacontent that interacts with external actions and those of the performer (e.g., multimedialive-performance arts, interactive museum installations, and video games). The multimedia content is structured in a spatial and temporal order according to the author’s requirements. Therefore, thepotentially high complexity of these scenarios requires adequate specification languages for theircomplete description and verification.Interactive scores is a formalism which has been proposed as a model for composing and performing interactive multimedia scenarios. In addition, an inter-media sequencer, called I-SCORE, hasbeen developed following the Petri Net semantics proposed by this formalism. During the last years,I-SCORE has been used successfully for the composition and performance of live performances and interactive exhibitions. Nevertheless, these applications and emergent applications such as videogames and interactive museum installations, increasingly demand two features that the current stable version of I-SCORE as well as its underlying model do not support: (1) flexible control structures such as conditionals and loops; and (2) mechanisms for the automatic verification of scenarios.In this dissertation we present two formal models for composition and automatic verification of multimedia interactive scenarios with interactive choices, i.e., scenarios where the performer or thesystem can take decisions about their execution state with a certain degree of freedom defined bythe composer.In our first approach, we define a novel programming language called REACTIVEIS. This language extends the full capacity of temporal organization of interactive scenarios by allowing the composerto use a defined logical system for the specification of the starting and stopping conditions of temporal objects (TOs). REACTIVEIS programs are formally defined as tree-like structures representing the hierarchical aspect of interactive scenarios and whose nodes contain the conditions needed to startand stop the TOs. Moreover, we define an operational semantics based on labeled trees, containing in their nodes, the information about the start and stop times of each TO.We show that this operational semantics offers an intuitive yet precise description of the behavior of interactive scenarios.We also endowed REACTIVEIS with a declarative interpretation as formulas in Intuitionistic LinearLogic with Subexponentials (SELL). We shall show that such interpretation is adequate: derivations in the logic correspond to traces of the program and vice-versa. Hence, we can use all the meta-theory of Intuitionistic Linear Logic (ILL) to reason about interactive scenarios and develop tools for theverification and analysis of interactive scenarios.In our second approach, we present a Timed Automata (TA) based framework. In the proposed framework, we model interactive scenarios as a network of timed automata and extend them with interactive points (IPs) guarded by conditions, thus allowing for the specification of branching behaviors.Moreover, we take advantage of the mature and efficient tools for TA to simulate and automatically verify scenarios. In our framework, scenarios can be synthesized into a reconfigurable hardware in order to provide a low-latency and real-time execution by taking advantage of the physical parallelism,low-latency, and high-reliability of these devices. Furthermore, we implemented a tool to systematically construct bottom-up TA models from the composition environment of I-SCORE. Doing that, we provide a friendly and specialized environment for composing and automatic verification of interactive scenarios. Finally, we present an extension of interactive scenarios using Colored Petri Nets (CPNs) thataims to handle complex data, in particular, dynamic and static data audio streams. [...]

Les terminaux à conteneurs constituent des interfaces inter-modales essentielles pour le réseau de transport mondial. Une manutention efficace des conteneurs dans des terminaux est d'une importance cruciale pour la réduction des coûts de transport et la détermination des plans d'embarquement. Dans ce rapport de thèse, nous proposons principalement une approche de résolution distribuée à travers la description d'un modèle d'optimisation heuristique distribuée baptisé COSAH COntainer Stacking via multi-Agent approach and Heuristic methodqui permet de simuler, résoudre et optimiser l'espace de stockage disponible pour manier les départs et les arrivées des conteneurs dans un port fluvial ou maritime. Autrement dit, COSAH permet de minimiser le nombre total de mouvements parasites tout en respectant des contraintes dynamiques d'espace et de temps. Les performances de COSAH sont ensuite évaluées sur des instances générées aléatoirement, ainsi que des instances extraites de la réalité d'un port maritime tunisien : le port de Radès. En effet, nous avons procédé à une étude expérimentale implémentant et comparant COSAH à la version centralisée associée, toutes deux basées sur un algorithme de recherche non informée et un algorithme de recherche informée. Les résultats obtenus, présentés et illustrés, montrent l'efficacité de COSAH en particulier, et d'une méthode d'optimisation heuristique distribuée alliant les deux concepts : Agent et Heuristique, en général.