Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Les systèmes informatiques envahissent notre vie quotidienne et sont devenus des éléments essentiels de chacun de nos instants de vie. La technologie de l'information est un secteur d'activités offrant des opportunités considérables pour l'innovation et cet aspect paraît sans limite. Cependant, des systèmes à logiciel intégré ont donné des résultats décevants. Selon les constats, ils étaient non fiables, parfois dangereux et ne fournissaient pas les résultats attendus. La faiblesse des pratiques de développement constitue la principale raison des échecs de ces systèmes. Ceci est dû à la complexité des logiciels modernes et au manque de connaissances adéquates et propres. Le développement logiciel fournit un cadre contribuant à simplifier la conception de systèmes complexes, afin d'en obtenir une meilleure compréhension et d'assurer une très grande qualité à un coût moindre. Dans les domaines de l'automatique, de la surveillance médicale, de l'avionique..., les systèmes embarqués hautement critiques sont candidats aux erreurs pouvant conduire à des conséquences graves en cas d'échecs. La thèse vise à résoudre ce problème, en fournissant un ensemble de techniques, d'outils et un cadre pour développer des systèmes hautement critiques, en utilisant des techniques formelles à partir de l'analyse des exigences jusqu'à la production automatique de code source, en considérant plusieurs niveaux intermédiaires. Elle est structurée en deux parties: d'une part des techniques et des outils et d'autre part des études de cas. La partie concernant des techniques et des outils présente une structure intégrant un animateur de modèles en temps-réel, un cadre de correction de modèles et le concept de charte de raffinement, un cadre de modélisation en vue de la certification, un modèle du coeur pour la modélisation en boucle fermée et des outils de générations automatiques de code. Ces cadres et outils sont utilisés pour développer les systèmes critiques à partir de l'analyse des exigences jusqu'à la production du code, en vérifiant et en validant les étapes intermédiaires en vue de fournir un modèle formel correct satisfaisant les propriétés souhaitées attendues au niveau le plus concret. L'introduction de nouveaux outils concourt à améliorer la vérification des propriétés souhaitées qui ne sont pas apparentes aux étapes initiales du développement du système. Nous évaluons les propositions faites au travers de cas d'études du domaine médical et du domaine des transports. De plus, le travail de cette thèse a étudié la représentation formelle des protocoles médicaux, afin d'améliorer les protocoles existants. Nous avons complètement formalisé un protocole réel d'interprétation des ECG, en vue d'analyser si la formalisation était conforme à certaines propriétés relevant du protocole. Le processus de vérification formelle a mis en évidence des anomalies dans les protocoles existants. Nous avons aussi découvert une structure hiérarchique pour une interprétation efficace permettant de découvrir un ensemble de conditions qui peuvent être utiles pour diagnostiquer des maladies particulières à un stade précoce. L'objectif principal du formalisme développé est de tester la correction et la consistance du protocole médical / Software systems are pervasive in all walks of our life and have become an essential part of our daily life. Information technology is one major area, which provides powerful and adaptable opportunities for innovation, and it seems boundless. However, systems developed using computer-based logic have produced disappointing results. According to stakeholders, they are unreliable, at times dangerous, and fail to provide the desired outcomes. Most significant reasons of system failures are the poor development practices for system development. This is due to the complex nature of modern software and lack of adequate and proper understanding. Software development provides a framework for simplifying the complex system to get a better understanding and to develop the higher fidelity quality systems at lower cost. Highly embedded critical systems, in areas such as automation, medical surveillance, avionics, etc., are susceptible to errors, which can lead to grave consequences in case of failures. This thesis intends to contribute to further the use of formal techniques for the development computing systems with high integrity. Specifically, it addresses that formal methods are not well integrated into established critical systems development processes by defining a new development life-cycle, and a set of associated techniques and tools to develop highly critical systems using formal techniques from requirements analysis to automatic source code generation using several intermediate layers with rigorous safety assessment approach. The approach has been realised using the Event-B formalism. This thesis has mainly two parts: techniques and tools and case studies. The techniques and tools section consists of development life-cycle methodology, a framework for real-time animator, refinement chart, a set of automatic code generation tools and formal logic based heart model for close loop modeling. New development methodology, and a set of associated techniques and tools are used for developing the critical systems from requirements analysis to code implementation, where verification and validation tasks are used as intermediate layers for providing a correct formal model with desired system behavior at the concrete level. Introducing new tools help to verify desired properties, which are hidden at the early stage of the system development. We also critically evaluate the proposed development methodology and developed techniques and tools through case studies in the medical and automotive domains. In addition, the thesis work tries to address the formal representation of medical protocols, which is useful for improving the existing medical protocols. We have fully formalised a real-world medical protocol (ECG interpretation) to analyse whether the formalisation complies with certain medically relevant protocol properties. The formal verification process has discovered a number of anomalies in the existing protocols. We have also discovered a hierarchical structure for the ECG interpretation efficiently that helps to find a set of conditions that can be very helpful to diagnose particular disease at the early stage. The main objective of the developed formalism is to test correctness and consistency of the medical protocol

