Les systèmes audios incluent les instruments de musique traditionnels (percussions, cordes, vents, voix) et les systèmes électro-acoustiques (amplificateurs de guitares, pédales d’effets, synthétiseurs analogiques). Ces systèmes multi-physiques possèdent une propriété commune : hors des sources d’excitation (les générateurs), ils sont tous passifs. Nous présentons dans cette thèse un ensemble de méthodes automatiques dédiées à leur modélisation, leur simulation et leur contrôle, qui garantissent explicitement et exploitent la passivité du système original. Nous utilisons dans ce travail le formalisme des systèmes hamiltoniens à ports (SHP), introduits en automatique et théorie des systèmes au début des années 1990. Pour la modélisation, on exploite le fait que la connexion de systèmes décrits dans ce formalisme préserve explicitement la dynamique de la puissance dissipée de l'ensemble, pour développer une méthode automatique de modélisation d'instruments complets à partir de modèles élémentaires rassemblés dans un dictionnaire. Pour la simulation, une méthode numérique qui préserve la structure passive des SHP à temps discret a été développée, garantissant ainsi la stabilité des simulations (pour lesquelles le code C++ est généré automatiquement). Concernant le contrôle, on exploite la structure d'interconnexion afin de déterminer automatiquement une forme découplée (sous-systèmes hiérarchisés) pour une certaine classe de SHP. Les systèmes de cette classe sont dits systèmes hamiltonien à ports plats, au sens de la propriété de platitude différentielle, à partir de laquelle une loi de commande en boucle ouverte exacte sur le modèle est générée. / The class of audio systems includes traditional musical instruments (percussion, string, wind, brass, voice) and electro-acoustic systems (guitar amplifiers, analog audio processing, synthesizers). These multi-physical systems have a common property: out of excitation sources (generators), they are all passive. We present a set of automatic methods dedicated to their modeling, simulation and control, which explicitly guarantee and exploit the passivity of the original system. This class of systems is that of port-Hamiltonian systems (PHS), introduced in system theory in the early 1990s. Regarding the models, we exploit the fact that the interconnection of systems described in this formalism explicitly preserves the dynamics of total dissipated power. This enabled the development of an automated method that builds models of complete instruments based on a dictionary of elementary models. Regarding the simulations, we developed a numerical method that preserves the passive structure of PHS in discrete-time domain. This ensures the stability of simulations (for which the C++ code is automatically generated). Regarding the control, we exploit the interconnection structure to automatically build an input-to-output decoupled form for a class of PHS. Systems of this class are flat, within the meaning of the differential flatness approach. A formula that yields the (open loop) control law for these systems is provided.

