Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version radicale de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondant: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans ce rapport une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple / Pedagogical formal systems have appeared recently for propositional calculus (up to the higher order), and it consists of systematically give examples of introduced notions (hypotheses). Formally, it means that to use a set Delta of formulas as hypotheses, one must first give a substitution sigma such that all the instances of formulas sigma(Delta) can be proved. This neccesity of giving examples has been pointed out by Poincaré (1913) as a common-sense practice: a definition of an object by means of assumptions has interest only if such an object can be constructed. This restriction applied to intuitionistic formal systems is consistent with the idea of negationless mathematics advocated by Griss (1946) in the middle of the past century, and shown as a more radical view of intuitionism. Through the Curry-Howard isomorphism (1980), the computational counterpart is the utility of programs defined in the associated functional systems: every function can be applied to a closed value. First results concerning propositional calculi up to the second-order has recently been published by Colson and Michel (2007, 2008, 2009). In this thesis we present an attempt to standardize and to extend to the Calculus of Constructions (CC) those previous results. First a formal and precise definition of pedagogical sub-systems of the Calculus of Constructions is introduced, and different such sub-systems are exhibited as examples

Contexte : Les systèmes à logiciels prépondérants sont de plus en plus interopérables formant des alliances nommées « Systèmes-des-Systèmes » (SdS). Les applications des SdS peuvent aller des systèmes de gestion du trafic jusqu’aux systèmes de gestion de crises. Étant donné que les SdS supportent souvent des domaines critiques, ils doivent être fiables en traitant les disfonctionnements ou les défauts et en évitant les défaillances qui pourraient causer des dégâts et pertes importantes aux utilisateurs.Problème : Ajuster les opérations d’un SdS dépend d’une spécification précise et une attestation rigoureuse de sa consistance opérationnelle. Cependant, en plus des limitations des langages pour capturer conjointement la structure et le comportement des SdS, les prédictions de la consistance opérationnelle des SdS reposent sur leurs systèmes constitutifs qui ne sont pas totalement connus au moment de la conception. Par conséquent, les SdS ont été développés et déployés sans évaluation de leurs opérations, puisque les langages actuels ne supportent pas ce type de précision lors de l’évaluation. Objectif : Cette thèse fournit des solutions théoriques et pratiques basées sur un langage formel de description d’architectures pour supporter une évaluation précoce des opérations du SdS par rapport à la structure et le comportement du SdS à travers les simulations. Contributions : Les contributions essentielles de ce projet comprennent (i) une approche de transformation des modèles pour produire automatiquement des modèles de simulation à partir des descriptions des architectures logicielles du SdS, combinant la description structurelle et comportementale du SdS dans la même solution, (ii) une méthode d’évaluation de l’architecture logicielle du SdS pour la prédiction des opérations du SdS tout en considérant les changements inhérents qui peuvent se produire, (iii) la modélisation de l’environnement et la génération automatique des générateurs de stimulus pour soutenir la simulation des SdS, livrant des données pour nourrir tel simulation, et (iv) une méthode pour la synchronisation automatique entre l’architecture descriptive d’exécution (qui change à l’exécution par suite de l’architecture dynamique) et son architecture prescriptive d’origine basée sur des mécanismes de découverte et de récupération de modèles et une transformation de modèle à l'envers.Évaluation : Nous avons conduit des cas d’études pour évaluer nos approches en utilisant le SdS de surveillance des inondations et le SdS d’espace.Résultats : Notre approche montre une précision importante pour (i) produire des simulations des architectures logicielles des SdS sans failles et complètement opérationnelles, (ii) supporte une évaluation et une prédiction fiable des opérations du SdS à la phase de conception, (iii) génère de manière automatique des générateurs de stimuli pour soutenir et nourrir l’exécution de la simulation et (iv) maintien la synchronisation entre les versions descriptives et prescriptives de l’architecture du SdS.Conclusion : Nous avons conclu que les approches proposées font évoluer l’état de l’art de l’évaluation des architectures logicielles des SdS en offrant des solutions pour prédire l’efficacité des opérations du SdS pour maintenir une opération continue malgré les changements architecturaux, fournissant plus de confidence aux utilisateurs qui reposent dans l’avenir sur les services du SdS. / Context: Software-intensive systems have been increasingly interoperated forming alliances termed as “Systems-of-Systems” (SoS). SoS comprises a collection of systems joined to achieve a set of missions that none of the systems can individually accomplish. Each constituent system keeps its own management, goals, and resources while coordinating within the SoS and adapting to meet SoS goals. Applications of SoS range from traffic control to emergency response and crisis management. As SoS often support critical domains, such systems must be trustworthy by dealing with malfunction or defects and avoiding failures that could cause extensive damage and losses to the users.Problem: Correct SoS operations depend on a precise specification of the SoS structure and a rigorous attestation of its behaviors. However, besides limitations on languages to jointly capture SoS structure and behavior, predictions on the SoS emergent behaviors rely on constituent systems not totally known at design-time. Therefore, SoS have been developed and deployed without evaluating their operation, since current languages do not support such precision in evaluation.Objectives: This PhD project provides solutions founded on a formal architectural description language to support an early evaluation of SoS behaviors regarding its inherent SoS structure and dynamics through simulations.Contribution: The main contributions of this project comprise (i) a model transformation approach for automatically producing simulation models from SoS software architecture descriptions, combining SoS structure and behavior description in a same solution, (ii) a SoS software architecture evaluation method for SoS operation prediction considering the inherent changes that can occur, (iii) environment modeling and automatic generation of stimuli generators to sustain the SoS simulation, delivering data to feed such simulation, and (iv) a method for the automatic synchronization between the runtime descriptive architecture (changed at runtime due to dynamic architecture) and its original prescriptive architecture based on model discovery and recovery mechanisms and a backward model transformation.Evaluation: We conducted case studies to assess our approaches using Flood Monitoring SoS and Space SoS.Results: Our approaches show a high accuracy to (i) produce fault-free and operational simulations for SoS software architectures, (ii) support a reliable evaluation and prediction of SoS operation at design-time, (iii) automatically generate stimuli generators to sustain and feed the simulation execution, and (iv) maintain the synchronization between descriptive and prescriptive versions of the SoS architecture.Conclusions: We concluded that the proposed approaches advance the state of the art in SoS software architecture evaluation by offering solutions to predict the SoS operations effectiveness to maintain a continuous operation despite architectural changes, providing more trust for users that in the future shall rely on SoS services.

