Les systèmes-de-systèmes (Systems-of-Systems, SoS) interconnectent plusieurs systèmes indépendants qui travaillent ensemble pour exécuter une action conjointe dépassant leurs compétences individuelles. Par ailleurs, les descriptions architecturales sont des artefacts qui décrivent des architectures logicielles jouant dans le contexte SoS un rôle important dans la promotion de l’interaction des éléments constituants tout en favorisant la communication parmi les intéressés et en soutenant les activités d’inspection et d’analyse dès le début de leur cycle de vie. Le principal problème traité dans cette thèse est le manque de descriptions architecturales adéquates pour les SoS qui sont développés sans l’attention nécessaire à leur architecture logicielle. Puisque les systèmes constituants ne sont pas forcément connus pendant la conception du projet à cause du développement évolutionnaire des SoS, la description architecturale doit définir à la conception même du projet quelles coalitions entre les systèmes constituants seront possibles pendant son exécution. En outre, comme plusieurs de ces systèmes sont développés pour le domaine critique de sécurité, des mesures supplémentaires doivent être mises en place pour garantir l’exactitude et la complétude de la description architecturale. Afin de résoudre ce problème, nous nous servons du SosADL, un langage formel créé spécialement pour le domaine SoS et qui permet de décrire les architectures logicielles comme des associations dynamiques entre systèmes indépendants où les interactions doivent être coordonnées pour réaliser une action combinée. Notamment, une nouvelle méthode formelle, nommée Ark, est proposée pour systématiser les étapes nécessaires dans la synthèse d’architectures concrètes obéissant à cette description. Dans ce dessein, cette méthode crée un modèle formel intermédiaire, nommé TASoS, qui décrit l’architecture du SoS en tant que problème de satisfaisabilité de restrictions, rendant ainsi possible la vérification automatique d’un ensemble initial de propriétés. Le résultat obtenu par cette analyse peut s’utiliser en raffinements et révisions ultérieurs de la description architecturale. Un outil logiciel nommé SoSy a été aussi développé pour automatiser la génération de modèles intermédiaires et d’architectures concrètes, en cachant l’utilisation de solveurs de contraintes dans le projet de SoS. Particulièrement, cet outil intègre un environnement de développement plus important et complet pour le projet de SoS. Cette méthode et son outil ont été appliqués dans un modèle de SoS de surveillance de rivières urbaines où la faisabilité d’architectures abstraites a été étudiée. En formalisant et en automatisant les étapes requises pour la synthèse architecturale de SoS, Ark contribue à l’adoption de méthodes formelles dans le projet d’architectures SoS, ce qui est nécessaire pour atteindre des niveaux plus élevés de fiabilité. / Systems-of-Systems (SoS) encompass diverse and independent systems that must cooperate with each other for performing a combined action that is greater than their individual capabilities. In parallel, architecture descriptions, which are the main artifact expressing software architectures, play an important role in fostering interoperability among constituents by facilitating the communication among stakeholders and supporting the inspection and analysis of the SoS from an early stage of its life cycle. The main problem addressed in this thesis is the lack of adequate architectural descriptions for SoS that are often built without an adequate care to their software architecture. Since constituent systems are, in general, not known at design-time due to the evolving nature of SoS, the architecture description must specify at design-time which coalitions among constituent systems are feasible at run-time. Moreover, as many SoS are being developed for safety-critical domains, additional measures must be placed to ensure the correctness and completeness of architecture descriptions. To address this problem, this doctoral project employs SoSADL, a formal language tailored for the description of SoS that enables one to express software architectures as dynamic associations between independent constituent systems whose interactions are mediated for accomplishing a combined action. To synthesize concrete architectures that adhere to one such description, this thesis develops a formal method, named Ark, that systematizes the steps for producing such artifacts. The method creates an intermediate formal model, named TASoS, which expresses the SoS architecture in terms of a constraint satisfaction problem that can be automatically analyzed for an initial set of properties. The feedback obtained in this analysis can be used for subsequent refinements or revisions of the architecture description. A software tool named SoSy was also developed to support the Ark method as it automates the generation of intermediate models and concrete architectures, thus concealing the use of constraint solvers during SoS design and development. The method and its accompanying tool were applied to model a SoS for urban river monitoring in which the feasibility of candidate abstract architectures is investigated. By formalizing and automating the required steps for SoS architectural synthesis, Ark contributes for adopting formal methods in the design of SoS architectures, which is a necessary step for obtaining higher reliability levels.

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.