L'un des aspects fondamentaux des systèmes informatiques modernes, et en particulier des systèmes critiques, est la possibilité d'exécuter plusieurs processus, partageant des ressources communes, de façon simultanée. De par leur nature concurrentielle, le bon fonctionnement de ces systèmes n'est assuré que lorsque leurs comportements ne dépendent pas d'un ordre d'exécution prédéterminé. En raison de cette caractéristique, il est particulièrement difficile de s'assurer qu'un système concurrent ne possède pas de faille. Dans cette thèse, nous étudions la vérification formelle, une approche algorithmique qui vise à automatiser la vérification du bon fonctionnement de systèmes concurrents en procédant par une abstraction vers des modèles mathématiques. Nous considérons deux de ces modèles, les réseaux de Petri et les systèmes d'addition de vecteurs, et les problèmes de vérification qui leur sont associés. Nous montrons que le problème d'accessibilité pour les systèmes d'addition de vecteurs (avec états) à deux compteurs est PSPACE-complet, c'est-à-dire complet pour la classe des problèmes solubles à l'aide d'une quantité polynomiale de mémoire. Nous établissons ainsi la complexité calculatoire précise de ce problème, répondant à une question demeurée ouverte depuis plus de trente ans. Nous proposons une nouvelle approche au problème de couverture pour les réseaux de Petri, basée sur un algorithme arrière guidé par une caractérisation logique de l'accessibilité dans les réseaux de Petri dits continus. Cette approche nous a permis de mettre au point un nouvel algorithme qui s'avère particulièrement efficace en pratique, tel que démontré par notre implémentation logicielle nommée QCover. Nous complétons ces résultats par une étude des systèmes de transitions bien structurés qui constituent une abstraction générale des systèmes d'addition de vecteurs et des réseaux de Petri. Nous considérons le cas des systèmes de transitions bien structurés à branchement infini, une classe qui inclut les réseaux de Petri possédant des arcs pouvant consommer ou produire un nombre arbitraire de jetons. Nous développons des outils mathématiques facilitant l'étude de ces systèmes et nous délimitons les frontières au-delà desquelles la décidabilité des problèmes de terminaison, de finitude, de maintenabilité et de couverture est perdue. / One fundamental aspect of computer systems, and in particular of critical systsems, is the ability to run simultaneously many processes sharing resources. Such concurrent systems only work correctly when their behaviours are independent of any execution ordering. For this reason, it is particularly difficult to ensure the correctness of concurrent systems.In this thesis, we study formal verification, an algorithmic approach to the verification of concurrent systems based on mathematical modeling. We consider two of the most prominent models, Petri nets and vector addition systems, and their usual verification problems considered in the literature.We show that the reachability problem for vector addition systems (with states) restricted to two counters is PSPACE-complete, that is, it is complete for the class of problems solvable with a polynomial amount of memory. Hence, we establish the precise computational complexity of this problem, left open for more than thirty years.We develop a new approach to the coverability problem for Petri nets which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. We demonstrate the effectiveness of our approach by implementing it in a tool named QCover.We complement these results with a study of well-structured transition systems which form a general abstraction of vector addition systems and Petri nets. We consider infinitely branching well-structured transition systems, a class that includes Petri nets with special transitions that may consume or produce arbitrarily many tokens. We develop mathematical tools in order to study these systems and we delineate the decidability frontier for the termination, boundedness, maintainability and coverability problems for these systems.