Dans le domaine maritime, la maitrise de la navigation et de la conduite d’un navire sont deux aspects essentiels pour la bonne marche et la sécurité du navire, des personnels et la préservation de l’environnement maritime. Or, les navires modernes embarquent de plus en plus de technologies informatisées, connectées et automatisées pour gérer ces fonctions primordiales. Ces technologies (capteurs, actionneurs, automates, logiciels) qui constituent le système d’information (SI) d’un navire peuvent cependant être leurrées ou corrompues par un tiers, remettant ainsi en cause la confiance qui leur est accordée. Dans ce contexte, une nouvelle approche de détection des falsifications des informations fondée sur l’évaluation de la confiance dans les composants du SI est proposée. Du fait de leurcomplexité, les systèmes d’information des navires peuvent être considérés comme des ensembles de blocs fonctionnels inter-reliés qui produisent, traitent et reçoivent des informations. La confiance d’un bloc fonctionnel producteur d’information est évaluée au travers de sa capacité, divisée en deux composantes (compétence et sincérité), à rendre compte de la situation réelle du navire. Elle se propage ensuite, à l’instar de l‘information, aux autres entités du système, quelle que soit leur complexité. Différents scénarios ont été expérimentés grâce à l’élaboration d’un simulateur. La variabilité de la confiance face à des altérations volontaires d’informations numériques permet de déduire la survenue d’une attaque ainsi que sa cible sous certaines conditions. Sans se restreindre aux systèmes navals, l’approche proposée permet de s’adapter à une grande variété de situations incluant le facteur humain. Les travaux de cette thèse ont été soutenus et co-financés par la région Bretagne ainsi que la Chaire de Cyber Défense des Systèmes Navals impliquant l’Ecole Navale, IMT Atlantique, NavalGroup et Thales. / Navigation and ship’s management are two essential aspects for the security of the ship itself and people on board as much as the maritime environment protection. Modern ships ensure these functions by increasingly embedding connected and automated technologies such as sensors, actuators, programmable logic controllers and pieces of software. However, the security of this objects as well as the trust in the information they produce cannot be guaranteed: they can be deceived or under the control of a malicious third party. In this context, a novel approach of data falsification detection is proposed. It is based on trust assessment of information system components which can be seen as inter-related functional blocks producing, processing and receiving pieces of information. The trust one can have inproduction blocks, called information sources, is assessed through its ability to report real situation of the ship. Trust is then propagated to the remainder part of the system. A simulator was made thanks to which we experiment several scenarios including intentional modification of numerical data. In these cases and under some conditions, the variability of trust give us the ability to identify the attack occurrence as much as its target. Our proposition is not restricted to naval information systems and can be employed in various situations even with human factor.

