Since the advent of the Internet, we have been observing a fast-paced development within the computing world. One of the major innovations in recent years is the “Internet of Things”, which brings interconnectedness between devices and humans to unprecedented heights. This technological breakthrough enabled the emergence of a new sub-field within Learning Analytics, Multimodal Learning Analytics, which makes use of several types of data sources to study learning-related processes. As computers and sensors become increasingly cheaper and more accessible,  research within this new sub-field grows, yet some gaps remain unexplored. Additionally, there is a research bias toward computer-assisted learning environments, rather than physical ones. At the same time, the current labor market is highly competitive, and possessing profession-related skills is not sufficient to land a job. Besides these skills, there is an increasing demand for social skills, such as communication, teamwork, and collaboration. However, there is a gap between the skills that are trained in an academic setting and the ones that are required by the labor market. Having this background in mind, this work aims at designing and evaluating an IoT sensor system capable of tracking patterns observed under social interactions within a group, and more specifically, in terms of the distance between group members while solving a task. Another important aspect of this study is the system's cost-effectiveness so that it can be employed in a scalable and sustainable manner. To achieve this goal, a multimethodological approach for Design Science Research was adopted, which implied the combination of several methods such as sketching, prototyping, and testing. As a result, this study contributes both to the research area of Multimodal Learning Analytics, and to educational practices.

<p>U ovoj tezi razvijen je formalni sistem za dokazivanje teorema<br />incidencije u projektivnoj geometiji. Osnova sistema je Čeva/Menelaj<br />metod za dokazivanje teorema incidencije. Formalizacija o kojoj je<br />ovdje riječ izvedena je korišćenjem &Delta;-kompleksa, pa su tako u<br />disertaciji spojene oblasti logike, geometrije i algebarske<br />topologije. Aksiomatski sekventi proizilaze iz 2-ciklova &Delta;-kompleksa.<br />Definisana je Euklidska i projektivna interpretacija sekvenata i<br />dokazana je saglasnost i odlučivost sistema. Dati su primjeri<br />iščitavanja teorema incidencije iz dokazivih sekvenata sistema. U<br />tezi je data i procedura za provjeru da li je skup od n šestorki tačaka<br />aksiomatski sekvent.</p> / <p>In this thesis, a formal sequent system for proving incidence theorems in<br />projective geometry is introduced. This system is based on the<br />Ceva/Menelaus method for proving theorems. This formalization is performed<br />using &Delta;-complexes, so the areas of logic, geometry and algebraic topology<br />are combined in the dissertation. The axiomatic sequents of the system stem<br />from 2-cycles of &Delta;-complexes. The Euclidean and projective interpretations of<br />the sequents are defined and the decidability and soundness of the system<br />are proved. Patterns for extracting formulation and proof of the incidence<br />result from derivable sequents of system are exemplified. The procedure for<br />deciding if set of n sextuples represent an axiomatic sequent is presented<br />within the thesis.</p>