Cette thèse traite des problématiques relatives à la modélisation, l’analyse et la simulation des systèmes électriques interconnectés. Elle a été principalement motivée par le besoin de comprendre et de clarifier les niveaux de modélisation de certains composants électriques comme les lignes de transmission ainsi que leur habilité à reproduire les différents phénomènes qui présentent un intérêt dans le système. En effet, pour faciliter les études et les simulations, les modèles les plus détaillés et les plus complexes sont généralement remplacés par des modèles plus simples selon le type des phénomènes visés. Usuellement, la structure dynamique de l’ensemble du système n’est pas prise en compte dans l’étape de simplification, ce qui fait que, dans la plupart du temps, des validations expérimentales sont nécessaires. C’est pourquoi un cadre structurel et une vision systémique sont proposés dans cette thèse afin d’apporter des solutions plus générales et plus fiables qui s’adaptent mieux à l’approximation des systèmes électriques. Le cadre proposé il nous a permis : d’une part, d’expliquer par le biais de la réduction l’approximation du modèle à paramètres distribués d’une ligne par un modèle plus simple de dimension finie appelé π et d’autre part, d’étendre les investigations à une échelle plus grande où une nouvelle méthodologie de troncature est proposée pour l’approximation des modèles dynamiques de grande taille. Elle se distingue des méthodes standards par l’efficacité d’évaluation des dynamiques du système même dans des situations particulières ainsi que la prise en compte de divers besoins pratiques. Il s’agit d’une approche mixte qui combine, d’une part, le principe de la troncature modale et, d’autre part, l’énergie de la réponse impulsionnelle afin de préserver les structures dynamique et physique du système. A cela s’ajoute également la question du nombre et choix des entrées des systèmes à paramètres distribués qui est posée ici d’un point de vue de l’automatique afin de lui donner plus d’utilité pratique, surtout dans les simulateurs numériques. L’approche utilisée à cet effet est algébrique, et la contribution est une étude assez détaillée de l’état de l’art sur le sujet qui a finalement affiné d’avantage la problématique et conduit à de nouvelles pistes plus prometteuses car la question est jusqu’alors partiellement résolue. Plus précisément, les investigations doivent se concentrer désormais sur les commandes dites aux bords ou frontières.D’un point de vue pratique, les résultats obtenus dans cette thèse peuvent être exploités dans l’avenir pour améliorer et facilité les techniques actuelles de simulation et d’analyse en adaptant, par exemple, chaque modèle utilisé aux phénomènes à reproduire. / This thesis was motivated by the need to better understand the connection between the models used in simulation of the power systems dynamics and the phenomena which have to be analyzed or reproduced by the simulation. Indeed, to study and to simulate the behavior of the interconnected power systems, the sophisticated models such as the one of the transmission lines are generally replaced by simple ones. Usually, a dynamic structure of the whole system is not taken into account in a simplification step. As a consequence, experimental validations are generally needed to assess the result of the approximation. For this reason, a structural framework and a systemic viewpoint are proposed to make the solutions more general and more appropriate to the approximation of power systems. First, this allows explaining the link between the distributed parameters model of the transmission lines and the finite dimensional one called π model based on the model reduction. Next, a novel mixed approximation methodology for large-scale dynamic models is proposed which allows one to better rate the dynamics of the system in different situations, and to take into account several practical needs. This methodology is based on a mixture between the modal truncation and the energy of the impulse response so that the dynamical and the physical structures of the system remain unchanged. Moreover, in the context of the automatic control theory, the issue related to a number and a choice of input variables for distributed parameters systems is discussed. To address this issue, an algebraic approach is applied. Here, the main contribution is the detailed study conducted on the basis of the state of the art by which a new way is proposed. Because the issue is not fully solved, more investigations have to be focused on the so called boundary control variables. For practical applications, all the results presented in this study can be exploited to further improve numerical simulations and behavioral studies of large-scale power systems.

Cette thèse traite d'une problématique globale qui porte sur la modélisation, l'évaluation et l'optimisation des performances des systèmes multi-états dont les caractéristiques opératoires sont soumises à la dégradation et à des défaillances aléatoires. Dans le domaine de la fiabilité, l'étude du fonctionnement des systèmes (équipements) technologiques a, longtemps, été entreprise en se basant sur la modélisation binaire où deux états sont considérés : l'état d'opération et l'état de défaillance complète. Cependant, de plus en plus de travaux dans la littérature scientifique tiennent compte des nombreuses situations qui peuvent survenir durant la vie utile de certains systèmes. De tels systèmes sont appelés des systèmes multi-états (SME). Les SME sont généralement soumis à divers modes de défaillance avec différents effets sur leurs performances. L'un de ces modes de défaillance, la dégradation, permet aux SME de continuer à assurer leur fonction (service) malgré l'occurrence d'une panne entraînant une réduction partielle de leurs performances nominales. Dans ce cas, la continuité du service est souvent assurée par la redondance, les stocks tampons, la maintenance, les mécanismes de reconfiguration, la tolérance aux fautes, etc. Une abondante littérature a été dédiée aux systèmes ne pouvant être qu'en état d'opération ou hors d'usage (binaires). Ainsi, les stratégies d'amélioration ou de restauration des performances de ces systèmes binaires ont souvent été basées sur l'emploi de la redondance, la maintenance préventive, etc. Cependant, peu de travaux ont été publiés sur les systèmes multi-états (SME). D'où la pertinence de : (a) caractériser les SME, (b) explorer des méthodes de modélisation, d'évaluation et d'amélioration de leurs mesures de performance, (c) mettre en oeuvre des stratégies d'optimisation de ces mesures de performance et des ressources requises

Québec Université Laval, Bibliothèque 2018