Les systèmes de contrôle en réseau sont un champ actif de recherche, où les différentes composantes du réseau sont spatialement distribué et tentent d'atteindre un objectif global. Ils apparaissent naturellement lors l'interaction d'un système piloté par ordinateur avec le monde physique.Avec les systèmes de contrôle en réseau une classe connexe des systèmes est décrit par les systèmes Cyber-physique, où les capacités de calcul embarqué peuvent interagir avec le monde physique.Dans ce travail, nous allons considérer la tâche classique d'observation et d'estimation et étudier les cas où les contraintes induite par le réseau nécessite une adaptation des mécanismes classique d'observation et d'estimation.Dans les système de contrôle en raison de limitation des capteurs (pour des raisons pratiques telles que la réduction des coûts) certains états ou paramètre du système ne sont pas connus. Dans ce contexte, la notion classique d'observabilitéexprime la capacité de déduire de la mesure les valeurs d'intérêt.Premièrement nous considérons le problème de la réduction de l'échantillonnage par l'utilisation de échantillonnage événementiel et ce pour plusieurs classes de systèmes. Ensuite, une procédure d'estimation et de contrôle sera proposé pour résoudre le problème du consensus dans un système multi-agent.Considérant enfin une dynamique de véhicule plus complexe, nous nous concentrons sur l'estimation du coefficient de frottement de la route pour résoudre un problème de suivi. / Network control systems is an active field of study where interacting component spatially distributed try to achieve a global goal. They naturally emerge from the interaction of computer driven mechanism and the physical world.Along with network control system a related class of systems is described by the so called: Cyber-physical systems, where integrated physical computational capabilities can interact.In this work we will consider the classical task of observation and estimation and investigate cases where network induced constraint calls for adapted observation and estimation scheme.In control system due to limitation in sensors ( for practical reason such as cost reduction) all the value of interest (whether the some unmeasured state or unknown parameter)are unknown. The classical notion of observabilityaccount for the ability to deduce from measurement those value of interest.First sampling reduction by use of event trigger will be studied for several class of systems. Then an estimation and control scheme will be establish to solve the problem of consensus in a multi agents system.Finally considering a more complex vehicle dynamic we focus on the estimation of tire road friction coefficient to solve a tracking problem.