Kontextmedvetenhet kan användas i turistguide applikationer för att bidra användare med information och tjänster. Majoriteten av turistguide applikationer utvecklas vanligtvis för utbildnings eller historiska ändamål. Den här studien presenterar en konceptvalidering av den opublicerade ljuvandrings applikationen "SoundTracker", i syfte att förbättra den. Den nya "SoundTracker" prototypen inriktar sig inte på utbildnings eller historiska ändamål, utan den är inriktad på inspelning, uppspelning, och delning av personliga ljudvandringar med vänner och familj. Konceptvalideringen är begränsad av de definierade forskningsfrågorna i den här uppsatsen. Det handlar i korta drag om en förbättring av noggranheten på de inlästa GPS koordinaterna från en användares position, för att förse användaren med en trevlig användarupplevelse. Dessutom är grafiska användargränssnittet av den originala prototypen förbättrat, och testat genom webb enkäter. Vad gäller delnings funktionaliteten, en test applikation är skapad för att hitta essentiella aspekter som behöver tas hänsyn till i den nya "SoundTracker" prototypen när en användare vill dela ett ljudspår med vänner och familj. Test applikationen testas baserat på samlade svar genom en semi strukturerad interview på människor i åldersgruppen 20-30 år.De erhållna resultaten indikerar på att genom användning av Kalman filter, förbättras noggrannheten på användarens position, vilket resulterar i en ljudvandring med mindre avvikelser jämfört med en GPS-sensor. Vad gäller det förbättrade grafiska användargränssnittet, det var enklare för användarna att förstå den förbättrade prototypen såväl som navigera igenom den, än fallet med den originala prototypen. Användarna finner det även intressant när en delningsfunktion implementeras med designen som diskuteras i det här arbetet. / Context-awareness can be used in tour guide applications in order to provide users with information and services. The majority of tour guide applications are usually developed for educational or historical review purposes. This paper presents a proof-of-concept of the unpublished audio tour guide application, “SoundTracker”, with the aim of improving it. The new “SoundTracker” prototype does not aim for educational or historical review purposes, instead it is aimed for recording, listening and sharing personal audio tour guides with friends and family. The proof-of-concept is limited by the defined research questions found in this paper. In summary, the accuracy of the read-in GPS coordinates of a user’s position is enhanced with Kalman filter, to give an enjoyable user experience. Additionally, the graphical user interface of the original prototype is improved and tested through web-surveys. As for the sharing functionality, a test application is created in order to find what necessary aspects need to be considered in the new "SoundTracker" prototype when a user wants to share a sound-walk with friends and family. The test application is tested based on responses obtained through a semi-structured interview from people in the age of 20-30 years.The obtained results indicate that, with use of Kalman filter, the location accuracy of the user is enhanced, which results in a sound-walk with less deviations compared to location accuracy of only GPS-sensor. Regarding the improved graphical user interface, users found the new "SoundTracker" prototype easier to understand, as well as to navigate through it, than the case in the original prototype. Users also find it interesting when a sharing function is implemented with the design that is discussed in this work.

