Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Dans ce mémoire, la conception de systèmes numériques complexes, et notamment de systèmes embarqués critiques, est abordée au travers d'une méthodologie allant de la modélisation formelle à l'implantation sur FPGA : la méthodologie HILECOP. Celle-ci offre au concepteur la possibilité de représenter dans un modèle formel d'une part l'architecture du système selon un assemblage de composants, et d'autre part le comportement de ces composants et leur composition par réseaux de Petri temporels. Le modèle décrit est ensuite transformé automatiquement en un modèle implémentable (en langage VHDL) pour son exécution sur la cible matérielle, mais également en un modèle analysable pour permettre l'analyse formelle des propriétés du système. Les deux objectifs principaux des travaux présentés sont l'étude de la conformité d'un point de vue comportemental entre les différents modèles utilisés dans la méthodologie (modèle conçu, modèle implémentable et modèle analysable), ainsi que l'intégration d'un mécanisme de gestion efficace des exceptions. Ces travaux ont permis de fiabiliser l'implémentation du modèle et d'obtenir un modèle analysable plus pertinent par rapport au modèle conçu, dans le sens où il garantit l'inclusion du comportement du modèle conçu dans celui du modèle analysé et réduit, dans une certaine mesure, le risque d'explosion combinatoire. Les limites de la pertinence des résultats obtenus par analyse formelle sont de plus désormais connues. En ce qui concerne la gestion des exceptions, principalement étudiée au niveau comportemental, le mécanisme de la macro-place a été retenu et adapté aux contraintes fonctionnelles et non-fonctionnelles des systèmes embarqués critiques. L'apport de la macro-place et la conservation de la conformité ont pu être validés sur des modèles industriels relatifs à l'architecture numérique de neuroprothèses. / In this thesis, the conception of digital complex systems, and notably of critical embedded systems, is discussed through a methodology which goes from formal modeling to the implementation on a FPGA: the HILECOP methodology. This methodology offers, to a designer, the possibility of representing in a formal model from one hand the digital architecture thanks to some components' assembly, and on the other hand the behavior of these components and their composition, thanks to time Petri nets. The described model is then automatically transformed in an implementable model (in the VHDL language) for its execution on a hardware target, but also in an analyzable model to allow some formal analysis on system properties to be performed. The two main goals of the presented work are the study of the behavioral conformity between the different models used in the methodology (designed model, implementable model and analyzable model) and the integration of an efficient mechanism for handling exception. These works allow to have a more reliable implementation of the model and to obtain a more relevant analyzable model. It is now possible to guarantee that the behavior of the designed model is included in the analyzed one. The risk of combinatorial explosion has also been reduced to some extent. The limits of the relevance of the obtained results thanks to the formal analysis are henceforth known. As for exception handling, it has been mostly studied on the behavioral level. The mechanism of the macroplace has been chosen and adapted to meet the functional and non-functional constraints of critical embedded systems. The benefits given by the use of the macroplace and the preservation of the conformity between the models have been validated on industrial models relative to the digital architecture of neuroprosthetics.

Les systèmes de surveillance et de supervision jouent un rôle majeur pour la sécurité des installations industrielles et la disponibilité des équipements. Signaler le plus tôt possible à l'opérateur les écarts détectés par rapport au comportement nominal prévu est fondamental pour la mise en œuvre des actions préventives et correctives sur le procédé. Certains types d'installations tels que les procédés chimiques et de traitement par lots (batch systems) présentent une grande complexité pour la commande/surveillance en raison de leur caractère hybride (aspects continus et discrets étroitement liés), du nombre de variables mis en jeu et de la complexité de leurs relations. Cette complexité est accentuée par la nécessité de nombreux changements de modes opératoires qui conduisent à de nombreuses phases transitoires. <br />La surveillance de ces phases transitoires est délicate. Le nombre élevé de variables à considérer rend difficile l'interprétation du comportement du procédé. En cas de défaut, un diagnostic devient alors une tâche complexe. Les écarts, même marginaux, par rapport au comportement nominal souhaité doivent être surveillés de façon à avertir l'opérateur sur des évolutions non prévues qui peuvent aboutir à une défaillance. Les écarts marginaux peuvent indiquer un dysfonctionnement qui dégénère lentement ou encore une conduite inadéquate de l'opérateur ou du système de pilotage. <br />Pour faire face à la complexité, le système de commande/surveillance est hiérarchisé selon la hiérarchie procédurale proposée par la norme ISA88. Notre démarche de surveillance et diagnostic se situe à deux niveaux hauts de cette hiérarchie procédurale : i) au niveau d'une opération et plus particulièrement lors du transitoire du mode opératoire (MOt) où les relations d'influence entre les variables sont faiblement connues ou non connues, ii) au sein d'une phase où les relations d'influence sont connues dans un intervalle de temps appartenant à l'horizon du mode opératoire.<br />Concernant la complexité des relations des variables mises en jeu, il n'est pas toujours facile et forcément nécessaire une modélisation précise de la dynamique du procédé. Dans ce cas, les approches qualitatives permettent une représentation avec un degré d'abstraction plus en adéquation avec le niveau haut de surveillance considéré. <br />Pour cela, nous proposons une abstraction des dynamiques continues basée sur un raisonnement temporel et événementiel compatibles avec les niveaux de la hiérarchie de surveillance. Cette abstraction est basée sur un partitionnement temporel flou de la dynamique des variables importantes définissant ainsi un ensemble d'états qualitatifs. Des mécanismes de vérification et de rétablissement de cohérence temporelle entre les variables sont proposés de façon à décrire les relations dynamiques locales existantes. Pour son pouvoir de représentation et pour rester cohérent avec une approche hiérarchique basée réseau de Petri, les Réseaux de Petri Temporels Flous ont été choisis.

