Dans le cadre de ce travail de thèse, nous nous sommes intéressés aux relations étroites qu'entretiennent processus moteurs et sensoriels pour déterminer les régions de l'espace où une action directe est possible. Dans ce but, nous nous sommes centrés sur la perception de l' "atteignabilité" d'un objet, c'est-à-dire sur les processus cérébraux qui vont permettre de décider si cet objet pourrait être atteignable ou pas par un mouvement du bras. Pour cela, nous faisons l'hypothèse que ces jugements requièrent la prise en compte de connaissances motrices et corporelles fonctionnelles en plus des informations visuelles extraites de l'environnement. Plus particulièrement, nous proposons qu'ils reposent sur une prédiction des conséquences des actes moteurs potentiels suggérés par cet objet et donc de leur faisabilité à un instant donné. Les études réalisées au cours de cette thèse ont ainsi permis d'écarter l'hypothèse de l'influence de l'effort associé à des actions sur la perception de l'espace atteignable. En revanche, le rôle critique de la prédiction des conséquences sensorimotrices des actions a été mis en évidence, grâce à la démonstration d'une relation forte entre d'une part les correspondances entre la distance visuelle et l'amplitude des mouvements, et d'autre part la distance à laquelle la limite d'atteignabilité est perçue. Les processus d'anticipation sensorimotrice ont également été mis en évidence lors de jugements de perception spatiale en présence de cibles dynamiques, rendant compte du caractère spatio-temporel des mécanismes impliqués. Enfin, une dernière étude a montré l'influence des représentations corporelles et de leur plasticité dans la perception de l'espace péripersonnel, mettant ainsi en lumière l'implication du corps en action dans les jugements perceptifs

Dans le cadre de ce travail de thèse, nous nous sommes intéressés aux relations étroites qu'entretiennent processus moteurs et sensoriels pour déterminer les régions de l'espace où une action directe est possible. Dans ce but, nous nous sommes centrés sur la perception de l' "atteignabilité" d'un objet, c'est-à-dire sur les processus cérébraux qui vont permettre de décider si cet objet pourrait être atteignable ou pas par un mouvement du bras. Pour cela, nous faisons l'hypothèse que ces jugements requièrent la prise en compte de connaissances motrices et corporelles fonctionnelles en plus des informations visuelles extraites de l'environnement. Plus particulièrement, nous proposons qu'ils reposent sur une prédiction des conséquences des actes moteurs potentiels suggérés par cet objet et donc de leur faisabilité à un instant donné. Les études réalisées au cours de cette thèse ont ainsi permis d'écarter l'hypothèse de l'influence de l'effort associé à des actions sur la perception de l'espace atteignable. En revanche, le rôle critique de la prédiction des conséquences sensorimotrices des actions a été mis en évidence, grâce à la démonstration d'une relation forte entre d'une part les correspondances entre la distance visuelle et l'amplitude des mouvements, et d'autre part la distance à laquelle la limite d'atteignabilité est perçue. Les processus d'anticipation sensorimotrice ont également été mis en évidence lors de jugements de perception spatiale en présence de cibles dynamiques, rendant compte du caractère spatio-temporel des mécanismes impliqués. Enfin, une dernière étude a montré l'influence des représentations corporelles et de leur plasticité dans la perception de l'espace péripersonnel, mettant ainsi en lumière l'implication du corps en action dans les jugements perceptifs / In this thesis, we assessed the tight relations between motor and sensory processes used to determine the areas of space in which a direct action is possible. We thus focused on the eprception of the reachability of an object, i.e. on the cerebral processes which allow to decide if an object could be reached or not by moving the arm. To do so, we made the hypothesis that theses judgments require to take into account functional motor and body knowledge, in addition to the visual information extracted from the environment. More specifically, we proposed that these judgments rely on a prediction of the consequences of a potential motor act toward the object, thus on the feasibility of the action at a given moment. Our studies discarded the hypothesis of the role of the effort associated to actions on the perception of reachable space. However, the critical role of predicting the sensorimotor consequences of an action has been showed, by demonstrating the strong relation between on the one hand the correspondence between visual distance and movement amplitude, and on the other hand the distance at which the reachability limit is perceived. Sensorimotor anticipation processes have also been showed in spatial perception involving dynamical targets, showing the spatio-temporal aspect of the involved mechanisms. Finally, our last study showed the influence of body representations and of their plasticity on the perception of peripersonal space, highlighting the implication of the body in action in perceptual judgments

