Nous nous intéressons à un cadre théorique de l'analyse de données : l'analyse formelle de concepts. Le formalisme de l'analyse formelle de concepts permet d'exprimer les notions centrales de la fouille de données telles que les implications ou les ensembles fermés, avec au centre la notion de treillis qui décrit la structure et les relations que ces objets ont entre eux. Pour les données multidimensionnelles, une proposition de formalisme existe en tant que généralisation de l'analyse formelle de concepts : l'analyse polyadique de concepts. Dans cette thèse, nous étudions certains problèmes de combinatoire et d'algorithmique dans le cas de l'analyse polyadique de concepts. Nous approchons aussi un cadre plus appliqué à l'analyse de données en proposant des approches de navigation conceptuelle et de classification. / We are interested in formal concept analysis, a theoretical framework for data analysis.This formalism allows to express some central notions of data mining such as implications or closed itemsets, and is centered around lattices, as the description of the relational structure that those objects can have.For multidimensional data, a formalism exists as a generalisation of formal concept analysis : polyadic concept analysis.In this document, we study some combinatorial and algorithmic problems that arose in polyadic concept analysis.We also introduce more applied data analysis techniques of conceptual navigation and classification.

Les équipements intelligents, notamment les smartphones, sont la cible de nombreuses attaques de sécurité. Par ailleurs, la mise en œuvre de mécanismes de protection usuels est souvent inadaptée du fait de leurs ressources fortement contraintes. Dans ce contexte, nous proposons d'utiliser des chaînes de fonctions de sécurité qui sont composées de plusieurs services de sécurité, tels que des pare-feux ou des antivirus, automatiquement configurés et déployés dans le réseau. Cependant, ces chaînes sont connues pour être difficiles à valider. Cette difficulté est causée par la complexité de ces compositions qui impliquent des centaines, voire des milliers de règles de configuration. Dans cette thèse, nous proposons l'architecture d'un orchestrateur exploitant la programmabilité des réseaux pour automatiser la configuration et le déploiement de chaînes de fonctions de sécurité. Il est important que ces chaînes de sécurité soient correctes afin d’éviter l'introduction de failles de sécurité dans le réseau. Aussi, notre orchestrateur repose sur des méthodes automatiques de vérification et de synthèse, encore appelées méthodes formelles, pour assurer la correction des chaînes. Notre travail appréhende également l'optimisation du déploiement des chaînes dans le réseau, afin de préserver ses ressources et sa qualité de service. / Smart environments, in particular smartphones, are the target of multiple security attacks. Moreover, the deployment of traditional security mechanisms is often inadequate due to their highly constrained resources. In that context, we propose to use chains of security functions which are composed of several security services, such as firewalls or antivirus, automatically configured and deployed in the network. Chains of security functions are known as being error prone and hard to validate. This difficulty is caused by the complexity of these constructs that involve hundreds and even thousands of configuration rules. In this PhD thesis, we propose the architecture of an orchestrator, exploiting the programmability brought by software defined networking, for the automated configuration and deployment of chains of security functions. It is important to automatically insure that these security chains are correct, before their deployment in order to avoid the introduction of security breaches in the network. To do so, our orchestrator relies on methods of automated verification and synthesis, also known as formal methods, to ensure the correctness of the chains. Our work also consider the optimization of the deployment of chains of security functions in the network, in order to maintain its resources and quality of service.