Les systèmes complexes ferroviaires étant de plus en plus contraints par des autorités de décision placées à un haut niveau d'abstraction, il devient problématique d'imposer des critères à une autre échelle que fonctionnelle. Ainsi, dès lors que l'on descend plus bas, nous sommes confrontés à des spécificités des systèmes nationaux qui font perdre la généralité du travail des décisionnaires Européens. Le problème est qu'à chaque niveau d'abstraction, des méthodes d'évaluation du risque existent, mais sans être compatibles entre elles. Par ailleurs, la combinaison des couches et la vision fonctionnelle du système ne prennent pas en compte l'impact des fonctions les unes sur les autres, ni le lien entre le niveau global et les composants afin d'allouer la sécurité.Nous proposons donc une démarche harmonisée d'évaluation du risque, capable de répartir les contraintes définies au niveau fonctionnel abstrait sur les entités qui implémentent les systèmes avec leurs spécificités.Notre contribution est méthodologique. Elle part d'un modèle fonctionnel du système ferroviaire constitué en couches. Le but étant de représenter ce système sans dépendance entre les fonctions, il a fallu les traduire indépendamment des autres en faisant apparaître les entrées/sorties comme des places/transitions d'un réseau de Petri. A chaque couche de la décomposition correspond une classe de réseau de Petri. Ainsi, à la couche structurelle, nous associons les réseaux de Petri Temporels; à la couche fonctionnelle les réseaux de Petri stochastiques et à la couche logique les réseaux de Petri Prédicats Transitions

Le " serious gaming " est une approche récente pour mener des activités " sérieuses " telles que communiquer, sensibiliser ou apprendre, en utilisant les techniques mises en œuvre dans les jeux vidéo. Les jeux sérieux sont devenus aujourd'hui un élément incontournable de la formation en ligne. C'est dans ce cadre du serious gaming pour la formation que se situe ce sujet de thèse. En effet, quelle que soit l'acception privilégiée, de nombreuses questions de recherche se posent. En particulier, comment peut-on évaluer les connaissances acquises par le joueur/apprenant à travers le jeu ? Nous sommes concentrés sur les jeux de type étude de cas utilisés notamment en gestion ou en médecine et proposons une méthode basée sur l'Evidence Centered Design pour concevoir le suivi de l'apprenant à des fins de diagnostic à destination de l'enseignant et de l'apprenant. Les actions liées aux études de cas sont très proches des actions métiers et recourent à des règles bien précises. Nous avons fait le choix de les représenter à l'aide de réseaux de Petri. Pour apporter de la sémantique à l'analyse par réseau de Petri, nous l'avons adossé à une ontologie du domaine et des actions de jeu. L'ontologie apporte une complémentarité non négligeable au réseau de Petri qui a une dimension purement procédurale. Nous combinons des réseaux de Petri et les ontologies afin de produire des indicateurs de performance pour cette catégorie particulière de jeux sérieux. L'étude des erreurs nous a conduits à proposer une taxinomie particulière pour les jeux sérieux en nous inspirant notamment des travaux réalisés dans le domaine de la sécurité. / "Serious gaming" is a recent approach, using the techniques implemented in video games, to conduct "serious" activities such as communication, awareness and learning. Serious games have now become an essential element of online training. This thesis takes place in the context of serious games for training. Indeed, whatever the preferred meaning, many research questions arise. In particular, how can we assess the knowledge acquired by the player / learner through the game? We have focused on case study type games used especially in management or medicine. We propose a method based on Evidence Centered Design to plan the monitoring of the learner for diagnostic purposes to the teacher and the learner. Actions in case studies are very close to business actions and resort to specific rules. We have chosen to represent them using Petri nets. To bring semantics to the Petri net analysis, we have added a domain and game action ontology. The ontology provides a significant complementarity to Petri net that has a purely procedural dimension. We have combined Petri nets and ontologies to produce performance indicators for this particular category of serious games. The study of errors led us to propose a particular taxonomy for serious games based on the work done in the field of security.