Cette thèse porte sur la notion de certification locale, un sujet central en décision distribuée, un domaine du calcul distribué. Le mécanisme de la décision distribuée consiste, pour les nœuds d'un réseau, à décider de manière distribuée si le réseau est dans une configuration correcte ou non, selon un certain prédicat. Cette décision est dite locale, car les nœuds du réseau ne peuvent communiquer qu'avec leurs voisins. Après avoir communiqué, chaque nœud prend une décision, exprimant si le réseau est correct ou non localement, c'est-à-dire correct étant donné l'information partielle récoltée jusque-là. Le réseau est déclaré correct globalement s'il est déclaré correct localement par tous les nœuds.Du fait de la contrainte de localité, peu de prédicats peuvent être vérifiés de cette manière. La certification locale est un moyen de contourner cette difficulté, et permet de décider tous les prédicats. C'est un mécanisme qui consiste à étiqueter les nœuds du réseau avec ce que l'on appelle des certificats, qui peuvent être vérifiés localement par un algorithme distribué. Un schéma de certification locale est correct si seuls les réseaux dans une configuration correcte peuvent être certifiés. L'idée de la certification locale est non seulement séduisante d'un point de vue théorique, comme une forme de non-déterminisme distribué, mais c'est surtout un concept très utile pour l'étude des algorithmes tolérants aux pannes, où une étape-clé consiste à vérifier l'état du réseau en se basant sur des informations stockées par les nœuds.Cette thèse porte sur quatre aspects de la certification locale : la sensibilité aux erreurs, l'uniformité, la redondance et l'interactivité. L'étude de ces quatre sujets est motivée par une question essentielle : comment réduire les ressources nécessaires à la certification et/ou permettre une meilleure tolérance aux pannes? Pour aborder cette question, il est nécessaire de comprendre le mécanisme de certification en profondeur. Dans cette optique, dans cette thèse, nous apportons des réponses aux questions suivantes. À quel point les certificats doivent-ils être redondants, pour assurer une certification correcte? Les schémas de certification classiques sont-ils robustes à un changement de la condition de correction? Le fait d'introduire de l'interactivité dans le processus change-t-il la complexité de la certification? / This dissertation is about local certification, a central topic in distributed decision, a subfield of distributed computing. The distributed decision mechanism consists, for the nodes of a network, in deciding in a distributed manner whether the network is in a proper configuration or not, with respect to some fixed predicate. This decision is said to be local because the nodes of the network can communicate only with their neighbours. After communication, every node outputs a decision, stating whether the network is locally correct, that is, correct given the partial information gathered so far by this node. The network is declared to be globally correct, if and only if, it is declared to be locally correct by every node.Most predicates cannot be verified by this type of computation, due to the locality constraint. Local certification is a mechanism that enables to circumvent this difficulty, and to check any property. It consists in providing the nodes of the network with labels, called certificates, that can be verified locally by a distributed algorithm. A local certification scheme is correct if only the networks that satisfy the predicate can be certified. In addition to its theoretical appeal, as a form of distributed non-determinism, the concept of local certification is especially relevant in the study of fault-tolerant distributed algorithms, where a key step consists in checking the status of the network, based on information stored at the nodes.This dissertation deals with four aspects of local certification: error-sensitivity, uniformity, redundancy, and interactivity. The study of these four topics is motivated by the same essential question: How to reduce the resources needed for certification, and/or ensure a better fault-tolerance? In order to tackle this question we have to understand fundamental properties of certification. In particular, in this dissertation we answer questions such as: How redundant the certificates need to be for a proper certification? Are the classic certification protocols robust to a strengthening of the acceptance condition? and, How does introducing interactivity in the process changes the complexity of certification?

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.