Résumé : La présente étude poursuit un double objectif. D'abord, elle cherche à comprendre le processus d'assimilation des systèmes de télésanté lorsque l'on fait passer la télésanté du mode expérimental au mode permanent de prestations de services de soins de santé. Ensuite, elle vise à identifier les facteurs d'influence de ce processus. Empruntant à des théories comme la théorie de la structuration, la théorie institutionnelle et la théorie de la cognition sociale, l'étude formule un modèle de recherche articulant un certain nombre de propositions théoriques relatives au processus d'assimilation des systèmes de télésanté et des facteurs influençant ce processus. En termes de stratégie de recherche, nous avons recouru à l'étude de cas unique. Pour collecter les informations, nous avons réalisé 23 entrevues semi-dirigées et analysé plus de 200 pages de documents que nous avons collectés avant et pendant la période de collecte de données. Pour le traitement des données, nous avons adopté les techniques de théorisation ancrée et nous nous sommes servis du logiciel Atlas.ti. Les résultats montrent en effet que le processus d'assimilation tel qu'il a émergé de la théorisation ancrée est bien plus complexe que le modèle de recherche a priori que nous avons élaboré. Par exemple, au niveau individuel l'assimilation suit deux parcours alternatifs et elle est influencée par des facteurs tels : l'utilité perçue de la télésanté, les aspirations et les attributs individuels des utilisateurs lesquels conduisent à l'adoption de comportements de citoyenneté organisationnelle. De plus, le nouveau modèle explicite la dynamique entre les phénomènes reliés au processus d'assimilation, les stratégies d'actions et d'interactions entre les acteurs, les conditions contextuelles du processus, les conditions causales, les conditions intervenantes et les conséquences. Au plan théorique, cette étude comporte plusieurs contributions. En particulier, elle étend les recherches antérieures sur l'assimilation des technologies en proposant un modèle multiniveau qui précise la nature du phénomène aux niveaux individuel, groupai et organisationnel. L'étude comporte également des implications pour la pratique. En particulier, elle souligne l'importance d'examiner le processus d'assimilation à l'intérieur du continuum des phénomènes entourant le déploiement de systèmes de télésanté. À ce compte, elle aide à comprendre pourquoi les actions de gestion visant à faciliter le processus d'assimilation doivent être mises en oeuvre dès la phase d'adoption. Par exemple, les questions relatives à la compatibilité entre les systèmes et les infrastructures de travail de l'organisation devraient être gérées au cours de la phase de développement. En bref, même si le processus d'assimilation est ultérieur à l'implantation des systèmes, les facteurs qui sont susceptibles de l'influencer devraient être pris en compte avant l'acquisition de systèmes. Nonobstant la qualité des résultats de cette étude, certaines questions demeurent non répondues. Celles-ci ouvrent de nouvelles avenues de recherche. Une première avenue immédiate serait de poursuivre cette étude afin de prendre en compte les évolutions récentes de la mise en oeuvre de la télésanté dans les RUIS. La prochaine étape consistera à investir ce que l'on aura appris au sujet de l'assimilation des systèmes de télésanté à d'autres innovations technologiques dans d'autres contextes organisationnels.||Abstract : The purpose of this study is twofold. First, it seeks to understand the process of assimilation of telehealth systems when telehealth is brought out of experimental settings into mainstream clinical care. Second, it seeks to determine the factors that influence this process. Borrowing from institutional, structuration and social cognition theories, a comprehensive research model is proposed to explain the nature of the process of assimilation of telehealth systems in healthcare organizations and the factors that affect it. We adopted a qualitative research methodology.The first phase is devoted to testing of the theoretical propositions of the research model. Since some propositions failed this test, we conducted a second phase which consisted of building a grounded theory of the assimilation of telehealth systems. In terms of research strategy, we used a single case study. Data were obtained from 23 semi-structured interviews, documentation was used as secondary source. For data processing, grounded theory analysis techniques along with Atlas.ti were used. The research findings show that the assimilation process as it emerged from the data is more complex than the a priori research model that we developed. For example, individual-level assimilation follows two alternative routes and is influenced by at least four factors.The perceived usefulness of telehealth, aspirations and attributes of individual users which lead to the adoption of organizational citizenship behaviors.The first refers to the usefulness of telehealth with the problems that confront both patient and clinician. Two other conditions refer to personal aspirations and to user's individual attributes. However, the influence of personal aspirations and individual attributes does not happen directly. Rather, it leads to the adoption of specific behaviors that positively influence the assimilation of telehealth. For instance, altruism, civility, professionalism, and tolerance are examples of behaviours that illustrate organizational citizenship. In addition, the new model makes explicit the dynamic between the phenomena underlying the assimilation process, the action/interaction strategies between actors, and the contextual, causal and intervening conditions of the process, including the consequences. This research expands on previous work by examining the process of assimilation from a multilevel perspective. Earlier studies on organizational assimilation of information technologies considered assimilation as an exclusively organizational phenomenon.The result, they have undoubtedly overshadowed more micro or meso explanations that could enrich our understanding still more. Unlike prior studies, our model proposes a detailed account of the assimilation process by clarifying both the structure and the functional relationships of assimilation. Put simply, the model accounts for how individual, group and organization characteristics interact to structure assimilation. Briefly, the adoption of a multilevel perspective resulted in a more comprehensive understanding of how the assimilation process unfolds across organizational levels. Our study also has implications for practice. In particular, it helps understand why managerial actions meant to facilitate assimilation should be employed as early as the adoption phase. For instance, issues related to the systems' compatibility with the organization's work infrastructure should be managed during the development phase. Even though routinization and infusion are post-implementation behaviors, factors that are likely to influence them should be taken into consideration before systems are acquired.