La préservation de propriétés établies sur le programme source jusqu'au code exécutable est un point important dans les méthodes formelles. Cette propriété de préservation est établie par la vérification formelle du proccessus de compilation. Un compilateur est formellement vérifié s'il est accompagné d'une preuve de préservation sémantique : "si la compilation réussit, le code compilé se comporte comme le code source le prédit." Le projet CompCert étudie la vérification formelle de compilateurs réalistes utilisable dans l'embarqué-critique. Il s'agit de développer et formellement vérifier de tels compilateur via l'assistant de preuve Coq. Un compilateur pour le langage C vers l'assembleur PowerPC a déjà ainsi été produit. Le code exécutable du compilateur a été obtenu en deux étapes non vérifiés : la génération automatique de code Ocaml par le mécanisme d'extration de Coq et la compilation du de ce code extrait par le système Objective Caml. En fait, cette lacune est commune à tous les développements spécifiés dans l'assistant de preuve Coq et destinés à produire un éxécutable. Cette thèse décrit l'étude, le développement et la vérification formelle, dans l'assistant de preuve Coq, d'un compilateur pour le fragment purement fonctionnel du langage ML : le langage cible du mécanisme d'extraction de Coq. Concrètement, il s'git d'une chaîne de compilation en amont pour mini-ML (lambda calcul, let, letrec et filtrage) vers le premier langage intermédiaire de la chaîne de compilation en aval du compilateur CompCert. Ce langage, Cminor, est un langage de bas niveau à la C. L'expressivité du langage source traité rend ce compilateur réaliste. Il comporte aussi des optimisations classiques propre à la compilation de langages fonctionnels : la décurryfication, comme celle implémentée dans le compilateur OCaml ; la représentation uniforme des données, explicitation des fermetures, numérotation des constructeurs et une mise en style par passage de continuation (CPS) optimisée. Le point fort de ce compilateur et que, comme les compilateurs modernes pour langage de haut niveau, il peut interagir avec un gestionnaire de mémoire automatique. Cette interaction a aussi été formellement vérifiée.

L'utilisation omniprésente des systèmes informatiques impose de s'assurer de leur bon fonctionnement. Dans ce but, les méthodes de vérification formelle permettent de suppléer les simulations qui ne peuvent être complètement exhaustives du fait de la complexité croissante des systèmes. Le model checking fait partie de ces méthodes et présente l'avantage d'être complètement automatisée. Cette méthode consiste à développer des algorithmes pour vérifier qu'une spécification exprimée la plupart du temps sous la forme d'une formule logique est satisfaite par un modèle du système. Les langages historiques de spécification utilisent comme formules atomiques des variables propositionnelles qui permettent d'exprimer principalement des propriétés portant sur les états de contrôle du modèle. Le but de cette thèse est de vérifier des propriétés plus riches portant sur diverses données manipulées par les modèles: des compteurs, des horloges ou des queues. Ces données peuvent prendre une infinité de valeurs et induisent donc des modèles avec un nombre infini d'états. Nous définissons un cadre général pour l'extension des logiques temporelles avec des contraintes permettant de comparer la valeur des variables a différents états de l'exécution. Nous établissons des résultats de décidabilité et complexité pour des problèmes de model checking impliquant diverses instances de ces extensions. Nous privilégions pour cela l'approche à base d'automates en combinant des constructions connues pour les logiques propositionnelles classiques avec des méthodes d'abstraction des modèles dont les variables sont interprétées dans des domaines infinis.

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.

