Дисертації з теми "Assistant logiciel"
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Ознайомтеся з топ-50 дисертацій для дослідження на тему "Assistant logiciel".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Переглядайте дисертації для різних дисциплін та оформлюйте правильно вашу бібліографію.
BIENVENU, OLIVIER. "Conception d'un assistant pour un logiciel d'elements finis dedie aux calculs de champs electromagnetiques." Paris 6, 1998. http://www.theses.fr/1998PA066033.
Повний текст джерелаZimmermann, Théo. "Challenges in the collaborative evolution of a proof language and its ecosystem." Thesis, Université de Paris (2019-....), 2019. http://www.theses.fr/2019UNIP7163.
Повний текст джерелаIn this thesis, I present the application of software engineering methods and knowledge to the development, maintenance, and evolution of Coq —an interactive proof assistant based on type theory— and its package ecosystem. Coq has been developed at Inria since 1984, but has only more recently seen a surge in its user base, which leads to much stronger concerns about its maintainability, and the involvement of external contributors in the evolution of both Coq, and its ecosystem of plugins and libraries.Recent years have seen important changes in the development processes of Coq, of which I have been a witness and an actor (adoption of GitHub as a development platform, first for its pull request mechanism, then for its bug tracker, adoption of continuous integration, switch to shorter release cycles, increased involvement of external contributors in the open source development and maintenance process). The contributions of this thesis include a historical description of these changes, the refinement of existing processes, and the design of new ones, the design and implementation of new tools to help the application of these processes, and the validation of these changes through rigorous empirical evaluation.Involving external contributors is also very useful at the level of the package ecosystem. This thesis additionally contains an analysis of package distribution methods, and a focus on the problem of the long-term maintenance of single-maintainer packages
Savary-Leblanc, Maxime. "Augmenting software engineers with modeling assistants." Thesis, Université de Lille (2018-2021), 2021. https://pepite-depot.univ-lille.fr/LIBRE/EDMADIS/2021/2021LILUB027.pdf.
Повний текст джерелаDomain knowledge is a prerequisite to produce software design and implementation tailored to stakeholders’ requirements. One common way to formalize that knowledge is achieved through conceptual models, which are commonly used to describe or simulate a system. Acquiring such expertise requires to discuss with knowledgeable stakeholders and/or to get an access to useful documents, which both might not always be easily accessible. In the same time, more and more model samples can be gathered from multiple sources, what represents an increasing number of already formalized and accessible knowledge pieces. For example, some companies keep archives of internal model repositories. There also exist numerous open source projects that contain models while some modeling tools even offer the possibility to create public projects that are free to browse. Such data sources could be exploited to create domain knowledge that could be provided to software engineers while modeling. To be useful, this knowledge must be of high quality, but must also be well integrated into the software modeling process. The focus of this thesis is to provide a framework to exploit knowledge to assist users of computer-based modeling tools with software modeling assistants. This thesis first introduces our research questions based on a systematic mapping study about software assistants for software engineering, and then focuses on software assistants for modeling. It reports on the design of modeling assistants based on a user-centered approach. We present the conclusions of interviews conducted with experts in modeling, a stage in which requirements are collected. Then, we develop the creation of a prototype modeling knowledge base allowing (i) to create general and specific artificial modeling knowledge, and (ii) to make them available to any software client via recommendations. After introducing the results of an experiment regarding the accuracy of the system, we discuss these preliminary results. Finally, this thesis presents a software modeling assistant implementation integrated to the Papyrus tool, which aims to cognify the UML modeling environment by integrating the previously created knowledge. Our work helps to clarify the need for assistance during software modeling work, presents an initial approach to the design of software assistants for software modeling, and identify research challenges in modeling assistance
Delépine, Ludovic. "L'assistance à la navigation hyperdocumentaire : un assistant logiciel d'aide à la recherche de documents visités par un lecteur dans le contexte du Web : une approche sémio-technologique." Dijon, 2003. http://www.theses.fr/2003DIJOS009.
Повний текст джерелаFilou, Vincent. "Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq." Thesis, Bordeaux 1, 2012. http://www.theses.fr/2012BOR14708/document.
Повний текст джерелаThe goal of this work is to build a framework allowing the study, in aformal setting, of the correctness of local computations systems aswell as the expressivity of this model. A local computation system isa set of graph relabelling rules with limited scope, corresponding to a class of distributed algorithms.Our first contribution is the formalisation, in the Coq proofassistant, of a relationnal semantic for local computation systems.This work is based on an original formal graph theory for Coq.Ambiguities inherent to a "pen and paper" definition of local computations are corrected, and we prove that our definition captures all sub-classes of relabelling relations studied in the remainder. We propose a draft of a proof methodology for local computation systems in Coq. Our second contribution is the study of the expressivity of classes of local computations inside our framework. We provide,for instance, a formal proof of D. Angluin results on election and graph coverings. We propose original "meta-theorems" concerningthe LC0 class of local computation, and use these theorem to produce formal impossibility proofs.Finally we study possible transformations of local computation systemsand of their proofs. To this end, we adapt the notion of ForwardSimulation, originally formulated by N. Lynch, to localcomputations. We use this notion to define certified transformationsof LC0 systems. We show how those certified transformation can be useto study the expressivity of certain class of algorithm in ourframework. We define, as certified transformation, two notions ofcomposition for LC0 systems.A Coq library of ~ 50000 lines of code, containing the formal proofs of the theorems presented in the thesis has been produced in collaboration with Pierre Castéran
Lelay, Catherine. "Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée." Thesis, Paris 11, 2015. http://www.theses.fr/2015PA112096/document.
Повний текст джерелаReal analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, the definitions of integrals and derivatives are based on dependent types, which make them cumbersome to use in practice. This thesis first describes various state-of-the-art libraries available in proof assistants. To palliate the inadequacies of the Coq standard library, we have designed a user-friendly formalization of real analysis: Coquelicot. An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals and asymptotic behaviors. Moreover, an algebraic hierarchy makes it possible to apply some of the theorems in a more generic setting, such as complex numbers or matrices. Coquelicot is a conservative extension of the classical analysis of Coq's standard library and we provide correspondence theorems between the two formalizations. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation
Nemouchi, Yakoub. "Model-based Testing of Operating System-Level Security Mechanisms." Thesis, Université Paris-Saclay (ComUE), 2016. http://www.theses.fr/2016SACLS061/document.
Повний текст джерелаFormal methods can be understood as the art of applying mathematical reasoningto the modeling, analysis and verification of computer systems. Three mainverification approaches can be distinguished: verification based on deductive proofs,model checking and model-based testing.Model-based testing, in particular in its radical form of theorem proving-based testingcite{brucker.ea:2012},bridges seamlessly the gap between the theory, the formal model, and the implementationof a system. Actually,theorem proving based testing techniques offer a possibility to directly interactwith "real" systems: via differentformal properties, tests can be derived and executed on the system under test.Suitably supported, the entire process can fully automated.The purpose of this thesis is to create a model-based sequence testing environmentfor both sequential and concurrent programs. First a generic testing theory basedon monads is presented, which is independent of any concrete program or computersystem. It turns out that it is still expressive enough to cover all common systembehaviours and testing concepts. In particular, we consider here: sequential executions,concurrent executions, synchronised executions, executions with abort.On the conceptual side, it brings notions like test refinements,abstract test cases, concrete test cases,test oracles, test scenarios, test data, test drivers, conformance relations andcoverage criteria into one theoretical and practical framework.In this framework, both behavioural refinement rules and symbolic executionrules are developed for the generic case and then refined and used for specificcomplex systems. As an application, we will instantiate our framework by an existingsequential model of a microprocessor called VAMP developed during the Verisoft-Project.For the concurrent case, we will use our framework to model and test the IPC API of areal industrial operating system called PikeOS.Our framework is implemented in Isabelle/HOL. Thus, our approach directly benefitsfrom the existing models, tools, and formal proofs in this system
Guettala, Abdelheq Et-Tahir. "VizAssist : un assistant utilisateur pour le choix et le paramétrage des méthodes de fouille visuelle de données." Thesis, Tours, 2013. http://www.theses.fr/2013TOUR4017/document.
Повний текст джерелаIn this thesis, we deal with the problem of automating the process of choosing an appropriate visualization and its parameters in the context of visual data mining. To solve this problem, we developed a user assistant "VizAssist" which mainly assist users (experts and novices) during the process of exploration and analysis of their dataset. We illustrate the approach used by VizAssit to help users in the visualization selection and parameterization process. VizAssist proposes a process based on two steps. In the first step, VizAssist collects the user’s objectives and the description of his dataset, and then proposes a subset of candidate visualizations to represent them. In this step, VizAssist suggests a different mapping between the database for representation and the set of visualizations it manages. The second step allows user to adjust the different mappings suggested by the system. In this step, VizAssist uses an interactive genetic algorithm to allow users to visually evaluate and adjust such mappings. We present finally the results that we have obtained during the user evaluation that we performed and the contributions of our tool to accomplish some tasks of data mining
Braun, David. "Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective." Thesis, Strasbourg, 2019. http://www.theses.fr/2019STRAD020.
Повний текст джерелаThis thesis work is part of the general field of computer-assisted proof and is methodologically based. The primary objective of proof assistants is to verify that handwritten demonstration is correct; the question here is how within such a system, it is possible to help a user to make a formal proof of the result in which he is interested. These questions around the verification of proofs, in particular in software certification, and beyond their traceability and readability have indeed become significant with the importance that algorithms have taken on in our society. Obviously, answering the question of proof assistance in all its generality goes far beyond the scope of this thesis. This is why we focus our work on proof in mathematics in a particular framework that is well known in our team: geometry and its formalization in the Coq system. In this field, we first highlight the levels at which we can work, namely the scientific context through the formalization methods but also the methodological and technical context within the Coq proof assistant. In a second step, we try to show how our methods and ideas can be generalized to other disciplines. In this way, we are putting in place the first steps towards effective proof assistance in a simple but omnipresent geometric context. Through a classical approach based on synthetic geometry and a complementary combinatorial approach using the concept of rank from matroid theory, we provide the user with general principles and tools to facilitate the development of formal proof. In this sense, we compare the automation capabilities of these two approaches in the specific context of finite geometries before finally constructing an automatic prover of geometric configurations of incidence
Boudissa, Mehdi. "Réduction virtuelle des fractures complexes du bassin à l'aide du premier simulateur biomécanique patient-spécifique Computer-assisted surgery in acetabular fractures: Virtual reduction of acetabular fracture using the first patient-specific biomechanical model simulator Computer Assisted Surgery in Preoperative Planning of Acetabular Fracture Surgery: State of the Art." Thesis, Université Grenoble Alpes (ComUE), 2019. http://www.theses.fr/2019GREAS038.
Повний текст джерелаL’objectif de cette thèse est de développer et valider une nouvelle méthode de planification pré-opératoire en chirurgie traumatique de l’acetabulum reposant sur un modèle biomécanique patient-spécifique. La première partie de ce travail a consisté en l’élaboration et l’amélioration progressive de ce nouvel outil de planification. La première étape était de générer des modèles tri-dimensionnels de plusieurs fractures acétabulaires à l’aide d’une méthode de segmentation semi-automatique. Dans le même temps, nous avons démontré que les fragments osseux segmentés pouvaient être utile pour classer correctement les fractures acétabulaires par des internes non expérimentés. La seconde étape était de générer un modèle biomécanique patient-spécifique, le plus simplement possible pour pouvoir être compatible avec une pratique clinique régulière. Une revue de la littérature à propos des différentes méthodes de planifications péri-opératoire en traumatologie de l’acetabulum a été réalisée afin d’identifier qu’un nouveau paradigme était nécessaire du fait des limites des méthodes existantes. Une fois les objectifs d’une modélisation biomécanique patient-spécifique définis, une revue de la littérature des différents modèles biomécanique de la hanche a été réalisée pour définir les propriétés biomécaniques des différents éléments à modéliser. Un compromis entre simplicité et comportement réaliste du modèle a été trouvé pour générer un modèle biomécanique patient-spécifique, dans un temps limité, compatible avec une utilisation courante en pratique clinique. Des études cliniques portant sur 14 cas de fractures acétabulaires opérées, puis 29 et finalement 39 cas ont été réalisées pour valider rétrospectivement les simulations biomécaniques. Les résultats montraient une parfaite adéquation avec la réalité. Seuls des logiciels en libre accès, avec leurs faiblesses, étaient utilisés car la fiabilité et la validité de la simulation étaient nécessaires avant d’envisager plus d’investissements. La preuve de concept était donnée. Enfin, une étude clinique prospective a démontré l’efficacité de la simulation biomécanique patient-spécifique et sa faisabilité en pratique clinique quotidienne. Ce travail ouvre la porte à de nouvelles approches en matière de planification chirurgicale et de modélisation patient-spécifique
Jourdan, Jacques-Henri. "Verasco : a Formally Verified C Static Analyzer." Sorbonne Paris Cité, 2016. http://www.theses.fr/2016USPCC021.
Повний текст джерелаIn order to develop safer software for critical applications, some static analyzers aim at establishing, with mathematical certitude, the absence of some classes of bug in the input program. A possible limit to this approach is the possibility of a soundness bug in the static analyzer itself, which would nullify the guarantees it is supposed to deliver. In this thesis, we propose to establish formal guarantees on the static analyzer itself: we present the design, implementation and proof of soundness using Coq of Verasco, a formally verified static analyzer based on abstract interpretation handling most of the ISO C99 language, including IEEE754 floating-point arithmetic (except recursion and dynamic memory allocation). Verasco aims at establishing the absence of erroneous behavior of the given programs. It enjoys a modular extendable architecture with several abstract domains and well-specified interfaces. We present the abstract iterator of Verasco, its handling of bounded machine arithmetic, its interval abstract domain, its symbolic abstract domain and its abstract domain of octagons. Verasco led to the development of new techniques for implementing data structure with sharing in Coq
Husson, Adrien. "Logical foundations of a modelling assistant for molecular biology." Thesis, Université de Paris (2019-....), 2019. http://www.theses.fr/2019UNIP7116.
Повний текст джерелаThis thesis addresses the issue of “Executable Knowledge Representation” in the context of molecular biology. We introduce the foundation of a logical framework, termed iota, whose aim is to facilitate knowledge collation of molecular interactions at the level of proteins and at the same time allows the modeler to “compile” a reasonable fragment of the logic into a finite set of executable graph rewriting rules. We define a logic FO[↓] over cell state transitions. States represent cell contents; domain elements are protein parts and relations are protein-protein bindings. The unary logical operator ↓ selects transitions where as little as possible happens. Formulas over transitions also denote runs, which are finite or infinite sequences of transitions. Every transition formula is moreover associated to a set of rewriting rules equipped with an operational semantics. We introduce two deductive systems that act as “typing” for formulas. We show that if a formula is typable in the first system then the execution of its associated rule set produces exactly the runs denoted by the formula, and that if it is typable in the second system then its associated rule set is finite. We introduce a grammar that produces formulas typable in both systems, up to logical equivalence. Finally we study decidability and definability properties of fragments of FO[↓]. In particular, we show that formulas typable in the second system are in a tight fragment of FO,which implies that the operator ↓ can then be eliminated
Canals, Gérôme. "Des mécanismes pour l'assistance aux utilisateurs dans un atelier de génie logiciel conduit par des modèles." Nancy 1, 1992. http://www.theses.fr/1992NAN10170.
Повний текст джерелаCherifi, Nadir. "Assistance au développement de logiciels embarqués contraints en énergie." Thesis, Lille 1, 2018. http://www.theses.fr/2018LIL1I036/document.
Повний текст джерелаThe designation under the term Internet of Things brings together a vast array of different connected systems.A significant number of these objects do not have a continuous power supply and are therefore supplied with batteries. In addition, we can list multiple use cases where the recharging of the battery is difficult or impossible (e.g. a buried object for structures monitoring). As a result, the energetic aspect represents a primary constraint to be taken into account by the developers when designing the embedded application on the object. The work issue consists in placing energy as a hard resource during the development phase by providing assistance and help to the developers in the management of this complex resource. We propose as a solution a methodology and tools to support the activities of the embedded developer in a constrained energy environment. We assert that the ability to accurately measure and track the energy consumption of a connected object and then correlate it to the underlying software can improve overall energy efficiency by implementing best practices related to use of the different hardware components. To achieve this goal, we base our work on a hardware energy measurement method able of providing accurate consumption figures. We than build an energy profiling and cartography framework of embedded software to help the developer understand the energy behavior of his application
Khammaci, Tahar. "Contribution à l'étude du processus de développement de logiciels : assistance à base de connaissance et modélisation des objets logiciels." Nancy 1, 1991. http://www.theses.fr/1991NAN10287.
Повний текст джерелаGallois-Wong, Diane. "Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie." Electronic Thesis or Diss., université Paris-Saclay, 2021. http://www.theses.fr/2021UPASG016.
Повний текст джерелаDigital filters have numerous applications, from telecommunications to aerospace. To be used in practice, a filter needs to be implemented using finite precision (floating- or fixed-point arithmetic). Resulting rounding errors may become especially problematic in embedded systems: tight time, space, and energy constraints mean that we often need to cut into the precision of computations, in order to improve their efficiency. Moreover, digital filter programs are strongly iterative: rounding errors may propagate and accumulate through many successive iterations. As some of the application domains are critical, I study rounding errors in digital filter algorithms using formal methods to provide stronger guaranties. More specifically, I use Coq, a proof assistant that ensures the correctness of this numerical behavior analysis. I aim at providing certified error bounds over the difference between outputs from an implemented filter (computed using finite precision) and from the original model filter (theoretically defined with exact operations). Another goal is to guarantee that no catastrophic behavior (such as unexpected overflows) will occur. Using Coq, I define linear time-invariant (LTI) digital filters in time domain. I formalize a universal form called SIF: any LTI filter algorithm may be expressed as a SIF while retaining its numerical behavior. I then prove the error filters theorem and the Worst-Case Peak Gain theorem. These two theorems allow us to analyze the numerical behavior of the filter described by a given SIF. This analysis also involves the sum-of-products algorithm used during the computation of the filter. Therefore, I formalize several sum-of-products algorithms, that offer various trade-offs between output precision and computation speed. This includes a new algorithm whose output is correctly rounded-to-nearest. I also formalize modular overflows, and prove that one of the previous sum-of-products algorithms remains correct even when such overflows are taken into account
GHISONI, BONNET ISABELLE. "Creation d'un logiciel de dietetique au centre hospitalier regional de nice, diet assistance." Nice, 1988. http://www.theses.fr/1988NICE6011.
Повний текст джерелаBenali, Khalid. "Assistance et pilotage dans le développement de logiciel : Vers un modèle de description." Nancy 1, 1989. http://www.theses.fr/1989NAN10382.
Повний текст джерелаZid, Talel. "Conception d' un atelier logiciel d' assistance à l' ingénierie du besoin en intelligence économique." Toulouse 1, 2002. http://www.theses.fr/2002TOU10030.
Повний текст джерелаThis research focuses on a proposal which integrates a set of models and a méta-model for the specification and the development of a software tool. This software tool is dedicated to the aid to the definition and analysis of the decision-makers requirements in competitive intelligence. The software tool aids also to the definition and prototyping of business competitive products
Cadavid, Gómez Juan José. "Assistance à la méta-modélisation précise." Rennes 1, 2012. http://www.theses.fr/2012REN1S089.
Повний текст джерелаDomain-specific modeling languages (DSMLs) promise increased productivity for modeling software-intensive systems. Still, the definition of a language that correctly captures the domain knowledge remains difficult. The definition of a metamodel that precisely captures a domain is challenging. Two majors obstacles arise: First, a metamodel is a description of the possibly infinite set of all conforming models. However, there is currently no systematic method to test that a metamodel captures all the correct models of the domain and no more. Second, domain experts who want to build a metamodel must master two different languages: an object-oriented model for the domain structure (MOF) and first order logic (OCL) to define well-formedness rules. We observe that most metamodels have only an object-oriented domain structure, leading to inaccurate metamodels. For the first obstacle, we argue that providing the expert with a qualified set of test data will allow him to ensure that it only captures correct models. We focus on the automatic selection of a test-adequate set of models in the modeling space captured by a metamodel. For the second obstacle, we perform an empirical study to analyze the state of practice in 33 metamodels that actually use MOF and OCL. We notice that there is a set of frequent OCL expressions, which resulted in a catalog of 20 patterns of MOF-OCL, used to suggest rules for an input metamodel, which the expert validates with a selected set of test models. We perform further refinement to rules by using genetic programming. We have thus a complete global approach to tackle the main two obstacles for assisting precise metamodeling
Chen, Kejia. "Contribution à la conception de la mémoire d'un agent assistant personnel." Compiègne, 2008. http://www.theses.fr/2008COMP1774.
Повний текст джерелаThe thesis concerns the structuration of a memory for personal assistant (PA) agents. This work is realized in the process of developing a genric model of PA agent. After studying the issues in this area, we plan to build a PA agent with memory, named MemoPA agent. This agent behaves in a more effective way, allowing to better understand the user and help the user. Having examined several cognitive memory models, we propose to organize the memory of PA agents in the form of MOP (Memory Organization Packets) and then build a memory mechanism inspired by the idea of Cased-Based Reasoning. A prototype of MemoPA agent was developed and implemented in our multi-agents plateform. In addition to the structuration of memory, we also produced a mechanism to update the knowledge base during the memory process, a mechanism of using cases to resolve new problems, a policy of identifying pronominal references in the conversation. Through several experiments in the prototype, we conclude that the MemoPA agent showed some wisdow in relation to the PA agent without memory. With a memory, the resolving process of the user tasks can be improved, some errors in this process can be avoided and the user statements may be better understood
Patto, Vincius Sebba. "Utilisation d'agents assistants pour l'analyse et la prise de décision pour la gestion participative." Paris 6, 2010. http://www.theses.fr/2010PA066093.
Повний текст джерелаHabhouba, Dounia. "Assistance à la prise de decision dans le processus de modification d'un produit en utilisant la technologie "Agent logiciel"." Thèse, Université de Sherbrooke, 2008. http://savoirs.usherbrooke.ca/handle/11143/1826.
Повний текст джерелаVidal, Jean-Philippe Dartus Denis Moisan Sabine Faure Jean-Baptiste. "Assistance au calage de modèles numériques en hydraulique fluviale apports de l'intelligence artificielle /." Toulouse : INP Toulouse, 2005. http://ethesis.inp-toulouse.fr/archive/00000116.
Повний текст джерелаTibermacine, Chouki. "Contractualisation de l'évolution architecturale de logiciels à base de composants : Une approche pour la préservation de la qualité." Phd thesis, Université de Bretagne Sud, 2006. http://tel.archives-ouvertes.fr/tel-00512361.
Повний текст джерелаUllah, Sehat. "Multi-modal assistance for collaborative 3D interaction : study and analysis of performance in collaborative work." Thesis, Evry-Val d'Essonne, 2011. http://www.theses.fr/2011EVRY0003.
Повний текст джерелаThe recent advancement in the field oh high quality computer graphics and the capability of inexpensive computers to render realistic 3D scenes have made it possible to develop virtual environments where two more users can co-exist and work collaboratively to achieve a common goal. Such environments are called Collaborative Virtual Environnment (CVEs). The potential application domains of CVEs are many, such as military, medical, assembling, computer aided designing, teleoperation, education, games and social networks etc.. One of the problems related to CVEs is the user's low level of awareness about the status, actions and intentions of his/her collaborator, which not only reduces user's performance but also leads to non satisfactory results. In addition, collaborative tasks without using any proper computer generated assistance are very difficult to perform and are more prone to errors. The basic theme of this thesis is to provide assistance in collaborative 3D interactiion in CVEs. In this context, we study and develop the concept of multimodal (audio, visual and haptic) assistance of a user or group of users. Our study focuses on how we can assist users to collaboratively interact with the entities of CVEs. We propose here to study and analyze the contribution of multimodal assistance in collaborative (synchronous and asynchronous) interaction with objects in the virtual environment. Indeed, we propose and implement various multimodal virtual guides. Theses guides are evaluated through a series of experiments where selection/manipulation task is carried out by users both in synchronous and asynchronous mode. The experiments were carried out in LISA (Laboratoire d'Ingénierie et Systèmes Automatisés) lat at University of Angers and IBISC (Informatique, Biologie Intégrative et Systèmes complexes) lab at University of Evry. In these experiments users were asked to perform a task under various conditions (with and without guides). Analysis was done on the basis of task completion time, errors and users' learning. For subjective evaluations questionnaires were used. The findings of this research work can contribute to the development of collaborative systems for teleopreation, assembly tasks, e-learning, rehabilitation, computer aided design and entertainment
Hajjam, El Hassani Amir. "Iac++ : un environnement interactif de programmation orientée objet dirigée par une assistance intelligente pour la réutilisation de composants logiciels." Mulhouse, 1990. http://www.theses.fr/1990MULH0154.
Повний текст джерелаMaroneze, André Oliveira. "Certified Compilation and Worst-Case Execution Time Estimation." Thesis, Rennes 1, 2014. http://www.theses.fr/2014REN1S030/document.
Повний текст джерелаSafety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods - built upon solid mathematical bases - to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant - a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence. In this thesis, we apply formal methods to obtain safe Worst-Case Execution Time (WCET) estimations for C programs. The WCET is an important property related to the safety of critical systems, but its estimation requires sophisticated techniques. To guarantee the absence of errors during WCET estimation, we have formally verified a WCET estimation technique based on the combination of two main methods: a loop bound estimation and the WCET estimation via the Implicit Path Enumeration Technique (IPET). The loop bound estimation itself is decomposed in three steps: a program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage. Each stage has a chapter dedicated to its formal verification. The entire development has been integrated into the formally verified C compiler CompCert. We prove that the final estimation is correct and we evaluate its performances on a set of reference benchmarks. The contributions of this thesis include (a) the formalization of the techniques used to estimate the WCET, (b) the estimation tool itself (obtained from the formalization), and (c) the experimental evaluation. We conclude that our formally verified development obtains interesting results in terms of precision, but it requires special precautions to ensure the proof effort remains manageable. The parallel development of specifications and proofs is essential to this end. Future works include the formalization of hardware cost models, as well as the development of more sophisticated analyses to improve the precision of the estimated WCET
Nelson, Mark J. "Representing and reasoning about videogame mechanics for automated design support." Diss., Georgia Institute of Technology, 2015. http://hdl.handle.net/1853/53875.
Повний текст джерелаFuckner, Márcio. "A personal assistant for the enactment of business processes." Thesis, Compiègne, 2016. http://www.theses.fr/2016COMP2270/document.
Повний текст джерелаOver the last few years, the advances in management science and information technology have transformed the business process management (BPM) discipline into an important topic for both industry and academy. BPM uses business processes as the means for improving the operational performance of organizations, and setting processes are at the heart of BPM allows linking together people, systems, and different organizations to deliver value to stakeholders. The target of our work is the family of BPM systems. A BPM system is a generic software system that is driven by explicit process designs to enact and manage operational business processes. Despite the wide range of topics addressed by the academy on business processes, there are still aspects not addressed by prior research. A particular problem in this regard is the mediation between BPM systems and humans. Human interaction in those systems follows a standard user interface based predominantly on work item lists and forms. Thus, there is little room for creativity for users. They have not only difficulties in enacting their processes but also for searching the most suitable one for their needs. It would be more efficient to let humans interact in natural language. However, process modeling languages are an insufficient means of capturing and representing the domain of discourse. The present thesis develops an original approach to agent dialog management for the problem of business process enactment. The overarching motivation for this work was to design a dialog model scalable to different domains. The model relies on domain and business process ontologies, and necessitates a minimum effort of adaptation on ontologies to improve the interaction. Results indicate the potential of our agent-based approach to generate natural language
Auvinet, Jean-Marie. "Interprétation, interactions et connaissances : artefacts et assistance aux opérateurs radio des salles d'information et de commandement." Paris 1, 2005. http://www.theses.fr/2005PA010009.
Повний текст джерелаBoutillier, Pierre. "De nouveaux outils pour calculer avec des inductifs en Coq." Phd thesis, Université Paris-Diderot - Paris VII, 2014. http://tel.archives-ouvertes.fr/tel-01054723.
Повний текст джерелаChinaei, Hamid Reza. "Learning Dialogue POMDP Model Components from Expert Dialogues." Thesis, Université Laval, 2013. http://www.theses.ulaval.ca/2013/29690/29690.pdf.
Повний текст джерелаSpoken dialogue systems should realize the user intentions and maintain a natural and efficient dialogue with users. This is however a difficult task as spoken language is naturally ambiguous and uncertain, and further the automatic speech recognition (ASR) output is noisy. In addition, the human user may change his intention during the interaction with the machine. To tackle this difficult task, the partially observable Markov decision process (POMDP) framework has been applied in dialogue systems as a formal framework to represent uncertainty explicitly while supporting automated policy solving. In this context, estimating the dialogue POMDP model components is a signifficant challenge as they have a direct impact on the optimized dialogue POMDP policy. This thesis proposes methods for learning dialogue POMDP model components using noisy and unannotated dialogues. Speciffically, we introduce techniques to learn the set of possible user intentions from dialogues, use them as the dialogue POMDP states, and learn a maximum likelihood POMDP transition model from data. Since it is crucial to reduce the observation state size, we then propose two observation models: the keyword model and the intention model. Using these two models, the number of observations is reduced signifficantly while the POMDP performance remains high particularly in the intention POMDP. In addition to these model components, POMDPs also require a reward function. So, we propose new algorithms for learning the POMDP reward model from dialogues based on inverse reinforcement learning (IRL). In particular, we propose the POMDP-IRL-BT algorithm (BT for belief transition) that works on the belief states available in the dialogues. This algorithm learns the reward model by estimating a belief transition model, similar to MDP (Markov decision process) transition models. Ultimately, we apply the proposed methods on a healthcare domain and learn a dialogue POMDP essentially from real unannotated and noisy dialogues.
Benayoun, Vincent. "Analyse de dépendances ML pour les évaluateurs de logiciels critiques." Phd thesis, Conservatoire national des arts et metiers - CNAM, 2014. http://tel.archives-ouvertes.fr/tel-01062785.
Повний текст джерелаFafiotte, Georges. "Multiprototypage d'un logiciel d'aide à la découverte de connaissances lexicales : cacao, environnement d'apprentissage assisté par ordinateur des caractères chinois." Université Joseph Fourier (Grenoble), 1994. http://www.theses.fr/1994GRE10024.
Повний текст джерелаUllah, Sehat. "Assistance multimodale pour l'interaction 3D collaborative : étude et analyse des performances pour le travail collaboratif." Phd thesis, Université d'Evry-Val d'Essonne, 2011. http://tel.archives-ouvertes.fr/tel-00562081.
Повний текст джерелаLeloup, Jérôme. "Le projet HM2PH, habitat modulaire et mobile pour personnes handicapées : spécification d'un espace de vie adapté pour personne en déficit d'autonomie." Tours, 2004. http://www.theses.fr/2004TOUR4055.
Повний текст джерелаAccording to the last statistics, the number of person with reduced mobility is constantly increasing. One of the main problems about this popultation is to find the best way to enable them to live at home as long as possible. The aim of the HM2PH project (in french Habitat Modulaire et Mobile pour Personnes Handicapées) is to specify the functionalities of a smart adapted and mobile living area that will give more autonomy to the resident by using specific devices (assistive technology, home automation. . . ). Moreover, this living area should be able to fit in a strongly medicalized facility as well as n a familial environment. In order to realise such a house, it'es necessary to ask for several professional skills (architect, doctors, occupational therapists. . . ), which leads to huge conception times and costs. To reduce this, we propose a software tool to help the creation of an adapted living area. Composed by three modules, this tool enables to first analyse the feficiencies and capabilities of the future resident and gives a list of several specific devices (assistive technologies, home automation devices. . . ) to use in order to compensate his eventual disabilities. Then it generates a set of layouts that are automatically created according to architecturales rules (classical rules and those linked to the disability) and to the resident's preferences. Finally the last module enable to visit at real time a 3D model of the layouts generated previously, in order to test and assess the different proposed and installed devices. The evolution of this project and much information about disability, assistive technology, networks and new technologies are available on the internet at http://www. Hant. Li. Univ-tours. Fr/webhant/HM2PH
Vidal, Jean-Philippe. "Assistance au calage de modèles numériques en hydraulique fluviale - Apports de l'intelligence artificielle." Phd thesis, Institut National Polytechnique de Toulouse - INPT, 2005. http://tel.archives-ouvertes.fr/tel-00010185.
Повний текст джерелаLy, Kim Quyen. "Automated verification of termination certificates." Thesis, Grenoble, 2014. http://www.theses.fr/2014GRENM036/document.
Повний текст джерелаMaking sure that a computer program behaves as expected, especially in critical applications (health, transport, energy, communications, etc.), is more and more important, all the more so since computer programs become more and more ubiquitous and essential to the functioning of modern societies. But how to check that a program behaves as expected, in particular when the range of its inputs is very large or potentially infinite? In this work, we explain the development of a new, faster and formally proved version of Rainbow based on the extraction mechanism of Coq. The previous version of Rainbow verified a CPF le in two steps. First, it used a non-certified OCaml program to translate a CPF file into a Coq script, using the Coq libraries on rewriting theory and termination CoLoR and Coccinelle. Second, it called Coq to check the correctness of the script. This approach is interesting for it provides a way to reuse in Coq termination proofs generated by external tools. This is also the approach followed by CiME3. However, it suffers from a number of deficiencies. First, because in Coq functions are interpreted, computation is much slower than with programs written in a standard programming language and compiled into binary code. Second, because the translation from CPF to Coq is not certified, it may contain errors and either lead to the rejection of valid certificates, or to the acceptance of wrong certificates. To solve the latter problem, one needs to define and formally prove the correctness of a function checking whether a certificate is valid or not. To solve the former problem, one needs to compile this function to binary code. The present work shows how to solve these two problems by using the proof assistant Coq and its extraction mechanism to the programming language OCaml. Indeed, data structures and functions de fined in Coq can be translated to OCaml and then compiled to binary code by using the OCaml compiler. A similar approach was first initiated in CeTA using the Isabelle proof assistant
Sun, Yudong. "Résolution de problèmes dans l'espace d'états avec abstraction de concepts : Le système oasis." Nancy 1, 1989. http://www.theses.fr/1989NAN10089.
Повний текст джерелаHerms, Paolo. "Certification of a Tool Chain for Deductive Program Verification." Phd thesis, Université Paris Sud - Paris XI, 2013. http://tel.archives-ouvertes.fr/tel-00789543.
Повний текст джерелаDelouette, Ilona. "Une analyse d’économie institutionnaliste du financement de la prise en charge de la dépendance : D’un risque social à un risque positif." Thesis, Lille 1, 2020. http://www.theses.fr/2020LIL1A002.
Повний текст джерелаThis doctoral dissertation focuses on the funding of care for elderly dependent persons in France. “Dependency” was not considered as a specific social protection issue until the Arreckz report (1979) in which emerges the idea of creating a 5th social security risk. However, care has always been the subject of overlapping schemes designed independently of social security. These schemes have always proved insufficient to cover social needs. We carry out an institutionalist political economy analysis rooted in the Régulation Theory, and more specifically in B. Théret's approach of national systems of social protection. The care of dependency is understood as a sub-system of social protection, i.e. as a means of reproduction of the economic, political, and domestic spheres which are supported by a shared symbolism. In order to understand the evolutions of the dependency’s funding system, we study the changes of this symbolism and the power relations that influence it. Within this symbolism we are specifically interested in the increasing use of the category of risk and insurance. This category widely used in the field of dependency is also at the core of the symbolism of French social protection. Our research is based on the analysis of observations made by think-tanks concerning the funding of dependency; on semi-directive interviews of “key” players in the field; and on a linguistic and historical analysis of public reports using the software Prospéro (Doxa). We demonstrate that since 1979, dependency has been understood as a social risk (1979-1997), then as a social protection risk (1997-2007), and finally as a predictable and positive risk (2008-2015). Within the symbolism of social protection, the category of risk and insurance is increasingly embedded in managerial and economic discourse. These changes justify the transition from funding defined within the primary share of the value added to funding relying on secondary redistribution. Thus, although the risk category has been used constantly since the 1970s, it does not justify the funding of the field commensurate with the stakes involved. On the contrary, since the 2000s onwards, in view of the power relations prevailing in the field, the category of risk has justified the privatisation of its funding
Ginon, Blandine. "Modèles et outils génériques pour mettre en place des systèmes d’assistance épiphytes." Thesis, Lyon, INSA, 2014. http://www.theses.fr/2014ISAL0080/document.
Повний текст джерелаThis thesis in computer science is situated more particulary in the field of knowledge engineering. It concerns the a posteriori setup of assistance systems in existing applications, while having a generic approach. In order to setup the setup of assistance systems in existing applications without a need to redevelop it or to access its source code, we choose to have a fully epiphytic approach. We proposed a adjunction process of an assistance system to a target-application with a epiphytic manner. It is constituted of two phases: the specification and the execution of the assistance. The assistance specification phase enables an expert, the assistance designer, to represent his knowledge relative to the target-application and to the assistance that he wishes to setup. The assistance execution phase uses this knowledge to provide the target-application end-users with the assistance wished by the designer. To make possible on the one hand the assistance specification by an assistance designer potentially non-computer scientist, and one the second hand the automatic execution of the specified assistance, we propose a pivot language: aLDEAS. This graphical language makes possible the definition of very varied assistance systems, with the shape of a set of rules. Our theoretical propositions have been implemented through the SEPIA system, constituted of different tools. The SEPIA assistance editor is aimed at assistance designers, and it implemented the assistance specification phase. It provided the assistance designers with an interface to handle aLDEAS elements in order to define assistance rules. These rules can then be executed by the SEPIA generic assistance engine, which implements the assistance execution phase. It provides the target-application end-users with the specified assistance. For this purpose, the assistance engine manages different epiphytic tools, in order to monitor and inspect the target-application, and to perform the assistance actions. The models implemented through the SEPIA system are generic, but it make possible the setup of assistance systems specifically suited on the one hand to their target-application, and on the second hand to the end-users
Jomaa, Narjes. "Le co-design d’un noyau de système d’exploitation et de sa preuve formelle d’isolation." Thesis, Lille 1, 2018. http://www.theses.fr/2018LIL1I075/document.
Повний текст джерелаIn this thesis we propose a new kernel concept adapted to verification that we have called protokernel. It is a minimal operating system kernel where the minimization of its size is motivated by the reduction of the cost of proof and of the attack surface. This leads us to define a new strategy of codesign of the kernel and its proof. It is based mainly on the feedbacks between the various steps of development of the kernel, ranging from the definition of its specification to the formal verification of its properties. Thus, in this context we have designed and implemented the Pip protokernel. All of its system calls were carefully identified during the design step to ensure both the feasibility of proof and the usability of the system. The code of Pip is written in Gallina (the specification language of the Coq proof assistant) and then automatically translated into C code. The main property studied in this work is a security property, expressed in terms of memory isolation. This property has been largely discussed in the literature due to its importance. Thus, our work consists more particularly in guiding the developer to define the fundamental concepts of this minimalistic kernel through the formal verification of its isolation property. The verification strategy was first experimented with a generic microkernel model that we also wrote in Gallina. With this simplified microkernel model we were able to validate our verification approach before applying it to the concrete implementation of the Pip protokernel
Saunier, Camille, and Camille Saunier. "La protection des données personnelles des utilisateurs d'enceintes connectées «intelligentes» par le Règlement européen no 2016/679, le droit canadien et le droit québécois : approche comparatiste." Master's thesis, Université Laval, 2020. http://hdl.handle.net/20.500.11794/38291.
Повний текст джерелаLe présent travail de recherche porte sur la protection des renseignements personnels des utilisateurs d’enceintes connectées « intelligentes ». Au regard de cet objet connecté particulier, l’étude se penchera sur la manière dont la protection des données personnelles est envisagée par le Règlement européen n°2016/679 (RGPD), la Loi sur la protection des renseignements personnels et les documents électroniques (LPRPDE) et la Loi québécoise sur la protection des renseignements personnels dans le secteur privé (LPRPSP) tout au long du cycle de vie de la donnée. Ces différentes législations divergent tant sur leurs dates d’adoption que sur leurs systèmes juridiques. Pourtant, les rapports de faits qui les animent en font une des objets de comparaison particulièrement intéressants. Il ressort de cette étude que l’enceinte connectée « intelligente » met en évidence les insuffisances des législations étudiées vis-à-vis du rapport au temps, de la masse de données collectées mais aussi de l’opacité de la machine.
BENMANSOUR-BEKHTI, FATIMA. "Interfacage d'un potentiostat avec un micro-ordinateur en vue de la mesure des impedances electrochimiques." Université Louis Pasteur (Strasbourg) (1971-2008), 1989. http://www.theses.fr/1989STR13076.
Повний текст джерелаRozot, Roger. "Facteurs électroniques et reconnaissance de formes en CAO de molécules pharmacologiquement actives : application à la famille des benzodiazépines." Nancy 1, 1988. http://www.theses.fr/1988NAN10215.
Повний текст джерелаBernard, Christophe. "Vers une gestion informatisée des cahiers de laboratoire : Le système "MANIP"." Nancy 1, 1989. http://www.theses.fr/1989NAN10006.
Повний текст джерелаMille, Alain. "Raisonnement basé sur l'expérience pour coopérer à la prise de décision : un nouveau paradigme en supervision industrielle." Saint-Etienne, 1995. http://www.theses.fr/1995STET4016.
Повний текст джерелаLasson, Marc. "Réalisabilité et paramétricité dans les systèmes de types purs." Phd thesis, Ecole normale supérieure de lyon - ENS LYON, 2012. http://tel.archives-ouvertes.fr/tel-00770669.
Повний текст джерела