Avec des motivations venant du domaine de la Vérification, nous définissons une notion de WQO effectifs pour lesquels il est possible de représenter les ensembles clos et de calculer les principales opérations ensemblistes sur ces représentations. Dans une première partie, nous montrons que de nombreuses constructions naturelles sur les WQO préservent notre notion d'effectivité, prouvant ainsi que la plupart des WQOs utilisés en pratique sont effectifs. Cette partie est basée sur un article non publié dont Jean Goubault-Larrecq, Narayan Kumar, Prateek Karandikar et Philippe Schnoebelen sont co-auteurs.Dans une seconde partie, nous étudions les conséquences qu'a notre notion sur la logique du première ordre interprété sur un WQO. Bien que le fragment existentiel positif soit décidable pour tous les WQOs effectif, les perspectives de généralisation sont limitées par le résultat suivant: le fragment existentiel de la logique du première ordre sur les mots finis, ordonnés par plongement, est déjà indécidable. Ce résultat a été publié à LICS 2017 avec Philippe Schnoebelen et Georg Zetzsche. / With motivations coming from Verification, we define a notionof effective WQO for which it is possible to represent closed subsetsand to compute basic set-operations on these representations. In a firstpart, we show that many of the natural constructions that preserve WQOsalso preserve our notion of effectiveness, proving that a large class ofcommonly used WQOs are effective. This part is based on an unpublishedarticle with Jean Goubault-Larrecq, Narayan Kumar, Prateek Karandikarand Philippe Schnoebelen.In a second part, we investigate the consequences of our notion onfirst-order logics over WQOs. Although the positive existential fragmentis decidable for any effective WQO, the perspective of extension tolarger fragments is hopeless since the existential fragment is alreadyundecidable for the first-order logic over words with the subwordordering. This last result has been published in LICS 2017 with PhilippeSchnoebelen and Georg Zetzsche.

Les techniques de biologie moléculaire dites haut-débit permettent de mesurer un grand nombre de variables simultanément. Elles sont aujourd'hui couramment utilisées et produisent des masses importantes de données. Leur exploitation est compliquée par le bruit généralement observé dans les mesures, et ce d'autant plus que ces dernières sont en général trop onéreuses pour être suffisamment reproduites. La question abordée dans cette thèse porte sur l'intégration et l'exploitation des données haut-débit : chaque source de données mesurant un aspect du fonctionnement cellulaire, comment les combiner dans un modèle et en tirer des conclusions pertinentes sur le plan biologique ? Nous introduisons un critère de consistance entre un modèle graphique des régulations cellulaires et des données de déplacement d'équilibre. Nous montrons ensuite comment utiliser ce critère comme guide pour formuler des prédictions ou proposer des corrections en cas d'incompatibilité. Ces différentes tâches impliquent la résolution de contraintes à variables sur domaines finis, pour lesquelles nous proposons deux approches complémentaires. La première est basée sur la notion de diagramme de décision, qui est une structure de données utilisée pour la vérification des circuits ; la deuxième fait appel à des techniques récentes de programmation logique. L'utilisation de ces techniques est illustrée avec des données réelles sur la bactérie "E. coli" et sur la levure. Les réseaux étudiés comportent jusqu'à plusieurs milliers de gènes et de régulations. Nous montrons enfin, sur ces données, comment notre critère de consistance nous permet d'arriver à des prédictions robustes, ainsi que des corrections pertinentes du modèle étudié.

La programmation par contraintes offre des langages et des outils permettant de résoudre des problèmes à forte combinatoire et à la complexité élevée tels que ceux qui existent en vérification de programmes. Dans cette thèse nous résolvons deux familles de problèmes de la vérification de programmes. Dans chaque cas de figure nous commençons par une étude formelle du problème avant de proposer des modèles en contraintes puis de réaliser des expérimentations. La première contribution concerne un langage réactif synchrone représentable par une algèbre de diagramme de blocs. Les programmes utilisent des flux infinis et modélisent des systèmes temps réel. Nous proposons un modèle en contraintes muni d’une nouvelle contrainte globale ainsi que ses algorithmes de filtrage inspirés de l’interprétation abstraite. Cette contrainte permet de calculer des sur-approximations des valeurs des flux des diagrammes de blocs. Nous évaluons notre processus de vérification sur le langage FAUST, qui est un langage dédié à la génération de flux audio. La seconde contribution concerne les systèmes probabilistes représentés par des chaînes de Markov à intervalles paramétrés, un formalisme de spécification qui étend les chaînes de Markov. Nous proposons des modèles en contraintes pour vérifier des propriétés qualitatives et quantitatives. Nos modèles dans le cas qualitatif améliorent l’état de l’art tandis que ceux dans le cas quantitatif sont les premiers proposés à ce jour. Nous avons implémenté nos modèles en contraintes en problèmes de programmation linéaire en nombres entiers et en problèmes de satisfaction modulo des théories. Les expériences sont réalisées à partir d’un jeu d’essais de la bibliothèque PRISM. / Constraint programming offers efficient languages andtools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming.In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments.The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.