The application domains of this thesis are Health Smart Homes, and the research is more precisely centered on the improvement of daily-living for cognitively impaired persons and theirs caregivers.The proposed system can observe the context of each person, personalize the environment and assist the tasks detected if they need to be. Every action of the system is as unobtrusive as possible and takes into consideration the presence of more than one person. To personalize and assist the daily-living activities of a lone person, we need to know his personal context. This context is the conjunction of the preferences and habits, the illness or impairment, the movements in the smart home and the state of the various sensor and electrical devices, and the current activities that are detected for one person. To be able to assist many persons simultaneously, we need to compute the overall conjunction of each and every person's context since every presence can influence the global context and every personal one. This complexity brings a lot of problems like the multiple person localization and identification, or the personalization and assistance of multiple persons in the same space with various activities. Those problems are even more interesting since, following an ethical choice to ensure inhabitant's privacy, this project avoid the use of some intrusive technologies.

Cette thèse propose un formalisme de représentation de connaissances adapté à l’enseignement explicite de connaissances stratégiques par système tutoriel intelligent (STI). Le formalisme est une proposition de solution au fait que dans le domaine des systèmes tutoriels intelligents multidisciplinaires, les efforts de modélisation croissent considérablement avec la complexité du domaine à enseigner. Le problème est particulièrement contraignant avec les domaines qui présentent des stratégies multiples de résolution de problèmes. Par ailleurs, le formalisme est aussi une réaction au constat que peu de systèmes tutoriels s’intéressent actuellement à l’enseignement explicite des stratégies, alors que plusieurs études en ont démontré les avantages. Le formalisme maintient le processus d’encodage du raisonnement stratégique à un niveau simple sans compromettre la fidélité de représentation, ce qui a été validé expérimentalement avec un groupe d’étudiants. Les mêmes expérimentations ont permis de confirmer l’efficacité du système tutoriel utilisant le formalisme dans plusieurs aspects : la résolution de problèmes avec explication et justification des étapes, l’interprétation des actions d’un apprenant d’un point de vue stratégique, et l’évaluation du degré de maîtrise d’une stratégie par un apprenant. L’architecture résultante, avec le module responsable du raisonnement stratégique activable à volonté, est particulièrement adaptée pour des études évaluant les impacts de l’enseignement explicite des stratégies et la réutilisation des connaissances stratégiques acquises d’un domaine à l’autre.