Cette thèse contribue à l’identification de modèles compacts et expressifs de Systèmes à Evénements Discrets (SED) réactifs, à des fins de rétro-conception ou de certification. L’identification est passive, et boîte-noire, la connaissance se limitant aux signaux d’entrées/sorties du système. Les Réseaux de Petri Interprétés (RdPI) permettent de modéliser à la fois le comportement observable (causalités entrées/sorties observées directement), et le comportement non observable du système (évolutions de variables internes). Cette thèse vise à identifier des modèles RdPI à partir d’une séquence observée de vecteurs entrées/sorties. Notamment, l’enjeu étant de traiter des systèmes concurrents de taille réaliste, l’approche développée permet le passage à l’échelle de résultats précédents.La construction de la partie observable est d’abord améliorée par l’ajout d’un filtre. Celui-ci détecte et supprime les synchronisations parasites causées par le contrôleur en présence de systèmes concurrents. Une nouvelle approche est ensuite proposée pour découvrir la partie non observable, basée sur l’utilisation de projections, et garantissant la reproductibilité du comportement observé malgré la concurrence. Une heuristique permet de construire un modèle satisfaisant pour la rétro-ingénierie, à coût de calcul limité. Enfin, une approche distribuée est proposée pour réduire davantage le coût de calcul, en partitionnant automatiquement le système en sous-systèmes. L’effet cumulatif de ces contributions est illustré par l’identification de RdPI sur un système de taille raisonnable, validant leur efficacité. / This thesis proposes a method to identify compact and expressive models of closed-loop reactive Discrete Event Systems (DES), for reverse-engineering or certification. The identification is passive, and blackbox, accessible knowledge being limited to input/output signals. Interpreted Petri Nets (IPN) represent both the observable behaviour (direct input/output causalities) and the unobservable behaviour (internal state evolutions) of the system. This thesis aims at identifying IPN models from an observed sequence of I/O vectors. The proposed contributions extend previous results towards scalability, to deal with realistic systems who exhibit concurrency.Firstly, the construction of the observable part of the IPN is improved by the addition of a filter limiting the effect of concurrency. It detects and removes spurious synchronizations caused by the controller. Then, a new approach is proposed to improve the discovery of the unobservable part. It is based on the use of projections and guarantees the reproduction of the observed behaviour, despite concurrency. An efficient heuristic is proposed to compute a model adapted to reverse-engineering, limiting the computational cost. Finally, a distributed approach is proposed to further reduce the computational cost, by automatically partitioning the system into subsystems. The efficiency of the cumulative effect of these contributions is validated on a system of realistic size.

Les travaux de thèse s‟inscrivent dans le cadre de la conception des systèmes de production/assemblage pour les produits de taille micrométrique, appelés micro-produits. Il s‟agit de produits constitués de composants de taille submillimétrique, si bien qu‟il est difficile, voire impossible, de les observer à l‟oeil nu et encore de les manipuler précisément soit directement avec les doigts, soit avec un outillage manuel. FEMTO-ST, dans son équipe SAMMI - Systèmes Automatisés de Micromanipulation et de Micro assemblage - propose des solutions robotisées pour la manipulation et l‟assemblage de ces microproduits. Ces microrobots sont conçus et réalisés pour tenir compte des forces en présence à cette échelle et les exploiter au mieux pour une manipulation dextre et précise. L‟intégration de ces microrobots pour concevoir des systèmes de production - nous traitons ici le problème du micro-assemblage - a fait émerger le concept de micro-usine. Au niveau international, nous avons pris un positionnement original en proposant une modularité non seulement au niveau des cellules de production mais également à l‟intérieur de ces cellules. Cette modularité porte à la fois sur les structures physiques mais également sur les systèmes de commande et de supervision. Dans ce manuscrit, nous proposons d‟étudier la pertinence de cette décomposition modulaire en fonction des conditions de production. Notamment, nous nous placerons dans le contexte de production changeante nécessitant réorganisation et/ou reconfiguration du système de production. Trois parties composent le travail de thèse. Nous avons établi une structure de micro-usine et une stratégie de commande dont nous avons identifié les propriétés. Nous avons ensuite formalisé une architecture des données. Enfin, l‟étude du comportement a été obtenue par simulation d‟un modèle réalisé par réseau de Petri stochastique et T-temporisé. L‟évolution stochastique se justifie par l‟incertitude inhérente au micromonde, celle-ci est d‟autant moins importante que s‟accroit la connaissance et le savoir-faire dans une situation donnée. La temporisation permet de prendre en considération les durées relatives des reconfigurations ou réorganisations qui évoluent au gré des expérimentations. Dans le cadre d‟une conception orientée objet, les modélisations sont établies au moyen du langage de modélisation graphique UML qui autorise une analyse syntaxique. Concernant les études menées avec le modèle mathématique discret de réseau de Pétri, l‟outil de simulation utilisé est PACE - IBE Simulation Engineering Gmbh -. Ce logiciel permet une programmation conditionnant les transitions grâce au langage de programmation orienté objet, SMALLTALK, pour temporiser et rendre stochastique l‟exécution du modèle. PACE comporte par ailleurs une interface graphique utilisateur souple et lisible. Les résultats de simulation sont ensuite analysés et mis en forme avec MATLAB. Ces résultats nous ont montré la pertinence de l‟approche modulaire et du choix de décomposition mis en place pour assurer de bonnes performances à une cellule de micro-assemblage.

