This dissertation investigates current trends concerning exceptions. Exceptions influence the reliability of software systems. In order to develop software systems that are most robust, thus delivering higher availability at a lower development and operating cost, the occurence of exceptions needs to be reduced and the effects of the exceptions controlled. In order to do this, issues such as detection, identification, classification, propagation, handling, language implementation, software testing and reporting of exceptions must be attended to. Although some of these areas are well researched there are remaining problems. The quest is to establish if a unified exception-handling framework is possible and viable, which can address the issues and problems throughout the software development life cycle, and if so, the requirements for such a framework. / Computing / M.Sc. (Information Systems)

Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Ces méthodes sont indispensables pour assurer les plus hauts niveaux de sûreté. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficultés d'ordre pratique et théorique. Les principales difficultés concernent la prise en compte des aspects bas niveau, comme les pointeurs et les interactions avec le matériel spécifique. De plus, le fait que ces systèmes soient concurrents conduit à une augmentation exponentielle du nombre de comportements possibles, ce qui rend plus difficile leur vérification. Dans cette thèse, nous proposons une méthodologie pour la spécification et la vérification par model-checking de ce type de systèmes, en particulier, ceux implémentés en C. Cette méthodologie est basée sur la traduction de la sémantique de C en TLA+, un langage de spécification formel adapté à la modélisation de systèmes concurrents. Nous avons proposé un modèle de mémoire et d'exécution d'un programme C séquentiel en TLA+. En se basant sur ce modèle, nous avons proposé un ensemble de règles de traduction d'un code C en TLA+ que nous avons implémenté dans un outil, appelé C2TLA+. Nous avons montré comment ce modèle peut s'étendre pour modéliser les programmes C concurrents et gérer la synchronisation entre plusieurs processus ainsi que leur ordonnancement. Pour réduire la complexité du model-checking, nous avons proposé une technique permettant de réduire significativement la complexité de la vérification. Cette réduction consiste pour un code C à agglomérer une suite d'instructions lors de la génération du code TLA+, sous réserve d'un ensemble de conditions.Nous avons appliqué la méthodologie proposée dans cette thèse sur un cas d'étude réel issu de l'implémentation d'un micronoyau industriel,sur lequel nous avons vérifié un ensemble de propriétés fonctionnelles. L'application de la réduction a permis de réduire considérablement le temps de la vérification, ce qui la rend utilisable en pratique.Les résultats ont permis d'étudier le comportement du système, de vérifier certaines propriétés et de trouver des bugs indétectables par des simples tests. / Software systems are critical and complex. In order to guarantee their correctness, the use of formal methodsis important. These methods can be defined as mathematically based techniques, languages and tools for specifying and reasoning about systems. But, the application of formal methods to software systems, implemented in C, is challenging due to the presence of pointers, pointer arithmetic andinteraction with hardware. Moreover, software systems are often concurrent, making the verification process infeasible. This work provides a methodology to specify and verify C software systems usingmodel-checking technique. The proposed methodology is based on translating the semantics of Cinto TLA+, a formal specification language for reasoning about concurrent and reactive systems. We define a memory and execution model for a sequential program and a set of translation rules from C to TLA+ that we developed in a tool called C2TLA+. Based on this model, we show that it can be extended to support concurrency, synchronization primitives and process scheduling. Although model-checking is an efficient and automatic technique, it faces the state explosion problem when the system becomes large. To overcome this problem, we propose a state-space reduction technique. The latter is based on agglomerating a set of C instructions during the generation phase of the TLA+ specification. This methodology has been applied to a concrete case study, a microkernel of an industrial real-time operating system, on which a set of functional properties has been verified. The application of the agglomeration technique to the case study shows the usefulness of the proposed technique in reducing the complexity of verification. The obtained results allow us to study the behavior of the system and to find errors undetectable using traditional testing techniques.