Résumé: Les propriétés que l'on souhaite exprimer sur les applications système d'information ne peuvent se restreindre aux propriétés statiques, dites propriétés d'invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l'état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l'efficacité pour le domaine des systèmes d'information est plutôt réduite à cause de l'explosion combinatoire de l'espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d'autant plus que ces dernières ne sont pas outillées. Pour pallier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d'atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d'obligations de preuve permettant de les prouver. Une propriété d'atteignabilité permet d'exprimer qu'il existe au moins une exécution du système qui permet d'atteindre un état cible à partir d'un état initial donné. Par contre, la propriété de précédence permet de s'assurer qu'un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l'utilisateur de la tâche de génération d'obligations de preuve qui peut être longue et fastidieuse.||Abstract: The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties , that depend on states taken at the same time. Indeed, some properties, called dynamic properties, may refer to the past or the future states of the system. Existing work on the verification of such properties typically use model checking whose effectiveness for data-intensive applications is rather limited due to the combinatorial explosion of the state space. In addition, the techniques, based on the proof, require fairly advanced knowledge and mathematical reasoning especially that they are not always supported by tools. To overcome these limitations, we propose in this thesis proof-based verification approaches that use the B formal method. We are mainly interested in reachability and precedence properties for which we defined formal rules to generate proof obligations that permit to discharge them. A reachability property expresses that there is at least one execution scenario that permits to reach a target state from a given initial state while a precedence property ensures that a given system state is always preceded by another state. To make these different approaches workable, we have developed a support tool that permits to discharge the users from tedious and error-prone tasks.

L’utilisation de cellules vivantes dans un procédé industriel tire profit de la complexité inhérente au vivant pour accomplir des tâches complexes et dont la compréhension est parfois limitée. Que ce soit pour la production de biomasse, pour la production de molécules d’intérêt ou pour la décomposition de molécules indésirables, ces procédés font appel aux multiples réactions formant le métabolisme cellulaire. Afin de décrire l’évolution de ces systèmes, des modèles mathématiques composés d’un ensemble d’équations différentielles sont utilisés. Au fur et à mesure que les connaissances du métabolisme se sont développées, les modèles mathématiques le représentant se sont complexifiés. Le niveau de complexité requis pour expliquer les phénomènes en jeu lors d’un procédé spécifique est difficile à définir. Ainsi, lorsqu’on tente de modéliser un nouveau procédé, la sélection du modèle à utiliser peut être problématique. Une des options intéressantes est la sélection d’un modèle provenant de la littérature et adapté au procédé utilisé. L’information contenue dans le modèle doit alors être évaluée en fonction des phénomènes observables dans les conditions d’opération. Souvent, les modèles provenant de la littérature sont surparamétrés pour l’utilisation dans les conditions d’opération des procédés ciblées. Cela fait en sorte de causer des problèmes d’identifiabilité des paramètres. De plus, l’ensemble des variables d’état utilisées dans le modèle n’est pas nécessairement mesuré dans les conditions d’opération normales. L’objectif de ce projet est de cibler l’information utilisable contenue dans les modèles par la simplification méthodique de ceux-ci. En effet, la simplification des modèles permet une meilleure compréhension des dynamiques à l’oeuvre dans le procédé. Ce projet a permis de définir et d’évaluer trois méthodes de simplification de modèles mathématiques servant à décrire un procédé de culture cellulaire. La première méthode est basée sur l’application de critères sur les différents éléments du modèle, la deuxième est basée sur l’utilisation d’un critère d’information du type d’Akaike et la troisième considère la réduction d’ordre du modèle par retrait de variables d’état. Les résultats de ces méthodes de simplification sont présentés à l’aide de quatre modèles cellulaires provenant de la littérature.