Cette thèse est dédiée à l'étude du problème de la stabilisation des systèmes affines à commutations. L'objectif est de concevoir des lois de commutation dépendantes de l'état qui stabilisent le système en boucle fermée. Premièrement, un aperçu de quelque résultat existant dans la littérature est présenté. Ensuite, un résultat général permettant la synthèse de lois de commutations pour la stabilisation des systèmes nonlinéaires affines en l'entré est proposé. La particularisation de ce résultat aux cas des systèmes affines à commutations et des systèmes linéaires à temps invariant avec une commande à relais a permis de synthétiser des lois de commutations garantissant leur stabilité asymptotique locale ou globale en boucle fermée. Grace à l'utilisation des fonctions de Lyapunov commutées une méthode numérique basée sur des LMIs permettant la conception de surfaces de commutations nonlinéaires est proposée. Une méthode permettant la synthèse de lois de commutations robustes vis-à-vis des perturbations sur les mesures est également développée pour assurer la stabilisation des systèmes affines à commutations. Le résultat est ensuite particularisé au cas des systèmes linéaires temps invariant avec commande à relais robuste. Enfin, le problème de la synthèse de lois de commutations basée-observateur est considéré. Des surfaces de commutations linéaires et nonlinéaires sont proposées en utilisant des fonctions de Lyapunov quadratiques et non-quadratiques. Des conditions de stabilisation asymptotique locale et globale sont développées. Les lois de commutations conçues dépendent de l'état reconstruit en utilisant un observateur de type Luenberger. De plus, le principe de séparation est démontré pour les systèmes affines à commutations ainsi que pour les systèmes linéaires temps invariant avec une commande à relais. / This thesis is dedicated to the study of the stabilization problem of switched affine systems with state-dependent switching laws. First, an overview of some existing results is proposed. In order to define the closed-loop system's solutions and to analyze its behavior over the switching surfaces the Filippov formalism is used. The stabilization problem is addressed using a Lyapunov approach which allows to derive numerical approaches based on LMIs. Throughout this thesis both switched affine systems and LTI systems with relay controllers are considered. Using a general framework for the class of nonlinear input-affine systems, a full state-dependent switching controller is designed in order to ensure both local and global asymptotic stability of the closed-loop system. Thanks to switching (Lur'e type) Lyapunov functions, a numerical approach based on LMIs that allows to derive a nonlinear stabilizing switching law is proposed. Moreover, a design approach of robust state-dependent switching laws for switched affine systems stabilization are proposed. The robustness property is studied with respect to bounded exogenous disturbances that affect the state measurements which are used for the design of the switching laws. Finally, observer-based switching controllers are designed to guarantee both local and global asymptotic stability of the closed-loop system. Using both quadratic and non-quadratic Lyapunov functions, linear and nonlinear switching surfaces are designed. The derived switching surfaces depend on the estimated state which is computed by a Luenberger observer. For both switched affine systems and LTI systems with relay controller the separation principle is proved.

Le fonctionnement d'un neurone, cellule fondamentale du système nerveux, intéresse de nombreuses disciplines scientifiques. Il existe ainsi des modèles mathématiques qui décrivent leur comportement par des systèmes d'EDO. Plusieurs de ces modèles peuvent ensuite être couplés afin de pouvoir étudier le comportement de réseaux, systèmes complexes au sein desquels émergent des propriétés. Ce travail présente, dans un premier temps, les principaux mécanismes régissant ce fonctionnement afin d'en comprendre la modélisation. Plusieurs modèles sont alors présentés, jusqu'à celui de Hindmarsh-Rose (1984), qui présente une dynamique lente-rapide. C'est sur l'étude numérique mais également théorique de la dynamique asymptotique et transitoire de ce dernier modèle, que se concentre la seconde partie de cette thèse. Dans une troisième partie, des réseaux d'interactions sont construits en couplant les systèmes dynamiques précédemment étudiés. L'étude du phénomène de synchronisation complète au sein de ces réseaux montre l'existence de propriétés émergentes pouvant être caractérisées par des lois de puissance. Enfin, un algorithme de détection de la synchronisation de bursts est proposé.