Ce mémoire est dédié à l'étude de la stabilité des systèmes non linéaires à commutation, systèmes qui peuvent être considérés comme une abstraction de haut niveau d'un système hybride, dans lequel la dynamique discrète est complètement omise. Ce problème est abordé de manières différentes : la stabilité conditionnelle par contrôle des commutations, la stabilisation uniforme et la commande sans modèle. Après une large introduction, le second chapitre se focalise sur la construction d'une séquence de commutation qui assure la stabilité du système. Cette approche repose sur la réécriture du système non linéaire par une représentation polytopique, utilisée pour dégager des conditions suffisantes en termes d'inégalités matricielles. Dans le troisième chapitre, la stabilisation uniforme est abordée. Une condition nécessaire et suffisante y est dégagée, construite sur la notion nouvelle de fonction de Lyapunov contrôlée commune. Dans le quatrième chapitre, un modèle formel est introduit pour représenter uniquement l'ensemble des scénarios admissibles par la physique du système. Pour ce faire, un réseau de Petri temporel est utilisé, permettant ainsi par son analyse la caractérisation de l'ensemble des scénarios admissibles. Divers concepts de stabilité sont par suite appliqués au modèle résultant. Un dernier chapitre propose une approche originale des systèmes à commutation, par une commande sans modèle de ces derniers, c'est-à-dire sans en connaître la dynamique des différents modes. L'algorithme proposé est basé sur des méthodes algébriques d'estimations rapides de dérivées et de paramètres, assurant ainsi une stabilité pratique si les commutations ne sont pas trop rapides.

La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple Uppaal) et les réseaux de Petri temporisés (par exemple Tina). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non-temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec Uppaal) et vers des réseaux de Petri temporisés (pour la vérification avec Tina). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple.

Les systèmes complexes ferroviaires étant de plus en plus contraints par des autorités de décision placées à un haut niveau d'abstraction, il devient problématique d'imposer des critères à une autre échelle que fonctionnelle. Ainsi, dès lors que l'on descend plus bas, nous sommes confrontés à des spécificités des systèmes nationaux qui font perdre la généralité du travail des décisionnaires Européens. Le problème est qu'à chaque niveau d'abstraction, des méthodes d'évaluation du risque existent, mais sans être compatibles entre elles. Par ailleurs, la combinaison des couches et la vision fonctionnelle du système ne prennent pas en compte l'impact des fonctions les unes sur les autres, ni le lien entre le niveau global et les composants afin d'allouer la sécurité.Nous proposons donc une démarche harmonisée d'évaluation du risque, capable de répartir les contraintes définies au niveau fonctionnel abstrait sur les entités qui implémentent les systèmes avec leurs spécificités.Notre contribution est méthodologique. Elle part d'un modèle fonctionnel du système ferroviaire constitué en couches. Le but étant de représenter ce système sans dépendance entre les fonctions, il a fallu les traduire indépendamment des autres en faisant apparaître les entrées/sorties comme des places/transitions d'un réseau de Petri. A chaque couche de la décomposition correspond une classe de réseau de Petri. Ainsi, à la couche structurelle, nous associons les réseaux de Petri Temporels; à la couche fonctionnelle les réseaux de Petri stochastiques et à la couche logique les réseaux de Petri Prédicats Transitions