Ces travaux de thèse s’intègrent au sein du projet Biocarb lancé par le Commissariat à l’Énergie Atomique dont l’objectif est de développer des procédés de production de carburants liquides ou gazeux à partir de gaz de synthèse riche en H2 et CO obtenu par gazéification de la biomasse lignocellulosique. L’objectif de cette étude est d’étudier le comportement de particules de biomasse millimétriques lors de la pyrolyse dans des conditions types de gazéifieurs industriels tels que les réacteurs à lit fluidisé ou à flux entraîné, qui fonctionnent pour des flux de chaleur élevés (105 – 106 W⋅m-2) et pour de hautes températures (>800°C). Tout d’abord, des expériences de pyrolyse sont menées à 800 et 950°C dans un four à chute de laboratoire sur des particules de bois entre 350 et 800 μm. Les résultats montrent que dans les conditions de l’étude, l’augmentation de la taille de la particule augmente seulement la durée de la pyrolyse mais ne modifie pas les rendements ou la composition du solide et du gaz au cours de la pyrolyse. Par ailleurs, des mesures basées sur la technique de PTV (Particle Tracking Velocimetry) sont réalisées à température ambiante pour caractériser la taille et la densité des particules de bois brut et de résidu, et valider une corrélation donnant le coefficient de traînée qui sert à calculer le temps de séjour des particules dans le réacteur. On constate à la fin de la pyrolyse une diminution de la densité comprise entre 70 et 80% ainsi qu’une diminution de la taille des particules entre 25 et 40%. Les résultats montrent également que la vitesse de glissement de la particule et l’évolution de ses propriétés doivent être prises en compte lors du calcul de sa vitesse. Enfin, à partir des résultats expérimentaux, un modèle unidimensionnel à coeur rétrécissant est développé pour décrire le comportement d’une particule de bois lors de sa pyrolyse. Le modèle est capable de prévoir l’évolution du rendement en solide, en gaz total et en goudrons au cours de la pyrolyse ainsi que la vitesse de glissement de la particule et son temps de séjour dans le réacteur.L’analyse de sensibilité du modèle montre que même pour des particules millimétriques, une connaissance précise de la chaleur de réaction associée à la pyrolyse, de la densité du bois et de la conductivité thermique du résidu solide est essentielle / The present work is part of a project of the French energy research centre Commissariat à l’Energie Atomique. The goal of the project is to develop processes of production of gaseous or liquid fuel from synthesis gas obtained by gasification of lignocellulosic biomass. The objective of the present work is to study the pyrolysis behaviour of millimetric biomass particles under the operating conditions encountered in fluidized bed or entrained flow gasifiers, namely high external heat flux (105 – 106 W⋅m-2) and high temperature (> 800°C). First, pyrolysis experiments are conducted at 800 and 950°C in a lab-scale drop tube reactor on wood particles between 350 and 800 μm. The results show that under the explored conditions, the increase of the particle size only increases the time required for pyrolysis but does not affect the product distribution during pyrolysis. Since in the pyrolysis experiments, the particle residence time cannot be directly measured, PTV (Particle Tracking Velocimetry) measurements are performed at room temperature to characterize the evolution of the particle size and density along pyrolysis and to validate a drag coefficient correlation for the particle residence time calculation. The optical measurements show that at the end of pyrolysis there is a decrease of particle density of 70 – 80% and of particle size of 25 – 40%. It is also proven that the particle slip velocity cannot be neglected and that the change of these particle properties must be taken into account for the calculation of the particle slip velocity and residence time. Finally, based on these experimental results, a 1D shrinking-core model is developed that is able to predict the solid/gas/tar yields and the residence time of a single particle along pyrolysis in the drop tube reactor. It is validated on both the pyrolysis and optical experiments. The model sensitivity analysis shows that even for millimetric particles, the accurate knowledge of the heat of pyrolysis, of the wood density and of the char thermal conductivity is essential