Les outils d’aide à la preuve basés sur la théorie des types permettent à l’utilisateur d’adopter soit un style fonctionnel, soit un style relationnel (c’est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être préféré parce qu’il permet à l’utilisateur de décrire seulement ce qui est vrai, de s’abstraire temporairement de la question de la terminaison, et de s’en tenir à une description utilisant des règles. Cependant, une spécification relationnelle n’est pas exécutable.Nous proposons un cadre général pour transformer une spécification inductive en une spécification fonctionnelle, en extrayant à partir de la première une fonction et en produisant éventuellement la preuve de correction de la fonction extraite par rapport à sa spécification inductive. De plus, à partir de modes définis par l’utilisateur, qui permettent de considérer les arguments de la relation comme des entrées ou des sorties (de fonction), nous pouvons extraire plusieurs comportements calculatoires à partir d’un seul type inductif.Nous fournissons également deux implantations de notre approche, l’une dans l’outil d’aide à la preuve Coq et l’autre dans l’environnement Focalize. Les deux sont actuellement distribuées avec leurs outils respectifs. / Proof assistants based on type theory allow the user to adopt either a functional style, or a relational style (e.g., by using inductive types). Both styles have advantages and drawbacks. Relational style may be preferred because it allows the user to describe only what is true, discard momentarily the termination question, and stick to a rule-based description. However, a relational specification is usually not executable.We propose a general framework to turn an inductive specification into a functional one, by extracting a function from the former and eventually produce the proof of soundness of the extracted function w.r.t. its inductive specification. In addition, using user-defined modes which label inputs and outputs, we are able to extract several computational contents from a single inductive type.We also provide two implementations of our approach, one in the Coq proof assistant and the other in the Focalize environnement. Both are currently distributed with the respective tools.

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.

L'interleukine-6 (IL-6) exerce des propriétés biologiques multiples telles que l'activation des cellules immunocompétentes, l'activation de la réponse inflammatoire et l'hématopoïèse. Produite également par les cellules tumorales, l'IL-6 impacte la prolifération, la différenciation et la survie de ces dernières. L'IL-6 représente donc depuis plusieurs années une cible thérapeutique pertinente. Dans la première partie de ce travail, nous avons exploré une nouvelle piste potentielle pour bloquer l'activité biologique de l'IL-6, en utilisant un antagoniste naturel que notre équipe a identifié dans plusieurs lignées d'adénocarcinomes du rein, à savoir la molécule tronquée tIL-6. Suite à l'évaluation comparée de deux systèmes d'expression (E. coli versus CHO), nous avons retenu les cellules CHO comme source de production de fractions enrichies en tIL-6 par chromatographie de gel d'exclusion. Disposant d'un panel d'adénocarcinomes de rein (ACHN, Caki1, CLB CHA, CLB VER) et d'une lignée érythroleucémique (TF1), l'activité fonctionnelle de tIL-6 in vitro a été étudiée sur (1) la signalisation IL-6 induite, (2) la prolifération cellulaire IL-6 induite, la survie cellulaire et (4) la modulation de l'expression de protéines relevantes de l'apoptose. La molécule tIL-6 bloque la phosphorylation de la tyrosine Tyr705 de STAT3, qui est un des éléments clés de la voie de signalisation de l'IL-6. Nous rapportons également une autre observation nouvelle indiquant que tIL-6 exerce un effet pro-apoptotique sur certaines lignées RCC. Dans la seconde partie de notre étude, l'impact d'un Ac Mo anti IL-6 dans la réversion de la résistance aux cytotoxiques ou à la radiothérapie a été étudié. Nos résultats démontrent que la voie IL-6 ne constituerait pas un mécanisme majeur de résistance / Interleukin-6 (IL-6) plays numerous physiological roles including haematopoiesis, immune response and inflammation, but also plays a role in modulating cell growth, differentiation and survival of tumors cells. The first goal of the present study was to investigate on the potential role of the truncated protein IL-6 (tIL-6) encoded by the spliced IL-6 mRNA discovered in renal carcinoma cells (RCC). The R&D program was designed based on an industrial approach, aiming at reaching the decision stage to enter or not into preclinical development. Firstly two different expression systems were investigated (E. coli versus CHO cell line). The mammalian expression system was selected as the protein source since a recombinant glycosylated tIL-6 with a molecular weight similar to the predicted natural molecule was obtained from enriched fractions following size exclusion chromatography. Secondly by using a cell line panel including renal carcinoma cells (ACHN, Caki-1, CLB CHA, CLB-VER ) and an erythroleucemic cell line (TF1), in vitro tIL-6 functional activity were analyzed on (1) IL-6 induced signaling, (2) IL-6 induced cell proliferation, (3) on cell survival and also (4) on expression of specific set of proteins involved in apoptosis pathways. The truncated IL-6 was found inhibit IL-6 induced STAT3 Tyr705 and to induce apoptosis in some RCC cell lines which could be depending on IL-6 expression. Understanding more precisely the role of natural truncated IL-6 and its impact in cell tumour growth control will be a major issue in the development of innovative approach to antagonize directly or not IL6. The second goal of the present study was to investigate on reversing resistance of cancer cell lines to cytotoxics or ionizing radiations through the use of a monoclonal antibody directed against IL-6. Our data support the fact that IL-6 is not the preponderant actor of cell resistance to cytotoxics and ionizing radiations, which seems to be regulated by a complex network of proteins

Standards apply the proof of competence method to prove that a design force does not exceed a certain limit to ensure a certain safety level. Furthermore, standards elaborated during the last years apply a cycle-based approach instead of a time-based approach. The shortcomings of the standard ISO 16625:2013 need to be addressed in a revision. Therefore, the working group WG3 of ISO/TC 96 SC3 is preparing a new working draft ISO/WD 16625. This presentation is showing the requirements and objectives.

No description available.