Nos activités de recherches se déclinent selon une double perspective : l'histoire de la pensée économique et l'économie historique. Ceci implique, si nécessaire, des détours par des disciplines connexes mais tout à fait nécessaires, comme la philosophie, la science politique et, bien sûr, l'histoire proprement dite. A cet égard, le mémoire de synthèse pour cette habilitation à diriger les recherches (HDR) est essentiellement centré autour de recherches en histoire des idées, même si un thème ordonne l'ensemble de nos travaux : la notion d'institution. Celle-ci, selon nous, permet de mieux comprendre la construction et la valeur empirique des catégories économiques. La référence à cette notion est issue des travaux fondateurs des économistes américains dits « institutionnalistes » du début du XXième siècle : plus encore, nous intégrons le travail de Polanyi et de son école dans cette mouvance.<br><br> C'est pourquoi la première partie de notre travail - « une trajectoire de recherche » - est une mise en confrontation, dans le champ de l'histoire économique, entre les thèses institutionnalistes et les thèses néoclassiques, voire néo-institutionnalistes (inspirées notamment par l'œuvre de North). Nous essayons de montrer que les débats portant sur l'histoire économique d'avant la révolution industrielle sont marqués par l'ambivalence de la figure du marché. Cette figure est, en effet, parfois comprise comme le système constitué par les marchés autorégulateurs, ou parfois entendue selon des cadres institutionnels n'autorisant pas de tels mécanismes autorégulateurs, comme en témoigne la problématique polanyienne de la « place de marché » et les travaux plus récents d'A. Guéry sur les marchés d'Ancien Régime. Nous ne faisons qu'illustrer la formule de Commons qui, en 1923, écrivit que le capitalisme avait besoin de fondations légales, ce qui nous contraint à revenir sur la richesse du cadre d'analyse wébérien pour enrichir notre perspective.<br><br> La seconde partie de la présente HDR est un exercice en histoire des idées, qui se distribue selon des axes a priori bien différents, mais tentant tous d'illustrer la problématique institutionnaliste dans ce qu'elle a d'essentiel. <br> Dans un premier chapitre - « instituer, « monnayer et troquer » -, nous nous interrogeons sur la place du troc dans le discours économique parce que celui-ci est la forme matricielle de l'interaction économique ne présupposant pas de cadre institutionnel. L'économie comme science part, en effet, de ce prototype de l'échange rationnel, qu'est le troc, pour y intégrer la monnaie a posteriori, qui fonctionne alors comme une marchandise d'un type singulier. L'hypothèse qui est présentée est inverse : c'est le caractère institutionnel de la monnaie qui est la condition de possibilité de l'économie marchande. Nous nous inscrivons, pour une bonne part, dans la problématique développée, dès 1982, par M. Aglietta et A. Orléan, en essayant d'y introduire des éléments fondamentaux de la problématique institutionnaliste comme Mitchell, le fondateur du NBER, les avait déjà conçus. La présente réflexion s'écarte toutefois de la problématique de la « fable du troc », reprise par nombre d'économistes hétérodoxes et de sociologues à la suite de J-M Servet, grâce à un réexamen critique des assertions typiques des années 1970 et d'une reconsidération de données anthropologiques. La thèse d'une « institution monétaire de la société » est ainsi remise en cause car, considérer la monnaie comme une essence anthropologique revient à l'essentialiser, ce qui est fort peu institutionnaliste. Par ailleurs, il n'est pas sûr que le perspectivisme nietzschéen s'accorde avec la valeur que l'économie comme science, marxiste ou non, accorde à la vérité.<br><br> Dans un deuxième chapitre – « Souveraineté et économie » -, nous essayons de poser la question du rapport entre économie et souveraineté à un moment où le processus actuel de la construction européenne, parce qu'il tend à modifier les institutions politiques et économiques, remet au premier plan une préoccupation fondatrice de l'économie politique, celle du Traicté de l'Œconomie politique de Montchrestien (1615). Cet auteur illustre une conception moderne, profondément politique, de l'économie, en rupture avec l'esprit antique ou médiéval selon lequel l'économie appartient de facto à la stricte sphère domestique et ne peut être l'objet de l'action publique. Montchrestien montre que la richesse des peuples, donc de l'Etat, est fondamentalement instituée par le Prince ; l'économie n'est pas ici une catégorie autonome de pensée ou une dimension émergente des comportements.<br> Mais, la concurrence est au cœur du discours de Montchrestien, les marchés étant la codification politique des flux concurrentiels. Contre une interprétation répandue, nous montrons que, selon Montchrestien, les échanges intérieurs, où les gains issus de l'échange sont possibles, s'opposent aux formes extérieures de l'échange réfractant l'état de nature, où ce que gagne l'un est perdu par l'autre. Il estime même que l'application du droit des gens pourrait rendre le commerce extérieur bénéfique si disparaissent les asymétries de position résultant des politiques des Etats. Toutefois, avec Cantillon, en moins d'un siècle, la question des articulations entre institutions politique et économique se reformule radicalement cependant qu'apparaît dans la théorie économique, en un sens devenu plus familier, une figure devenue majeure : l'entrepreneur. Il n'en demeure pas moins que Cantillon ne pousse pas ses intuitions libérales de l'autoconstitution du social et de l'équilibre économique jusqu'à dénier au politique toute efficacité en économie. <br>Dans le dernier chapitre – « Economie, politique et fascisme » -, contribution à l'histoire des idées institutionnalistes, nous montrons que la portée scientifique de l'apport de Polanyi va bien au delà du concept fort connu d'embeddedness, en exposant les analyses méconnues faites par Polanyi des fascismes et de l'économie des années 1930. La thèse fondamentale de Polanyi est la suivante : la société de marché n'est pas le fruit d'un évolutionnisme qui aurait conduit au meilleur des mondes. Fruit de contingences historiques, comme le furent les actions délibérées des Etats et la volonté d'incarner un projet essentiellement utopique, la société de marché doit être comprise comme une création humaine porteuse de catastrophes dont le nazisme est un exemple. Anticipant la fameuse « querelle des historiens » propre à l'Allemagne des années 1980, Polanyi s'inscrit en faux contre l'explication de la genèse des fascismes par le bolchevisme, thèse déjà développée dans les années 1930 elles-mêmes, et veut redonner toute sa force à ce processus très singulier de la constitution d'une société économique du XIXième siècle.<br>Polanyi met donc en avant le caractère absolument nouveau que constitue le capitalisme concurrentiel du XIXième siècle, tout en insistant sur la nature endogène des processus détruisant les capacités d'autorégulation de ce système inédit. A cet égard, le fascisme est une issue à la société libérale caractérisée par la séparation institutionnelle du politique et de l'économie. Or, dans cette société, les propriétaires du capital ont la capacité de vider de tout pouvoir effectif les institutions politiques investies par les représentants des partis populaires, chose fréquente en cas de crise grave, ce qui rend impossible la reproduction même d'une société complexe qui ne peut faire l'économie d'une régulation politique de ses contradictions. Le fascisme est ainsi une expression toujours possible de la contradiction entre démocratie et capitalisme. Il s'agit donc de redonner à la science économique toute sa place dans l'explication d'un phénomène comme le fascisme et de reconsidérer les acquis problématiques d'une certaine science politique en la matière.<br>En conclusion, nous rappelons que notre intérêt pour les institutions, du point de vue des idées ou des faits, est issu de la problématique de P. Dockès dans La Libération Médiévale, qui se donnait pour objet, en 1979, comme l'école radicale américaine, de penser la détermination sociale de l'économie à l'encontre des thèses technicistes ou économicistes.