L'automatique est une discipline qui traite entre autres de la commande et du diagnostic des systèmes industriels. Une première étape à l'obtention de schémas de commande et de diagnostic est d'analyser les propriétés du système considéré. Les principales propriétés analysées sont la commandabilité, l'observabilité, la diagnosticabilité, la stabilité... Des critères, souvent basés sur des approches algébriques ou géométriques, permettent de caractériser ces propriétés. En outre, des travaux publiés dans les années 1970 ont permis d'introduire une nouvelle représentation de systèmes à base de graphes orientés. De ces travaux, il résulte que l'approche graphique fournit des solutions simples et est ainsi très bien adaptée pour analyser des systèmes de grande dimension et/ou incertains. Malheureusement, peu de travaux basés sur des méthodes graphiques traitent des systèmes non linéaires. Par notre travail, nous avons souhaité combler ce manque en étudiant les propriétés d'observabilité et de diagnosticabilité des systèmes bilinéaires structurés à l'aide d'une approche graphique. Des conditions graphiques nécessaires et suffisantes d'observabilité de l'ensemble et d'une partie de l'état d'un système sont formulées. Par la suite le problème de placement de capteurs est abordé afin de recouvrer les propriétés d'observabilité. Enfin, nous nous sommes focalisés sur la propriété de diagnosticabilité. Après avoir donné une condition graphique nécessaire et suffisante de solubilité du problème de détection de défauts, nous avons alors étudié différents cas particuliers de commande afin de donner des conditions de solubilité au problème actif de détection de défauts.

Un des plus importants profits qu'on peut tirer des M/NEMS est la capacité de les fabriquer en grande masse permettant leur assemblage sous forme de réseau. Toutefois, de nombreux problèmes s'opposent à l'utilisation de ces systèmes tels que la complexité de leur contrôle, la non-uniformité et les couplages entre leurs éléments, les sources de bruits et de non-linéarités, etc.. Il est alors nécessaire de prendre en compte ces différents aspects dès la phase de conception, les corriger ou les exploiter, pour aboutir à des nouvelles architectures qui répondent aux exigences de hautes performances. En se servant d'un large réseau de nano-transducteurs, une contribution au contrôle dynamique robuste d'une micro-surface « intelligente » est développée. La structure continue est ensuite remplacée par un réseau de NEMS dont le modèle est détaillé pour la première fois en tenant compte des dispersions entre les éléments. Des architectures de réseaux couplés sont proposées pour réduire les effets des dispersions, améliorant ainsi la sélectivité des filtres résultants. Basée sur le schéma de transductions distribuées, une nouvelle stratégie d'ajustement du filtre est élaborée par contrôle modal. Ces différents réseaux (couplés ou non) peuvent être utilisés pour des applications capteurs où le système de mesure est modélisé en fonction de la technique utilisée et de la structure adoptée avant d'améliorer les performances par un contrôle approprié. Une nouvelle configuration exploitant les non-linéarités de transduction est proposée pour compenser et mesurer la variation de la fréquence de résonance permettant de réduire la complexité du système global.

Les Systèmes Multi-Agents (SMA) forment un paradigme prometteur pour la conception de systèmes logiciel complexes. En effet, ce paradigme propose de nouvelles stratégies pour analyser, concevoir et implémenter de tels systèmes. Les systèmes multi-agents sont considérés comme des sociétés composées d'entités autonomes et indépendantes, appelées agents, qui interagissent en vue de résoudre un problème ou de réaliser collectivement une tâche. Nous nous plaçons dans un cadre d'ingénierie logicielle pour ce mémoire. Pour tout nouveau paradigme d'ingénierie logicielle pour pouvoir être pleinement appliqué et déployé il est nécessaire de disposer de nouveaux modèles et d'abstractions nouvelles. Ces abstractions servent de base à l'analyse et à la conception des SMA. De plus, toute méthodologie dédiée aux SMA doit prendre ces abstractions pour pouvoir développer des SMA de manière sys\-té\-ma\-ti\-que, sure, robuste et fiable. Les modèles à la base de tous les travaux dans ce mémoire sont composés de concepts organisationnels qui permettent de concevoir les SMA comme des sociétés d'individus, les agents, qui jouent des rôles dans des organisations. Ces concepts permettent également la description de structures organisationnelles complexes telles que les holarchies dans lesquelles les agents, désignés par le terme holons, peuvent être composés d'autres holons et définir une structure hiérarchique. La définition de ces concepts se fait au travers de méta-modèles exprimés avec une notation semi-formelle. Pour définir une sémantique non ambigüe et bénéficier d'outils de validation et de vérification nous proposons de spécifier des concepts au travers d'un langage formel. Aucun langage ne satisfaisant nos besoins nous avons composé deux langages existants : Object-Z et les statecharts. La syntaxe et la sémantique du langage formel OZS sont définies sur cette base. Des architectures d'agents sont étudiées en utilisant le modèle organisationnel et les outils formels. Ces études sont de deux types, définition complète d'une architecture et rétro-ingénierie afin de comprendre et analyser les éléments fondateurs d'architectures existantes pour pouvoir les réutiliser dans d'autres contextes. Deux méthodologies sont exploitant les concepts et la notation formelle sont proposées. La première est issue d'un travail initial concernant l'analyse et la conception de SMA Holoniques utilisant un cadre particulier. La deuxième est issue d'une collaboration avec Massimo Cossentino et est plus générale.

