Cette thèse porte sur l'analyse statique de code par typage dans le but de détecter les erreurs dans les programmes avant leur exécution. Plus précisément, nous nous intéressons ici au domaine du sous-typage, dans lequel les propriétés du code sont représentées par des ensemble de contraintes de la forme (t1 <= t2). Nos mécanismes de vérification sont alors basés sur l'agrégation de contraintes de sous-typage et la vérification de leur compatibilité par saturation. Le langage de base sur lequel nous travaillons est un ML étendu, muni de variants et d'un mécanisme de filtrage de motifs. Nous commençons par définir un formalisme nous permettant d'exprimer nos systèmes de types sous forme de règles d'inférences. Ce formalisme présente l'avantage d'être suffisamment souple pour nous permettre de prouver les propriétés de validité et de terminaison de nos systèmes, et suffisamment précis pour nous permettre d'en dériver une implémentation de manière systématique. Après avoir défini un système de types de base pour notre langage, nous en présentons trois extensions originales : * Une amélioration du typage du filtrage de motifs basée en particulier sur l'ajout d'un opérateur de disjonction entre les contraintes de sous-typage. Cet opérateur permet alors d'exprimer, pour chaque cas de filtrage, le lien entre le filtre et les contraintes extraites du typage de l'expression correspondante. Ceci nous permet en particulier de représenter beaucoup plus finement le type de certaines fonctions et ainsi d'accepter plus de programmes valides. * Une alternative au mécanisme classique de généralisation permettant de distinguer les contraintes associées aux différents usages des paramètres des fonctions. Un tel mécanisme rend en particulier la construction de langage "let" de ML obsolète. Mixé avec la première extension, nous obtenons un système permettant d'encoder dans le langage lui même (c'est à dire sans ajouter de construction supplémentaire), un modèle objet intéressant. * Une formalisation des GADT basée sur une implantation originale des variables de type existentielles. En plus d'être compatible avec le sous-typage, cette variante des GADT présente une amélioration notable par rapport aux GADT standards par le fait qu'elle étend les possibilités d'inférence. Les annotations de type, habituellement obligatoires en présence de GADT, deviennent ici presque toutes facultatives. Bien qu'il soit possible de dériver directement une implémentation de ces systèmes, ce qui est principalement utile pour leur compréhension et leur prototypage, les performances des typeurs obtenus de la sorte ne sont pas suffisantes pour analyser des programmes de taille réelle. Ceci est principalement dû aux différentes extensions que nous apportons au langage des contraintes, en particulier les opérateurs de disjonction et de négation. Nous présentons alors les différentes techniques que nous avons mises en place pour l'implémentation de nos systèmes permettant à nos analyses de passer à l'échelle en pratique. / This PHD thesis focuses on static analysis of programs by type inference in order to detect program errors before their execution. More precisely, we focus hear in the field of sub-typing, where program properties are described by sets of constraints of the form (t1 <= t2). Our verification mechanisms are based on the aggregation of sub-typing constraints and checking of their compatibility by saturation. The base language on which we define our type systems is an ML-like language provided with variants and pattern matching. We starts by defining a formalism to express our type systems thanks to inference rules. This formalism has the advantage to be sufficiently flexible to allow proving validity and termination properties of our systems, and sufficiently precise to allow a systematic derivation of our inference rules into a runnable typer. After the definition of a base type system for our language, we present three novel extensions: * An improvement of type inference for the pattern matching based on the addition of the "or" operator between sub-typing constraints. This operator allow to express a link, in each cases of a match, between the pattern and the constraints generated at typing time of the case expression. This allows us to refine the type of some functions, and then to accept more valid programs. * A new implementation of the generalization mechanism. This allows to distinguish constraints associated to the different occurrences of a function parameter in its body. Thanks to this mechanism, the "let" construction from ML is in particular obsolete. By mixing this extension with the first one, we obtain a type system able to encode "objects" without any additional language construction. * A formalization of GADT based on an novel implementation of existential type variables. In addition to be compatible with the sub-typing context of this thesis, this alternative to GADT has the advantage to improve type inference. As a consequence, most of type annotations, usually required in the presence of GADT, are now optional. Despite the fact that it is possible to directly derive an implementation of our type systems from their rules, that is principally interesting for their comprehension and prototyping, the effectiveness of such typer is insufficient to analyze real world programs. This is principally due to the extensions we provide to the language of constraints, and in particular to the "or" and "not" operators. At then end, we present multiple techniques we used in our implementation to extend the scalability of our analysis.

Québec Université Laval, Bibliothèque 2015

« Thèse présentée à l'École des gradués de l'Université Laval pour l'obtention du grade de philosophiæ doctor (Ph. D.) » / « Ayant mis en évidence les faiblesses analytiques de la dynamique des systèmes, notre recherche se préoccupera d'abord de modifier le modèle de dynamique des système pour pouvoir exploiter les outils puissants du Contrôle Automatique. Comme nous le verrons, cette modification consistera à procéder à une approximation linéaire du modèle initial de dynamique des systèmes qui est non linéaire. Dans cet effort, nous éviterons la méthode de transformation utilisée par les tenants du Contrôle Automatique (Appiah et Coyle 1983, Mohpatra et Sharma 1983) ; elle nous éloigne de ce qui est le langage par excellence de la dynamique des systèmes: DYNAMO; et surtout, elle est impuissante devant les modèles de grande taille. Nous partirons des principes de linéarisation, pour y procéder directement avec DYNAMO (on y arriverait avec n'importe quelle version de DYNAMO) sans recourir comme N. B. Forrester à un logiciel supplémentaire, DYNASTAT ou autre. Après avoir mis au point un instrument de linéarisation, la thèse montrera comment les gestionnaires peuvent recourir à l'analyse modale pour comprendre la nature et l'ampleur des forces dynamiques présentes au sein de leur entreprise. Pour cela, elle s'appuyera sur la correspondance existant entre la stabilité intrinsèque d'un système et les valeurs propres de son modèle linéaire. En troisième lieu, la thèse fournira une procédure de modification des forces dynamiques pour stabiliser et ajuster les divers secteurs de l'entreprise. La stabilisation consiste à identifier et changer les politiques qui causent l'instabilité. L'ajustement n'intervient qu'après la stabilisation; il consiste à identifier et à renforcer les politiques qui augmentent la stabilité. Basée sur les valeurs propres et l'analyse de leur sensibilité, cette procédure se révélera être un excellent moyen de mettre en évidence les effets réels des politiques suivies dans l'entreprise et d'évaluer l'opportunité de renforcer, atténuer ou éliminer ces politiques par des mesures appropriées. Enfin, elle donne une méthode d'implantation, dans le réel, des suggestions issues de l'analyse modale. L'application sera faite sur le modèle bien connu de Lyneis. Cela permettra d'identifier les sous-systèmes constitutifs du modèle global: leur nature, leur taille et leur mode d'interaction. Le degré d'intégration des différents secteurs de l'entreprise telle que modélisée par Lyneis apparaîtra avec plus de netteté. Nous nous servirons de la procédure développée dans cette thèse pour dégager les mesures et transformations nécessaires à la stabilisation accrue de chaque secteur. Il en résultera une meilleure performance. »--Pages 10-12

Québec Université Laval, Bibliothèque 2015

Le cours d'un professeur donné à des étudiants se sépare en général en deux parties distinctes, la première consiste en la transmission des connaissances, et ensuite vient un dialogue entre les deux parties afin de répondre aux questions des étudiants et de les faire progresser. La phase d'échange est très importante, car elle permet aux élèves de mieux appréhender les notions qu'ils viennent d'apprendre. Elle demande cependant une grande implication du professeur pour répondre aux questions de chaque étudiant. À l'inverse, la phase de transmission des connaissances est souvent une élocution du professeur plutôt qu'une interaction avec les élèves. De plus, cette transmission est répétitive d'une année à l'autre, et certaines notions basiques pourraient être apprises d'une autre manière afin que l'enseignant puisse se concentrer davantage sur l'échange avec ses étudiants. À l'image de la médecine personnalisée, une médecine qui se base sur les caractéristiques génétiques et moléculaires du patient afin de lui proposer un traitement plus efficace, nous proposons dans ce mémoire de réfléchir à une méthode permettant d'adapter et d'automatiser la phase de transmission des connaissances à chaque étudiant. Plutôt que d'énoncer le même cours à tous les élèves, ou de donner le même médicament à tous les patients, nous souhaitons utiliser les antécédents de l'étudiant en vue de lui proposer une version personnalisée du cours adaptée à ses besoins, ce qui lui permettrait d'apprendre plus facilement. L'automatisation de cette tâche permettrait en plus de libérer du temps au professeur pour d'autres tâches. Nous allons nous concentrer dans ce mémoire sur l'apprentissage d'un langage de programmation tel que le Python. Nous allons réfléchir à une démarche permettant d'automatiser et de personnaliser son apprentissage. Pour ce faire, nous allons travailler sur la génération de code Python à partir d'une description en langage naturel afin de créer automatiquement des exercices. Cette génération permet de recommander automatiquement des exercices adaptés aux élèves. Nous allons utiliser les avancées en intelligence artificielle afin de simuler l'intelligence d'un professeur pour adapter au mieux le programme à chaque étudiant. / A teacher's lecture to students is usually divided into two distinct parts, the first of which consists of the transmission of knowledge, followed by a dialogue between the two parties in order to answer the students' questions and help them progress. The exchange phase is very important, as it allows the students to better understand the concepts they have just learnt. However, it requires a great deal of involvement on the part of the teacher to answer each student's questions. In contrast, the knowledge transmission phase is often a speech by the teacher rather than an interaction with the students. Moreover, this transmission is repetitive from one year to the next, and some basic notions could be learnt in another way so that the teacher can concentrate more on the exchange with his students. In the image of personalised medicine, a medicine that is based on the genetic and molecular characteristics of the patient in order to propose a more effective treatment, we propose in this manuscript to think about a method that would allow us to adapt and automate the phase of knowledge transmission to each student. Rather than giving the same lecture to all students, or the same drug to all patients, we want to use the student's background to provide a personalised version of the lecture that is tailored to their needs, making it easier for them to learn. The automation of this task would also free up the teacher's time for other tasks. In this manuscript, we will focus on the learning of a programming language such as Python. We will think about an approach that allows us to automate and personalise its learning. To do this, we will work on the generation of Python code from a natural language description in order to automatically create exercises. This generation allows us to automatically recommend exercises adapted to the students. We will use advances in artificial intelligence to simulate the intelligence of a teacher to best adapt the programme to each student.

La dynamique actuelle des marchés entraîne avec elle une complexité croissante des demandes du client et nécessairement des contraintes de production. Les méthodologies traditionnelles de conception de systèmes montrent leurs limites dans des contextes très changeants pour lesquels les spécifications sont amenées à évoluer rapidement, des éléments technologiques particuliers de réalisation étant souvent pris en compte trop tôt dans le travail d'étude, limitant la versabilité des développements. Les entreprises doivent alors capitaliser au maximum les efforts menés dans les phases amont de spécification pour optimiser les temps d'étude. Notre travail de recherche s'intéresse plus précisément au domaine des systèmes antomatisés et se propose de répondre à la problématique précédente en utilisant des techniques issues du monde de l'informatique pour la réalisation des sytèmes physiques, comme l'OOA (Approche Orienté Objet) et la modélisation objet UML (Langage de Modélisation Unifié) avec la perspective d'une spécialisation tardive et d'une génération automatique selon les cibles technologiques choisies, comme le préconise la logique IDM (Ingéniérie Dirigée par les Modèles). L'originalité de ce mémoire est de décrire une méthodologie et une organisation de travail pour la conception des systèmes automatisés, en s'appuyant sur le concept d'objet d'automatisme multi-facettes. De plus, nous proposons une utilisation de l'extension SysML (Langage de Modélisation des Systèmes) pour la représentation d'éléments d'automatismes particuliers, les blocs fonctions de la norme IEC 61131-3, à travers le stéréotype "block". Enfin nous montrons comment il est possible d'obtenir une première génération de code automate en passant par les spécifications PLCopen, définissant un lien entre une syntaxe XML (Langage de balisage eXtensible), se voulant standard, et les langages de la norme IEC 61131-3. Le passage par cette représentation standardisée permet de garder l'indépendance des implémentations vis-à-vis d'un environnement intégré de développement particulier. Le processus de conception décrit a été appliqué à un cas d'étude industriel réel appartenant au domaine de la palettisation robotisée.

L'évaluation des systèmes répartis est habituellement fondée sur des critères numériques relatifs à la quantité d'information échangée au cours des calculs. Nous montrons que ces critères ne sont pas suffisants pour évaluer le degré de répartition des algorithmes répartis usuels. Des critères qualitatifs, spécifiques de la répartition, sont nécessaires.<br /><br />La modularité exprime que les processeurs du système n'ont initialement aucune connaissance concernant globalement le réseau dans lequel ils sont plongés. La symétrie exprime que les processeurs avec des positions topologiquement équivalentes dans le réseau ont aussi des rôles équivalents dans les calculs.<br /><br />Nous définissons ces propriétés dans le cadre du langage CSP des processus séquentiels communicants de Hoare. Nous proposons une définition syntaxique pour la modularité. Nous montrons qu'une définition syntaxique de la symétrie n'est pas suffisante. Nous en proposons une définition sémantique. Cette définition se réfère implicitement à une sémantique partiellement ordonnée de CSP. <br /><br />Nous étudions l'existence d'algorithmes de diffusion et d'élection dans les réseaux de processus communicants, qui soient modulaires et symétriques. Nous obtenons de nombreux résultats positifs et négatifs. Ceci conduit en particulier à une évaluation précise du pouvoir expressif de CSP. Nous montrons par exemple qu'il n'existe pas d'implantation des gardes d'émission par des gardes de réception seulement, si la symétrie doit être préservée.<br /><br />Ces résultats sont enfin utilisés pour proposer une solution modulaire, symétrique et bornée au problème de la détection de la terminaison répartie proposé par Francez.

Le développement d'applications informatiques passe souvent par l'utilisation de langages évolués pour la programmation et de systèmes d'exploitation pour la gestion de l'exécution. Une famille de langages de programmation (les LPC pour "langages à parallélisme Compilé") peuvent procurer les même fonctionnalités et avantages qu'un langage de programmation couplé à un système d'exploitation multi-tâches. Notre intention est de montrer que les LPC ont certains attraits supplémentaires surtout dans le domaine d'application qu'est l'informatique industrielle. Pour mettre ceci en évidence, nous avons développé plusieurs versions d'une même application en utilisant d'une part un LPC et, d'autre part, un langage évolué classique avec un système d'exploitation. Ensuite, nous avons fait une comparaison chiffrée des différentes versions.

Reproduction de : Thèse de doctorat : Systèmes industriels : Toulouse, INPT : 2007. / Titre provenant de l'écran-titre. Bibliogr. 111 réf.

La construction de logiciels pour des appareils qui ne peuvent pas accueillir localement des outils de développement peut être difficile. Ces appareils soit ont une puissance de calcul trop limitée pour exécuter un IDE (par exemple, smartphones), ou manquent d' interfaces d'entrée / sortie appropriées (écran, clavier , souris) pour la programmation (par exemple, les robots mobiles) ou sont tout simplement inaccessibles pour des développements locaux (par exemple cloud - serveurs). Dans ces situations, les développeurs ont besoin d'une infrastructure appropriée pour développer et déboguer des applications distantes. Des solutions de débogage à distance sont parfois délicates à utiliser en raison de leur nature distribuée. Les études empiriques nous montrent que, en moyenne 10,5 minutes par heure de codage (plus de cinq semaines de travail de 40 heures par an) sont passées pour le re-déploiement d'applications pour corriger les bugs ou améliorer leur fonctionnalité [ZeroTurnAround 2011]. En plus, les solutions courantes manquent des aménagements qui seraient autrement disponibles dans un contexte local, car c'est difficile de les reproduire à distance (par exemple débogage objet-centré [Ressia 2012b]). Cet état influe sur la quantité d' expérimentation au cours d'une session de débogage à distance - par rapport à un contexte local. Dans cette thèse, afin de surmonter ces problèmes, nous identifions d'abord quatre propriétés désirables qu'une solution idéale pour le débogage à distance doit présenter : l'interactivité, l'instrumentation, la distribution et la sécurité. L'interactivité est la capacité d'une solution de débogage à distance de mise à jour incrémentale de toutes les parties d'une application sans perdre le contexte de d'exécution (sans arrêter l'application). L'instrumentation est l'aptitude d'une solution de modifier la sémantique d'un processus en cours en vue d'aider le débogage. La distribution est la capacité d'une solution de débogage à adapter son cadre alors que le débogage d'une cible à distance. Enfin la sécurité fait référence à la disponibilité de conditions préalables pour l'authentification et la restriction d'accès. Compte tenu de ces propriétés, nous proposons Mercury, un modèle de débogage à distance et une architecture pour des langues réflexifs à objets. Mercury ouvre (1) l'interactivité grâce à un méta-niveau à distance miroir basé sur un lien de causalité avec sa cible, (2) l'instrumentation à travers une intercession réflective basée sur la réification de l'environnement d'exécution sous-jacent, (3) la distribution grâce à un middleware adaptable et (4) la sécurité par la décomposition et l'authentification de l'accès aux aspects réflexifs. Nous validons notre proposition à travers un prototype dans le langage de programmation Pharo à l'aide d'un cadre expérimental diversifié de multiples dispositifs contraints. Nous illustrons des techniques de débogage à distance supportées par les propriétés de Mercury, tels que le débogage agile distant et l'instrumentation objet à distance et montrons comment ils peuvent résoudre dans la pratique, les problèmes que nous avons identifiés.