Cette thèse propose une Démarche de Vérification Formelle d'Architectures Logicielles : DVFAL. La démarche DVFAL supporte divers formalismes de description d'architectures logicielles tels que : les ADL (langages de description d'architectures), UML2.0, Symphony et des profils UML2.0 dédiés au domaine des architectures logicielles. La démarche DVFAL préconise l'ADL Wright en tant que langage formel pivot permettant de représenter des architectures logicielles décrites dans les divers formalismes. En outre, elle propose des transformations de modèles sous forme des traducteurs (Wright vers CSP de Hoare et Wright vers Ada) pour bénéficier des outils de vérification des propriétés supportant CSP et Ada tels que FDR et FLAVERS. Enfin, la démarche DVFAL propose un profil UML2.0-Wright jouant le rôle d'un langage intermédiaire entre les formalismes à base d'UML et Wright.

Nos travaux de recherche consistent à apporter des solutions de modélisation conformément à l'approche MDA. Nos recherches consistent à fournir des solutions permettant de guider et d'assister les activités de modélisation des architectures logicielles. Il s'agit principalement de proposer une démarche de conception orientée modèle permettant de décrire l'architecture logicielle en tenant compte de trois aspects : le style architectural, les opérations de reconfiguration et le protocole de reconfiguration.<br />Nous proposons des notations visuelles permettant de décrire de façon compatible avec UML 2.0 l'architecture logicielle. La technique de description que nous adoptons est orientée règles, basée sur les théories de transformation de graphe, permettant, ainsi, de décrire la dynamique structurelle.<br />Nous proposons une extension d'UML 2.0 par un nouveau profil formé de trois méta-modèles. Nous proposons aussi une approche de validation basée sur des règles intra-modèle et des règles inter-modèles. Nous adoptons également une approche de vérification. Cette approche permet, dans une première étape, une transformation automatique du style architectural et de chaque opération de reconfiguration vers le langage Z. Elle permet dans une deuxième étape, de vérifier la consistance du style architectural et la conformité de l'évolution d'une architecture vis-à-vis de son style architectural. Nous utilisons le système de preuve Z/EVES. Finalement, nous proposons une démarche de modélisation des architectures logicielles dynamiques, appelée X, permettant de décrire les différentes étapes pour modéliser l'architecture logicielle. La démarche proposée est inspirée de la méthode MDA et 2TUP.<br />Le profil et la démarche X que nous avons proposés ont fait l'objet d'une implémentation et d'une intégration, sous forme de plug-in java, dans l'atelier d'aide à la conception FUJABA. Le plug-in implémenté est disponible sur l'URL : http://www.laas.fr/~khalil/TOOLS/X.zip.

Cette thèse traite de la restriction en français et fournit tout d'abord une « grammaire » de la restriction à partir de la description fine des unités restrictives telles "seul" (Seule Marie a vu Emma), "seulement" (Marie a seulement vu Emma), et "ne... que" (Marie n'a vu Emma qu'hier), ainsi qu'un modèle sémantique du phénomène. Elle rend ensuite compte de trois études sémantiques motivées par la complexité de certaines données. La première s'intéresse à l'interaction entre syntagmes nominaux et restriction. On observe que la grammaticalité d'une phrase composée d'un SN modifié par la restriction dépend de contraintes non pas syntaxiques mais sémantiques et pragmatiques. La seconde étude traite de l'application du principe de l'association avec le focus valable pour "only" (Jackendoff, 1972) à l'équivalent français "seulement". La validité du principe est remise en question à partir d'une étude sémantique inspirée par Vallduvi et Zacharski (1994), et d'une expérimentation prosodique, étude pilote sur les données du français. Enfin, la troisième étude propose de représenter compositionnellement la contribution sémantique de la restriction. En prolongeant le travail initié par Rooth (1985,1992), nous mettons en évidence que la contribution de la restriction ne peut pas toujours être représentée de la même façon et est fonction de la profondeur de l'élément modifié syntaxiquement par la restriction et/ou de l'élément auquel s'associe la restriction.

Lustre est un langage de programmation spécialement conçu pour la réalisation des systèmes réactifs. Le besoin de garantir que ces systèmes ont un comportement conforme a celui attendu nécessite de définir et de mettre en œuvre des méthodes de vérification formelle des programmes lustre, qui sont relatées dans cette thèse. La vérification d'un système consiste a contrôler que tous ses comportements sont corrects vis-a-vis de ses spécifications. Les comportements d'un programme lustre peuvent classiquement être représentés par une machine d'états finis, dont la génération permet de vérifier ses spécifications. La methode standard mettant en œuvre ce principe est limitée par le probleme d'explosion de la machine générée, qui n'est pas minimale. Un nouvel algorithme évitant ce probleme est présenté. Son implémentation nécessite l'emploi d'une technique de représentation et de manipulation symbolique de la machine (bdds), dont le cout d'utilisation est largement abaisse grâce a de nombreuses optimisations. Basées sur cette technique, deux autres implémentations originales de la methode standard et de la nouvelle methode proposée ci-dessus sont décrites. Les aspects de diagnostic correspondant au cas ou les programmes sont incorrects vis-a-vis de leurs spécifications sont aussi abordes