Suivant le domaine où on les sollicite, les solutions d’un système de contraintes géométriques (SCG) peuvent être : – formelles et exactes : elles prennent par exemple la forme d’un plan de construction produisant toutes les solutions, obtenu en appliquant des règles dérivées de lemmes de géométrie. Beaucoup de SCG, surtout en 3D, résistent à cette approche ; – numériques et approchées : elles sont les solutions d’un système d’équations construit à partir des contraintes et trouvées grâce à des méthodes numériques efficaces quand elles ne recherchent qu’une solution. De par la nature des problèmes traités, chercher toutes les solutions conduit à une complexité exponentielle. Les méthodes par continuation, ou homotopie, permettent d’obtenir toutes les solutions d’un système d’équations polynomiales. Leur application à des SCG est coûteuse et difficilement sujette aux raisonnements permis par l’origine géométrique du problème car elles opèrent hors de l’espace des figures géométriques. Notre travail a pour objet la spécialisation d’une méthode par continuation à des SCG. La géométrie simplifie et justifie sa mise en œuvre dans l’espace des figures, ou des raisonnements géométriques sont possibles. On aborde également les cas ou l’ensemble de solutions d’un problème contient des éléments isolés et des continuums. Des solutions proches d’une esquisse fournie par un utilisateur sont d’abord trouvées. La recherche d’autres solutions, malgré sa complexité exponentielle, est rendue envisageable par une approche itérative. Une nouvelle méthode de décomposition est proposée pour maîtriser le coût de la résolution. / Depending on the required application field, the solutions of a geometric constraints system (GCS) are either : – symbolic and exact such as construction plans, providing all the solutions, obtained by applying geometric rules. Many problems, mostly in a 3D context, resist to this approach ; – or numerical and approximated : they are the solutions of a system of equations built from the constraints, provided by generical numerical methods that are efficient when only one solution is sought. However, searching all the solutions leads to an exponential computation cost, due to the nature of problems. Continuation methods, also called homotopic methods, find all the solutions of a polynomial system. Using them to solve systems of equations associated to systems of constraints is nevertheless costly. Moreover, combining them with geometric reasoning is a challenge, because they act in a projective complex space and not in the realizations space. The aim of this work is to specialize a continuation method to GCS. Geometry is exploited to simplify and justify its adaptation in the space of realizations, so allowing geometric reasoning. Cases where the connected components of the solution space of a problem have heterogeneous dimensions are addressed. The method discussed here provides in a first step solutions that are similar to a sketch drawn by the user. Then a procedure is proposed to search new solutions. Its iterative nature seems to make the exponential complexity of this task bearable. A new decomposition method is proposed, that restrains the resolution cost.

En chirurgie mini-invasive guidée par l’image, une planification préopératoire précise des trajectoires des outils chirurgicaux est un facteur clé pour une intervention réussie. Cependant, une planification efficace est une tâche difficile, qui peut être considérablement améliorée en considérant différents facteurs contributifs tels que les déformations biomécaniques intra-opératoires, ou en introduisant de nouvelles techniques d'optimisation. Dans ce travail, nous nous concentrons sur deux aspects. Le premier aspect porte sur l'intégration de la déformation intra-opératoire dans le processus de planification de trajectoire. Nos méthodes combinent des techniques d'optimisation géométrique à base de simulations biomécaniques. Elles sont caractérisées par un certain niveau de généralité, et ont été expérimentées sur deux types d’interventions chirurgicales: les procédures percutanées pour l'ablation de tumeurs hépatiques, et la stimulation cérébrale profonde en neurochirurgie. Deuxièmement, nous étudions, mettons en œuvre, et comparons plusieurs approches d'optimisation en utilisant des méthodes qualitatives et quantitatives, et nous présentons une méthode efficace d'optimisation évolutionnaire multicritères à base de Pareto qui permet de trouver des solutions optimales qui ne sont pas accessibles par les méthodes existantes. / In image-guided minimally invasive surgery, a precise preoperative planning of the surgical tools trajectory is a key factor to a successful intervention. However, an efficient planning is a challenging task, which can be significantly improved when considering different contributing factors such as biomechanical intra-operative deformations, or novel optimization techniques. In this work, we focus on two aspects. The first aspect addresses integrating intra-operative deformation to the path planning process. Our methods combine geometric-based optimization techniques with physics-based simulations. They are characterized with a certain level of generality, and are experimented on two different surgical procedures: percutaneous procedures for hepatic tumor ablation, and in neurosurgery for Deep Brain Stimulation (DBS). Secondly, we investigate, implement, and compare many optimization approaches using qualitative and quantitative methods, and present an efficient evolutionary Pareto-based multi-criteria optimization method which can find optimal solutions that are not reachable via the current state of the art methods.