Le pré-dimensionnement se situe en amont du processus de conception d'un système : à partir d'un ensemble d'exigences, il consiste à déterminer un ensemble de solutions techniques possibles dans un espace de recherche souvent très grand et structuré par une connaissance partielle et incertaine du futur système et de son environnement. Bien avant de penser au choix définitif des composants et au dimensionnement précis du système complet, les concepteurs doivent s'appuyer sur un premier cahier des charges, des modélisations des principaux phénomènes et divers retours d'expériences pour formaliser des contraintes, faire des hypothèses simplificatrices, envisager diverses architectures et faire des choix sur des données imprécises (i.e. caractérisées sous la forme d'intervalles, de listes de valeurs possibles, etc…). Les choix effectués lors du pré-dimensionnement pouvant être très lourds de conséquences sur la suite du développement, il est primordial de détecter au plus tôt d'éventuelles incohérences et de pouvoir vérifier la satisfaction des exigences dans un contexte incertain. Dans ce travail, une méthodologie de vérification des exigences basée sur l'échange de modèles ensemblistes entre donneurs d'ordre et fournisseurs est proposée. Elle s'inscrit dans le cadre d'un paradigme de conception basé sur la réduction d'incertitudes. Après un travail portant sur la modélisation des systèmes mécatroniques, une attention particulière est portée à la prise en compte d'incertitudes déterministes sur des grandeurs continues : des techniques basées sur l'analyse par intervalles telles que la satisfaction de contraintes (CSP), des calculs d'atteignabilité pour des modèles dynamiques de connaissances ou encore l'identification de modèles de comportements ensemblistes sont ainsi mis en œuvre et développés afin d'outiller la méthodologie proposée et contribuer à répondre à l'objectif d'une vérification à couverture garantie. / The pre-sizing takes place upstream to the process of designing a system: from a set of requirements, it consists in determining a set of possible technical solutions in an often very large search space which is structured by the uncertain and partial knowledge available about the future system and its environment. Long before making the final choice and the final sizing of the system components, the designers have to use specifications, models of the main phenomena, and experience feedbacks to formalize some constraints, make simplifying assumptions, consider various architectures and make choices based on imprecise data (i.e. intervals, finite sets of possible values, etc…). The choices made during the pre-sizing process often involving strong commitments for the further developments, it is very important to early detect potential inconsistencies and to verify the satisfaction of the requirements in an uncertain context. In this work, a methodology based on the exchange of set-membership models between principals and suppliers is proposed for the verification of requirements. This methodology is fully consistent with a design paradigm based on the reduction of uncertainties. After a work dedicated to the modeling of mechatronic systems, a special attention is paid to dealing with deterministic uncertainties affecting continuous values: some techniques based on interval analysis such as constraint satisfaction (interval CSP), reachability computations for knowledge dynamic models or identification of set-membership behavioral models are used and developed, so providing a set of tools to implement the proposed methodology and contribute to reach the goal of a verification with a full and guaranteed coverage.