La Méthode B est une méthode formelle de spécification et de développement de logiciels critiques largement utilisée dans l'industrie ferroviaire. Elle permet le développement de programmes dit corrects par construction, grâce à une procédure de raffinements successifs d'une spécification abstraite jusqu'à une implantation déterministe du programme. La correction des étapes de raffinement est garantie par la vérification de la correction de formules mathématiques appelées obligations de preuve et exprimées dans la théorie des ensembles de la Méthode B. Les projets industriels utilisant la Méthode B génèrent généralement des milliers d'obligation de preuve. La faisabilité et la rapidité du développement dépendent donc fortement d'outils automatiques pour prouver ces formules mathématiques. Un outil logiciel, appelé Atelier B, spécialement développé pour aider au développement de projet avec la Méthode B, aide les utilisateurs a se décharger des obligations de preuve, automatiquement ou interactivement. Améliorer la vérification automatique des obligations de preuve est donc une tache importante. La solution que nous proposons est d'utiliser Zenon, un outils de déduction automatique pour la logique du premier ordre et qui implémente la méthode des tableaux. La particularité de Zenon est de générer des certificats de preuve, des preuves écrites dans un certain format et qui permettent leur vérification automatique par un outil tiers. La théorie des ensembles de la Méthode B est une théorie des ensembles en logique du premier ordre qui fait appel à des schémas d'axiomes polymorphes. Pour améliorer la preuve automatique avec celle-ci, nous avons étendu l'algorithme de recherche de preuve de Zenon au polymorphisme et à la déduction modulo théorie. Ce nouvel outil, qui constitue le cœur de notre contribution, est appelé Zenon Modulo. L'extension de Zenon au polymorphisme nous a permis de traiter, efficacement et sans encodage, les problèmes utilisant en même temps plusieurs types, par exemple les booléens et les entiers, et des axiomes génériques, tels ceux de la théorie des ensembles de B. La déduction modulo théorie est une extension de la logique du premier ordre à la réécriture des termes et des propositions. Cette méthode est parfaitement adaptée à la recherche de preuve dans les théories axiomatiques puisqu'elle permet de transformer des axiomes en règles de réécriture. Par ce moyen, nous passons d'une recherche de preuve dans des axiomes à du calcul, réduisant ainsi l'explosion combinatoire de la recherche de preuve en présence d'axiomes et compressant la taille des preuves en ne gardant que les étapes intéressantes. La certification des preuves de Zenon Modulo, une autre originalité de nos travaux, est faite à l'aide de Dedukti, un vérificateur universel de preuve qui permet de certifier les preuves provenant de nombreux outils différents, et basé sur la déduction modulo théorie. Ce travail fait parti d'un projet plus large appelé BWare, qui réunit des organismes de recherche académique et des industriels autour de la démonstration automatique d'obligations de preuve dans l'Atelier B. Les partenaires industriels ont fournit à BWare un ensemble d'obligation de preuve venant de vrais projets industriels utilisant la Méthode B, nous permettant ainsi de tester notre outil Zenon Modulo.Les résultats expérimentaux obtenus sur cet ensemble de référence sont particulièrement convaincant puisque Zenon Modulo prouve plus d'obligation de preuve que les outils de déduction automatique de référence au premier ordre. De plus, tous les certificats de preuve produits par Zenon Modulo ont été validés par Dedukti, nous permettant ainsi d'être très confiant dans la correction de notre travail. / The B Method is a formal method heavily used in the railway industry to specify and develop safety-critical software. It allows the development of correct-by-construction programs, thanks to a refinement process from an abstract specification to a deterministic implementation of the program. The soundness of the refinement steps depends on the validity of logical formulas called proof obligations, expressed in a specific typed set theory. Typical industrial projects using the B Method generate thousands of proof obligations, thereby relying on automated tools to discharge as many as possible proof obligations. A specific tool, called Atelier B, designed to implement the B Method and provided with a theorem prover, helps users verify the validity of proof obligations, automatically or interactively. Improving the automated verification of proof obligations is a crucial task for the speed and ease of development. The solution developed in our work is to use Zenon, a first-orderlogic automated theorem prover based on the tableaux method. The particular feature of Zenon is to generate proof certificates, i.e. proof objects that can be verified by external tools. The B Method is based on first-order logic and a specific typed set theory. To improve automated theorem proving in this theory, we extend the proof-search algorithm of Zenon to polymorphism and deduction modulo theory, leading to a new tool called Zenon Modulo which is the main contribution of our work. The extension to polymorphism allows us to deal with problems combining several sorts, like booleans and integers, and generic axioms, like B set theory axioms, without relying on encodings. Deduction modulo theory is an extension of first-order logic with rewriting both on terms and propositions. It is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. This way, we turn proof search among axioms into computations, avoiding unnecessary combinatorial explosion, and reducing the size of proofs by recording only their meaningful steps. To certify Zenon Modulo proofs, we choose to rely on Dedukti, a proof-checker used as a universal backend to verify proofs coming from different theorem provers,and based on deduction modulo theory. This work is part of a larger project called BWare, which gathers academic entities and industrial companies around automated theorem proving for the B Method. These industrial partners provide to BWare a large benchmark of proof obligations coming from real industrial projects using the B Method and allowing us to test our tool Zenon Modulo. The experimental results obtained on this benchmark are particularly conclusive since Zenon Modulo proves more proof obligations than state-of-the-art first-order provers. In addition, all the proof certificates produced by Zenon Modulo on this benchmark are well checked by Dedukti, increasing our confidence in the soundness of our work.