Les gaz d'atomes ultrafroids offrent des possibilités sans précédent pour la réalisation et la manipulation des systèmes quantiques. Le contrôle exercé sur les interactions entre particules permet d'atteindre le régime de fortes interactions, pour des espèces d'atomes à la fois fermioniques et bosoniques. Dans la limite unitaire, où la force d'interaction est à son maximum, des propriétés universelles émergent. Pour les atomes bosoniques, celles-ci comprennent l'effet Efimov, l'existance surprenante d'une séquence infinie d'états liés à trois corps. Dans cette thèse, nous avons étudiés un système de bosons unitaires. Partant des cas à deux et à trois corps, nous avons montrés que le modèle choisi capturait correctement les caractéristiques universelles de l'effet Efimov. Pour le modèle à N-corps, nous avons développé un algorithme de Monte Carlo quantique capable de réaliser les différentes phases thermodynamiques du système : gaz normal à haute-température, condensat de Bose-Einstein, et liquide d'Efimov. Un unique composant de notre modèle resterait pertinent à la limite de température infinie, à savoir la répulsion corps dur à trois corps, qui constitue une généralisation du potentiel classique entre sphères dures. Pour ce modèle, nous avons proposé une solution au problème d'empilement compact en deux et trois dimensions, fondée sur une Ansatz analytique et sur la technique de recuit simulé. En étendant ces résultats à une situation de pression finie, nous avons montré que le système présente une transition de fusion discontinue, que nous avons identifié à travers la méthode de Monte Carlo. / Ultracold atomic gases offer unprecedented possibilities to realize and manipulate quantum systems. The control on interparticle interactions allows to reach the strongly-interacting regime, with both fermionic and bosonic atomic species. In the unitary limit, where the interaction strength is at its maximum, universal properties emerge. For bosonic atoms, these include the Efimov effect, the surprising existence of an infinite sequence of three-body bound states. In this thesis, we have studied a system of unitary bosons. Starting from the two- and three-body cases, we have shown that the chosen model correctly captures the universal features of the Efimov effect. For the corresponding many-body problem, we have developed a quantum Monte Carlo algorithm capable of realizing the different thermodynamic phases in which the system may exist: The high-temperature normal gas, Bose-Einstein condensate, and Efimov liquid. A single ingredient of our model would remain relevant in the infinite-temperature limit, namely the three-body hard-core repulsion, which constitutes a generalization of the classical hard-sphere potential. For this model, we have proposed a solution to the two- and three-dimensional packing problem, based on an analytical ansatz and on the simulated-annealing technique. Extending these results to finite pressure showed that the system has a discontinuous melting transition, which we identified through the Monte Carlo method.