Cette thèse est consacrée au calcul des états atteignables des systèmes linéaires et hybrides. La première partie est consacrée aux systèmes linéaires. Après avoir présenté les méthodes existantes, nous introduisons notre principale contribution: un nouveau schéma algorithmique pour l'analyse d'accessibilité des systèmes linéaires invariants qui surclasse nettement les algorithmes existants. Une implémentation exacte peut produire des ensembles difficiles à manipuler, nous proposons donc une version produisant une sur-approximation non soumise à l'effet d'emballage, une accumulation incontrôlée des erreurs d'approximation, ainsi qu'une variante dédiée aux fonctions support, une représentation fonctionnelle des ensembles convexes. La deuxième partie adapte ces résultats aux systèmes hybrides. Nous montrons d'abord comment gérer les invariants, avant de nous intéresser à l'approximation de l'intersection entre l'ensemble atteignable par la dynamique continue et des gardes hyperplanaires.

Dans cette thèse nous nous intéressons à une technique de vérification basée sur les approximations par réécriture dans le but de l'automatiser et d'étendre son domaine d'application. L'utilisation de cette technique permet la vérification de propriétés pour des systèmes informatique. Une sur-approximation des termes atteignables par réécriture est calculée et nous pouvons déterminer si des termes indésirables (représentant la propriété) appartiennent à la sur-approximation. Si ils n'appartiennent pas à la sur-approximation alors on est sûr que les termes indésirables ne sont pas atteignables par le système et la propriété est vérifiée, sinon nous ne pouvons pas conclure à cause de la sur-approximation. C'est dans ce cadre que se placent les contributions de cette thèse. Tout d'abord nous présentons une méthode de raffinement d'approximation, s'inspirant du paradigme CEGAR (Counterexample-Guided Abstraction Refinement), déterminant comment construire automatiquement une approximation qui ne contient pas de terme indésirable. Si cette construction échoue alors des termes indésirables sont atteignables et on peut conclure que le système analysé ne vérifie pas la propriété. De plus, à partir d'un graphe des réécritures, nous présentons comment vérifier trois modèles de propriétés LTL exprimant des conditions sur l'ordre d'application des règles de réécriture. D'autre part, nous présentons dans cette thèse deux nouvelles applications de cette technique : la vérification de spécifications écrites avec l'algèbre de processus CCS (sans renommage) et l'analyse d'atteignabilité par approximation de deux problèmes indécidables pour les machines de Turing.

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles. / The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks.

Cette thèse porte sur le calcul d'une sur-approximation conservative pour les solutions d'équations différentielles ordinaires en présence d'incertitudes et sur son application à l'estimation et l'analyse de systèmes dynamiques à temps continu. L'avantage principal des méthodes et des algorithmes de calculs présentés dans cette thèse est qu'ils apportent une preuve numérique de résultats. Cette thèse est organisée en deux parties. La première partie est consacrée aux outils mathématiques et aux méthodes d'intégration numérique garantie des équations diff érentielles incertaines. Ces méthodes permettent de caractériser de manière garantie l'ensemble des trajectoires d'état engendrées par un système dynamique incertain dont les incertitudes sont naturellement représentées par des intervalles bornés. Dans cette optique, nous avons développé une méthode d'intégration hybride qui donne de meilleurs résultats que les méthodes d'intégration basées sur les modèles de Taylor intervalles. La seconde partie aborde les problèmes de l'identification et de l'observation dans un contexte à erreurs bornées ainsi que le problème d'atteignabilité continue pour la véri cation de propriétés des systèmes dynamiques hybrides.

Cette thèse est consacrée à l'analyse algorithmique des systèmes hybrides. Nous examinons plusieurs problèmes liés à l'étude et au controle des systèmes hybrides linéaires par morceaux. Dans une première partie, nous présentons les notions de base de la théorie. Nous illustrons notre propos grace à de nombreux exemples. La deuxième partie est dédiée au calcul algorithmique des exécutions acceptées par un système hybride. Une méthode de détection des événements (changement de valeur de la variable discrète du système) est proposée. Le cas des exécutions périodiques est également examiné. Dans la troisième partie, nous abordons le problème du calcul de l'ensemble atteignable des systèmes hybrides. Nous apportons un soin particulier aux systèmes où les dynamiques continues sont connues de manière incertaine. Dans la quatrième partie, nous nous intéressons au controle des systèmes hybrides. Nous construisons une analyse multirésolution de l'espace des entrées d'un système linéaire et calculons une base d'ondelettes associée. Les propriétés de cette base se révèlent intéressantes pour la synthèse de signaux d'entrée d'un système hybride. Dans la dernière partie nous montrons que les techniques développées pour les systèmes hybrides linéaires par morceaux peuvent etre utilisées pour analyser des systèmes dynamiques non-linéaires.