This study investigated the use of ORM as a conceptual modelling technique by using the UML domain model class diagram as benchmark. The rationale was that if the ORM-class diagram compared favourably with the benchmark, then ORM could be proposed as an alternate conceptual modelling technique. Proponents of ORM suggest that it has significant advantages over other techniques for conceptual modelling. The benchmark UML class diagram was developed according to the Unified Process through use-cases and collaboration diagrams. The ORM-class diagram was derived using the Conceptual Schema Design Process and ORM-UML Mapping Process. The evaluation of the two class diagrams was conducted by means of a questionnaire, based on a set of principles for conceptual models. The study concluded that ORM could not be proposed as a conceptual modelling technique up to the UML domain class diagram level without considering additional techniques for capturing the dynamics of the system. / Computer Science / M.Sc. (Computer Science)

Dans le domaine du projet de conception-construction architecturale, la gestion de la collaboration entre les différents acteurs d'un projet est un enjeu important. D'un projet à un autre, en fonction du projet, mais aussi des acteurs qui y interviennent, les pratiques de travail varient. Parallèlement, de nombreux services sont proposés et utilisés pour assister la collaboration, certains sur un modèle « grand public » et d'autres plus orientés vers un usage professionnel. L'expérience CRTI-weB est un projet de développement d'un collecticiel mené avec et pour les professionnels du secteur au Luxembourg. Malgré l'étude des besoins métiers menée en amont du développement, l'outil présente cependant des manques d'adaptation. Ce constat d'inadaptation n'est pas un cas isolé, il reflète une lacune générale de ce genre d'outils à satisfaire pleinement les attentes des professionnels. C'est pourquoi ce travail doctoral propose un cadre d'analyse supporté par la modélisation des comportements des utilisateurs. Nous adoptons alors plusieurs points de vue relatifs à différents champs de recherches : le génie logiciel, la conception d'interfaces homme-machine, l'entreprise orientée services et la conception de système d'information, et enfin le travail collaboratif assisté par ordinateur (TCAO). Nous proposons la méthode PUSH (Practices and Usages based Services enHancement) qui orchestre ces différents points de vue et permet de générer un ensemble d'exigences pour le développement de services dits « adaptés ». Communication et traçabilité sont les maitres mots de cette méthode de conception. Le contexte d'étude à la fois orienté recherche et développement nous a permis d'évaluer et d'améliorer la définition des concepts mis en avant ainsi que la mise en place de la méthode PUSH à travers trois expérimentations / In the sector of the architectural design-construction project, the management of the collaboration between the different actors of a project is an important issue. From a project to another, considering the project type and also the actors involved, business practices vary. In parallel, many services are proposed and used to assist the collaboration, some of them being generic and others more specific to professional usage. The CRTI-weB experience is a groupware development project lead with and for professionals of the Luxembourgish sector. Despite the analysis of business needs lead before development, the tool has some lacks of adaptation. This statement isn't isolated; in general, this type of tools doesn't fully satisfy professionals' expectations. This doctoral work proposes an analysis framework supported by users' behaviors modeling. We adopt several viewpoints related to several research fields: software engineering, human-computer interactions design, service-oriented enterprise and information system design, and finally computer-supported collaborative work (CSCW We propose the PUSH method (Practice and Usages based Service enhancement) that orchestrates the different viewpoints to generate an amount of requirements for the development of adapted services. The communication and the traceability are supported by this design method. The context of study, both research and development-oriented (through the collaboration of the MAP-CRAI laboratory in Nancy and the CRP Henri Tudor in Luxembourg) allows us evaluating and enhancing the definition of our concepts and the applicability of the PUSH method through three experimentations

La compétitivité toujours plus importante et la mondialisation ont mis l'industrie manufacturière au défi de rationaliser les différentes façons de mettre sur le marché de nouveaux produits dans un délai court, avec des prix compétitifs tout en assurant des niveaux de qualité élevés. Le PDP moderne exige simultanément la collaboration de plusieurs groupes de travail qui assurent la création et l’échange d’information avec des points de vue multiples dans et à travers les frontières institutionnelles. Dans ce contexte, des problèmes d’interopérabilité sémantique ont été identifiés en raison de l'hétérogénéité des informations liées à des points de vue différents et leurs relations pour le développement de produits. Le travail présenté dans ce mémoire propose un cadre conceptuel d’interopération pour la conception et la fabrication de produits. Ce cadre est basé sur un ensemble d’ontologies clés, de base d’ingénierie et sur des approches de cartographie sémantique. Le cadre soutient les mécanismes qui permettent la conciliation sémantique en termes de partage, conversion et traduction, tout en améliorant la capacité de partage des connaissances entre les domaines hétérogènes qui doivent interopérer. La recherche a particulièrement porté sur la conception et la fabrication de produits tournants en plastique et explore les points particuliers de la malléabilité - la conception et la fabrication de moules. Un système expérimental a été proposé à l’aide de l'outil Protégé pour modéliser des ontologies de base et d’une plateforme Java intégrée à Jena pour développer l'interface avec l'utilisateur. Le concept et la mise en œuvre de cette recherche ont été testés par des expériences en utilisant des produits tournants en plastiques. Les résultats ont montré que l'information et ses relations rigoureusement définies peuvent assurer l'efficacité de la conception et la fabrication du produit dans un processus de développement de produits moderne et collaboratif / Global competitiveness has challenged manufacturing industry to rationalise different ways of bringing to the market new products in a short lead-time with competitive prices while ensuring higher quality levels. Modern PDP has required simultaneously collaborations of multiple groups, producing and exchanging information from multi-perspectives within and across institutional boundaries. However, it has been identified semantic interoperability issues in view of the information heterogeneity from multiple perspectives and their relationships across product development. This research proposes a conceptual framework of an Interoperable Product Design and Manufacturing based on a set of core ontological foundations and semantic mapping approaches. This framework has been particularly instantiated for the design and manufacturing of plastic injection moulded rotational products and has explored the particular viewpoints of moldability, mould design and manufacturing. The research approach explored particular information structures to support Design and Manufacture application. Subsequently, the relationships between these information structures have been investigated and the semantics reconciliation has been designed through mechanisms to convert, share and translate information from the multi-perspectives. An experimental system has been performed using the Protégé tool to model the core ontologies and the Java platform integrated with the Jena to develop the interface with the user. The conceptual framework proposed in this research has been tested through experiments using rotational plastic products. Therefore, this research has shown that information rigorously-defined and their well-defined relationships can ensure the effectiveness of product design and manufacturing in a modern and collaborative PDP

Η ΒΥΠ διαθέτει αντίτυπο της διατριβής σε έντυπη μορφή στο βιβλιοστάσιο διδακτορικών διατριβών που βρίσκεται στο ισόγειο του κτιρίου της. / Στα πλαίσια της παρούσας Μεταπτυχιακής Διπλωματικής Εργασίας, προτείνουμε (α) μια ταξινόμηση των πιο σημαντικών ερευνητικών αποτελεσμάτων για την επιστημονική περιοχή του Web Engineering και (β) μια μεθοδολογία για την αξιολόγηση εργαλείων για τον ίδιο χώρο τα οποία θα ενσωματωθούν στο WEP (WEB-Engineering Resources Portal). Στην συγκεκριμένη εργασία αναλύονται οι επιστημονικές έννοιες Body of Knowledge(BOK), Software Engineering, Web Engineering, Software Engineering Body of Knowledge (SWEBOK) και γίνεται μια πρώτη προσπάθεια θεμελίωσης ενός Σώματος Γνώσης (Body of Knowledge) για το Web Engineering, που θα εμπεριέχεται στο WEP. Για την ταξινόμηση των ερευνητικών αποτελεσμάτων του WEP βασιστήκαμε στη δομή του SWEBOK (Software Engineering Body of Knowledge), το οποίο αποτελεί μια προσπάθεια της IEEE (Institute of Electrical and Electronics Engineers) για τον καθορισμό και τη μελέτη ενός Σώματος Γνώσης της Επιστήμης Λογισμικού, μια επιστημονική περιοχή που συγγενεύει άμεσα με το Web Engineering. Όσο αφορά την εύρεση και αξιολόγηση εργαλείων για το WEP προτείνουμε έναν αλγόριθμο επιλογής και αξιολόγησης ο οποίος βασίζεται κυρίως στην κατηγοριοποίηση και αξιολόγηση εφαρμογών από τους Ιστότοπους http://www.tucows.com και http://www.download.com, οι οποίοι επιλέχτηκαν βάσει της δημοτικότητά τους και της πληθώρας και καλής οργάνωσης των εργαλείων τους. Τα αποτελέσματα από την εφαρμογή αυτού του αλγορίθμου αξιολόγησης εργαλείων ήταν αρκετά ικανοποιητικά, ενώ υπάρχουν περιθώρια βελτίωσης τόσο με τη χρήση επιπλέον παραμέτρων από τους δύο παραπάνω βασικούς Ιστότοπους όσο και με τη συνεισφορά στοιχείων και από άλλους Ιστότοπους. / In this Master Thesis, we suggest (a) A methodology of classification of the most important research results in Web Engineering (b) A methodology of selection and evaluation web development tools. These tools would be in included in WEP (WEB-Engineering Resources Portal). During this Master Thesis the following definitions are explained: Body of Knowledge (BOK), Software Engineering, Web Engineering, Software Engineering Body of Knowledge (SWEBOK). Moreover, it is suggested a solution of building a “Body of Knowledge” in the field of Web Engineering. This Body of Knowledge would be included in WEP. The basis for the classification of the research results is WEP was the SWEBOK (Software Engineering Body of Knowledge). SWEBOK is an effort of IEEE, in order to establish a baseline for the “Body of Knowledge” for the field of Software Engineering, which is close related with the field of Web Engineering. As far is concerned the selection and evaluation of web development tools, we suggest an algorithm which is based on the classification and evaluation of web development tools by the web sites http://www.tucows.com and http://www.download.com. These web sites have been selected, due to their credibility, popularity and the large number of tools which are presented. Although this algorithm has quite good results, there are some open issues by including more parameters from the 2 main web sites and by investigating other similar web sites, too.

This study investigated the use of ORM as a conceptual modelling technique by using the UML domain model class diagram as benchmark. The rationale was that if the ORM-class diagram compared favourably with the benchmark, then ORM could be proposed as an alternate conceptual modelling technique. Proponents of ORM suggest that it has significant advantages over other techniques for conceptual modelling. The benchmark UML class diagram was developed according to the Unified Process through use-cases and collaboration diagrams. The ORM-class diagram was derived using the Conceptual Schema Design Process and ORM-UML Mapping Process. The evaluation of the two class diagrams was conducted by means of a questionnaire, based on a set of principles for conceptual models. The study concluded that ORM could not be proposed as a conceptual modelling technique up to the UML domain class diagram level without considering additional techniques for capturing the dynamics of the system. / Computer Science / M.Sc. (Computer Science)

Ce travail s’inscrit dans une problématique générale de l’analytique de l’apprentissage numérique et particulièrement dans le contexte du projet ANR HUBBLE, un observatoire national permettant le dépôt de processus d’analyse de haut niveau. Nous nous intéressons principalement à la communication des données d’analyse aux utilisateurs en mettant à leur disposition des tableaux de bord d'apprentissage (TBA). Notre problématique porte sur l’identification de structures génériques dans le but de générer dynamiquement des TBA sur mesure. Ces structures doivent être à la fois génériques et adaptables aux besoins d’utilisateurs. Les travaux existants proposent le plus souvent des TBA trop généraux ou développés de manière adhoc. Au travers du projet HUBBLE, nous souhaitons exploiter les décisions des utilisateurs pour générer dynamiquement des TBA. Nous nous sommes intéressés au domaine de l’informatique décisionnelle en raison de la place des tableaux de bord dans leur processus. La prise de décision exige une compréhension explicite des besoins des utilisateurs. C'est pourquoi nous avons adopté une approche de conception centrée sur l'utilisateur dans le but de lui fournir des TBA adaptés. Nous proposons aussi un processus de capture des besoins qui a permis l’élaboration de nos modèles (indicateur, moyens de visualisation, utilisateur, …). Ces derniers sont utilisés par un processus de génération implémenté dans un prototype de générateur dynamique. Nous avons procédé à une phase d'évaluation itérative dont l’objectif est d'affiner nos modèles et de valider l'efficacité de notre processus de génération ainsi que de démontrer l'impact de la décision sur la génération des TBA. / This work is part of a broader issue of Learning Analytics (LA). It is particularly carried out within the context of the HUBBLE project, a national observatory for the design and sharing of data analysis processes. We are interested in communicating data analysis results to users by providing LA dashboards (LAD). Our main issue is the identification of generic LAD structures in order to generate dynamically tailored LAD. These structures must be generic to ensure their reuse, and adaptable to users’ needs. Existing works proposed LAD which remains too general or developed in an adhoc way. According to the HUBBLE project, we want to use identified decisions of end-users to generate dynamically our LAD. We were interested in the business intelligence area because of the place of dashboards in the decision-making process. Decision-making requires an explicit understanding of user needs. That's why we have adopted a user-centered design (UCD) approach to generate adapted LAD. We propose a new process for capturing end-users’ needs, in order to elaborate some models (Indicator, visualization means, user, pattern, …). These models are used by a generation process implemented in a LAD dynamic generator prototype. We conducted an iterative evaluation phase. The objective is to refine our models and validate the efficiency of our generation process. The second iteration demonstrates the impact of the decision on the LAD generation. Thus, we can confirm that the decision is considered as a central element for the generation of LADs.

Cette thèse présente les résultats d'expérimentations visant à mettre en évidence des mécaniques de jeu utiles pour aider le joueur à développer une posture plus réflexive sur la manière dont il prend une décision. Notre approche consiste à mettre le joueur en défaut en exploitant ses biais de raisonnement, permettant dans un second temps de l’amener à mieux cerner ses processus décisionnels. A ce titre, nous cherchons à placer le joueur en excès de confiance dans le cadre spécifique d'un jeu vidéo. Pour mesurer le comportement, le joueur doit utiliser un outil intégré au déroulement de la partie : un système de mise au travers duquel il renseigne sa confiance en ses chances de succès. Deux jeux spécifiques ont été développés en vue de mesurer l’influence des biais sur la confiance du joueur : un se focalise sur l’influence des biais d’ancrage et de confirmation, l’autre sur l’influence du biais de l'effet difficile / facile d’autre part. / This thesis introduces the results of experiments testing specific game mechanics to help the players to develop reflective decision making. Our approach is, firstly, to bias the players’ judgment. Then, through the bias awareness, we want to help them to have a better understanding about their judgment processes. To do this, we try to place the player in an overconfident state while playing video games. To measure their behavior, the players must use an integrated tool to the game progression: a bet system through which they assess on their confidence in their chances of success. Two games were developed to measure the influence of the biases on the confidence of the player: one focusing on the effect of anchoring and confirmation biases, another one on the hard / easy effect.