A l'heure où le paradigme dominant du développement est contesté par le succès de pays qui s'en sont démarqués, nous proposons de repenser le concept et le rôle de la « bonne gouvernance », présentée par les organisations internationales comme une solution ingénieuse et universelle qui viendrait pallier les carences des modèles de développement économique. Si les mesures de bonne gouvernance, qui visent par exemple à réduire la corruption, à améliorer la transparence de l'action publique ou à instaurer l'État de droit sont aussi souhaitables que nécessaires, les objectifs qui leur sont assignés en matière de développement économique ne peuvent être atteints sans une prise en compte des architectures institutionnelles spécifiques des pays en transition.<br />Dans ce travail, le développement est compris avant tout comme un processus de transformation institutionnelle d'un système où l'État est instrumentalisé à des fins privées via des arrangements interrelationnels et informels vers un système institutionnel fondé sur des mécanismes plus transparents et davantage respectueux de la règle du droit impersonnel. Les importants travaux de Douglass North nous enseignent en effet que la source d'une croissance économique durable est à rechercher d'abord dans l'existence d'institutions qui incitent à une organisation économique efficiente. Ce sont ces institutions, définies comme les règles du jeu dans une société, qui réduisent l'incertitude en offrant une structure stable des interactions humaines. Elles fournissent l'élément fondamental du processus de création de richesse : la confiance, la confiance que les agents économiques ont dans le respect des institutions qui régissent leurs interactions. Dès lors, l'analyse du développement se déplace vers la recherche des facteurs qui génèrent la confiance, voire les facteurs de destruction de cette confiance.<br />Appliquée aux pays arabes de la Méditerranée (PAM), notre démarche cherche à expliquer pourquoi les réformes de bonne gouvernance mise en oeuvre dans ces pays n'ont pas produit les résultats attendus. Pour ce faire, nous élaborons de nouveaux outils conceptuels afin d'analyser conjointement les dynamiques des institutions de gouvernance et du développement économique dans ces pays qui connaissent des mutations importantes en raison de leur insertion dans l'économie mondiale et la multiplication des acteurs. Nous mobilisons les indicateurs institutionnels issus des enquêtes élaborées par le MINEFE afin de décrire les spécificités institutionnelles des pays arabes de la Méditerranée. À travers une analyse multidimensionnelle,<br />nous montrons que les réformes institutionnelles dans ces pays sont effectives mais les systèmes de gouvernance des entreprises et des Etats, censés délimiter le pouvoir discrétionnaire des élites dirigeantes, demeurent faiblement contraignants. La transition institutionnelle reste ainsi partielle en raison de la résistance d'une certaine élite au changement d'un système institutionnel qui leur permet un accès privilégié aux ressources du pouvoir. Nous soutenons dans ce travail que les systèmes institutionnels à l'oeuvre dans les PAM ne sont pas de nature à contraindre l'action des élites dirigeantes à entreprendre les réformes nécessaires au changement institutionnel. Nous avançons les arguments selon lesquels la persistance des institutions héritées du passé et la perpétuation des modèles de pensée claniques ont plutôt favorisé les organisations prédatrices et les institutions tournées vers la recherche de rente.