Les programmes informatiques prennent une place de plus en plus importante dans nos vies. Certains de ces programmes, comme par exemple les systèmes de contrôle de centrales électriques, d'avions ou de systèmes médicaux sont critiques : une panne ou un dysfonctionnement pourraient causer la perte de vies humaines ou des dommages matériels ou environnementaux importants. Les méthodes formelles visent à offrir des moyens de concevoir et vérifier de tels systèmes afin de garantir qu'ils fonctionneront comme prévu. Au fil du temps, ces systèmes deviennent de plus en plus évolués et complexes, ce qui est source de nouveaux défis pour leur vérification. Il devient nécessaire de développer ces systèmes de manière modulaire afin de pouvoir distribuer la tâche d'implémentation à différentes équipes d'ingénieurs. De plus, il est important de pouvoir réutiliser des éléments certifiés et les adapter pour répondre à de nouveaux besoins. Aussi les méthodes formelles doivent évoluer afin de s'adapter à la conception et à la vérification de ces systèmes modulaires de taille toujours croissante. Nous travaillons sur une approche algébrique pour la conception de systèmes corrects par construction. Elle définit un formalisme pour exprimer des spécifications de haut niveau et permet de les raffiner de manière incrémentale en des spécifications plus concrètes tout en préservant leurs propriétés, jusqu'à ce qu'une implémentation soit atteinte. Elle définit également plusieurs opérations permettant de construire des systèmes complexes à partir de composants plus simples en fusionnant différents points de vue d'un même système ou en composant plusieurs sous-systèmes ensemble, ainsi que de décomposer une spécification complexe afin de réutiliser des composants existants et de simplifier la tâche d'implémentation. Le formalisme de spécification que nous utilisons est basé sur des spécifications modales. Intuitivement, une spécification modale est un automate doté de deux types de transitions permettant d'exprimer des comportements optionnels ou obligatoires. Raffiner une spécification modale revient à décider si les parties optionnelles devraient être supprimées ou rendues obligatoires. Cette thèse contient deux principales contributions théoriques basées sur une extension des spécifications modales appelée " spécifications à ensembles d'acceptation ". La première contribution est l'identification d'une sous-classe des spécifications à ensembles d'acceptation, appelée " spécifications à ensembles d'acceptation convexes ", qui permet de définir des opérations bien plus efficaces tout en gardant un haut niveau d'expressivité. La seconde contribution est la définition d'un nouveau formalisme, appelé " spécifications à ensembles d'acceptation marquées ", qui permet d'exprimer des propriétés d'atteignabilité. Ceci peut, par exemple, être utilisé pour s'assurer qu'un système termine ou exprimer une propriété de vivacité dans un système réactif. Les opérations usuelles sont définies sur ce nouveau formalisme et elles garantissent la préservation des propriétés d'atteignabilité. Cette thèse présente également des résultats d'ordre plus pratique. Tous les résultats théoriques sur les spécifications à ensembles d'acceptation convexes ont été prouvés en utilisant l'assistant de preuves Coq. L'outil MAccS a été développé pour implémenter les formalismes et opérations présentés dans cette thèse. Il permet de les tester aisément sur des exemples, ainsi que d'étudier leur efficacité sur des cas concrets. / Software programs are taking a more and more important place in our lives. Some of these programs, like the control systems of power plants, aircraft, or medical devices for instance, are critical: a failure or malfunction could cause loss of human lives, damages to equipments, or environmental harm. Formal methods aim at offering means to design and verify such systems in order to guarantee that they will work as expected. As time passes, these systems grow in scope and size, yielding new challenges. It becomes necessary to develop these systems in a modular fashion to be able to distribute the implementation task to engineering teams. Moreover, being able to reuse some trustworthy parts of the systems and extend them to answer new needs in functionalities is increasingly required. As a consequence, formal methods also have to evolve in order to accommodate both the design and the verification of these larger, modular systems and thus address their scalability challenge. We promote an algebraic approach for the design of correct-by-construction systems. It defines a formalism to express high-level specifications of systems and allows to incrementally refine these specifications into more concrete ones while preserving their properties, until an implementation is reached. It also defines several operations allowing to assemble complex systems from simpler components, by merging several viewpoints of a specific system or composing several subsystems together, as well as decomposing a complex specification in order to reuse existing components and ease the implementation task. The specification formalism we use is based on modal specifications. In essence, a modal specification is an automaton with two kinds of transitions allowing to express mandatory and optional behaviors. Refining a modal specification amounts to deciding whether some optional parts should be removed or made mandatory. This thesis contains two main theoretical contributions, based on an extension of modal specifications called acceptance specifications. The first contribution is the identification of a subclass of acceptance specifications, called convex acceptance specifications, which allows to define much more efficient operations while maintaining a high level of expressiveness. The second contribution is the definition of a new formalism, called marked acceptance specifications, that allows to express some reachability properties. This could be used for example to ensure that a system is terminating or to express a liveness property for a reactive system. Usual operations are defined on this new formalism and guarantee the preservation of the reachability properties as well as independent implementability. This thesis also describes some more practical results. All the theoretical results on convex acceptance specifications have been proved using the Coq proof assistant. The tool MAccS has been developed to implement the formalisms and operations presented in this thesis. It allows to test them easily on some examples, as well as run some experimentations and benchmarks.

Cette thèse porte sur le calcul d'une sur-approximation conservative pour les solutions d'équations différentielles ordinaires en présence d'incertitudes et sur son application à l'estimation et l'analyse de systèmes dynamiques à temps continu. L'avantage principal des méthodes et des algorithmes de calculs présentés dans cette thèse est qu'ils apportent une preuve numérique de résultats. Cette thèse est organisée en deux parties. La première partie est consacrée aux outils mathématiques et aux méthodes d'intégration numérique garantie des équations diff érentielles incertaines. Ces méthodes permettent de caractériser de manière garantie l'ensemble des trajectoires d'état engendrées par un système dynamique incertain dont les incertitudes sont naturellement représentées par des intervalles bornés. Dans cette optique, nous avons développé une méthode d'intégration hybride qui donne de meilleurs résultats que les méthodes d'intégration basées sur les modèles de Taylor intervalles. La seconde partie aborde les problèmes de l'identification et de l'observation dans un contexte à erreurs bornées ainsi que le problème d'atteignabilité continue pour la véri cation de propriétés des systèmes dynamiques hybrides. / This thesis addresses the computation of conservative over-approximation of the solutions of uncertain ordinary di erential equations and its application to the estimation and the analysis of uncertain continuous-time dynamical systems. The main feature of the methods and algorithms presented in this thesis is the fact that they are numerically veri ed and hence can be used to obtain numerical proof of properties. This thesis is organized in two parts. The first part is devoted to the mathematical tools and the guaranteed numerical integration methods for uncertain ordinary di erential equations. These methods make it possible to characterize in a guaranteed way all the state trajectories generated by an uncertain dynamical system whose uncertainties are in a natural way described by bounded boxes. Accordingly, we have developed a hybrid integration method which gives better results than the integration methods based on interval Taylor models. The second part is dedicated to the resolution of identi cation and observation issues in a bounded error context. It also deals with continuous reachability computation for the veri cation of the properties of hybrid dynamical systems.