Owing to advancements in component re-use technology, component-based software development (CBSD) has come a long way in developing complex commercial software systems while reducing software development time and cost. However, assembling distributed resource-constrained and safety-critical systems using current assembly techniques is a challenge. Within complex systems when there are numerous ways to assemble the components unless the software architecture clearly defines how the components should be composed, determining the correct assembly that satisfies the system assembly constraints is difficult. Component technologies like CORBA and .NET do a very good job of integrating components, but they do not automate component assembly; it is the system developer's responsibility to ensure thatthe components are assembled correctly. In this thesis, we first define a component-based system assembly (CBSA) technique called "Constrained Component Assembly Technique" (CCAT), which is useful when the system has complex assembly constraints and the system architecture specifies component composition as assembly constraints. The technique poses the question: Does there exist a way of assembling the components that satisfies all the connection, performance, reliability, and safety constraints of the system, while optimizing the objective constraint? To implement CCAT, we present a powerful framework called "CoBaSA". The CoBaSA framework includes an expressive language for declaratively describing component functional and extra-functional properties, component interfaces, system-level and component-level connection, performance, reliability, safety, and optimization constraints. To perform CBSA, we first write a program (in the CoBaSA language) describing the CBSA specifications and constraints, and then an interpreter translates the CBSA program into a satisfiability and optimization problem. Solving the generated satisfiability and optimization problem is equivalent to answering the question posed by CCAT. If a satisfiable solution is found, we deduce that the system can be assembled without violating any constraints. Since CCAT and CoBaSA provide a mechanism for assembling systems that have complex assembly constraints, they can be utilized in several industries like the avionics industry. We demonstrate the merits of CoBaSA by assembling an actual avionic system that could be used on-board a Boeing aircraft. The empirical evaluation shows that our approach is promising and can scale to handle complex industrial problems.

Combinatorial problems are ubiquitous in our society and solving such problems efficiently is often crucial. One technique for solving combinatorial problems is constraint-based local search. Its compositional nature together with its efficiency on large problem instances have made this technique particularly attractive. In this thesis we contribute to simplifying the solving of combinatorial problems using constraint-based local search. To provide higher-level modelling options, we introduce set variables and set constraints in local search by extending relevant local search concepts. We also propose a general scheme to follow in order to define what we call natural and balanced constraint measures, and accordingly define such measures for over a dozen set constraints. However, defining such measures for a new constraint is time-consuming and error-prone. To relieve the user from this, we provide generic measures for any set constraint modelled in monadic existential second-order logic. We also theoretically relate these measures to our proposed general scheme, and discuss implementation issues such as incremental algorithms and their worst-case complexities. To enable higher-level search algorithms, we introduce constraint-directed neighbourhoods in local search by proposing new constraint primitives for representing such neighbourhoods. Based on a constraint, possibly modelled in monadic existential second-order logic, these primitives return neighbourhoods with moves that are known in advance to achieve a decrease (or preservation, or increase) of the constraint measures, without the need to iterate over any other moves. We also present a framework for constraint-based local search where one can model and solve combinatorial problems with set variables and set constraints, use any set constraint modelled in monadic existential second-order logic, as well as use constraint-directed neighbourhoods. Experimental results on three real-life problems show the usefulness in practice of our theoretical results: our running times are comparable to the current state-of-the-art approaches to solving the considered problems.

Le raisonnement epistémique joue un rôle en théorie de la concurrence de plusieurs manières distinctes mais complémentaires; cette thèse en décrit trois. La première, et presque certainement la moins explorée jusqu'à présent, est l'idée d'utiliser les modalités épistémiques comme éléments d'un langage de programmation. La programmation logique émergea sous le slogan <> et dans le paradigme de la programmation concurrente par contraintes, le lien est manifeste de manière très claire. Dans la première partie de cette thèse, nous explorons le rôle des modalités épistémiques, ainsi que celui des modalités spatiales qui leur sont étroitement liées, en tant que partie intégrante du langage de programmation et non simplement en tant que partie du meta-langage du raisonnement à propos des protocoles. La partie suivante explore une variante de la logique épistémique dynamique adaptée aux systèmes de transitions étiquetés. Contrairement à la partie précédente, on serait tenté de croire que tout ce qu'on pouvait dire à ce sujet a déjà été dit. Cependant, le nouvel ingrédient que nous proposons est un lien étroit entre la logique épistémique et la logique de Hennessy-Milner, cette dernière étant \emph{la} logique des systèmes de transitions étiquetés. Plus précisement, nous proposons une axiomatisation et une preuve d'un théorème de complétude faible, ce qui est conforme au principe général qu'on utilise pour des logiques telles que la logique dynamique mais nécessite des adaptations non triviales. La dernière partie de la thèse se concentre sur l'étude d'agents en interaction dans les processus concurents. Nous présentons une sémantique des jeux pour l'interaction d'agents qui rend manifeste le rôle de la connaissance et du flux d'information dans les interactions entre agents, et qui permet de contrôler l'information disponible aux agents en interaction. Nous utilisons les processus comme support de jeu et définissons des stratégies pour les agents de telle sorte que deux agents qui interagissent conformément à leurs stratégies respectives déterminent l'exécution du processus, rempla{\c}cant ainsi l'ordonnanceur traditionnel. Nous démontrons que des restrictions différentes sur les stratégies réprésentent des quantités d'information différentes disponibles à l'ordonnanceur. Ces restrictions sur les stratégies ont un aspect épistémique explicite, et nous présentons une logique modale pour les stratégies et une caractérisation logique de plusieurs restrictions possibles sur les stratégies. Ces trois approches d'analyse et de représentation de l'information épistémique en théorie de la concurrence apportent une nouvelle manière de comprendre la connaissance des agents dans des processus conncurrents, ce qui est vital dans le monde d'aujourd'hui, dans lequel les systèmes distribués composés de multiples agents sont omniprésents.

This thesis focuses on improving the SAT solving technology. The improvements focus on two major subjects: sequential SAT solving and parallel SAT solving. To better understand sequential SAT algorithms, the abstract reduction system Generic CDCL is introduced. With Generic CDCL, the soundness of solving techniques can be modeled. Next, the conflict driven clause learning algorithm is extended with the three techniques local look-ahead, local probing and all UIP learning that allow more global reasoning during search. These techniques improve the performance of the sequential SAT solver Riss. Then, the formula simplification techniques bounded variable addition, covered literal elimination and an advanced cardinality constraint extraction are introduced. By using these techniques, the reasoning of the overall SAT solving tool chain becomes stronger than plain resolution. When using these three techniques in the formula simplification tool Coprocessor before using Riss to solve a formula, the performance can be improved further. Due to the increasing number of cores in CPUs, the scalable parallel SAT solving approach iterative partitioning has been implemented in Pcasso for the multi-core architecture. Related work on parallel SAT solving has been studied to extract main ideas that can improve Pcasso. Besides parallel formula simplification with bounded variable elimination, the major extension is the extended clause sharing level based clause tagging, which builds the basis for conflict driven node killing. The latter allows to better identify unsatisfiable search space partitions. Another improvement is to combine scattering and look-ahead as a superior search space partitioning function. In combination with Coprocessor, the introduced extensions increase the performance of the parallel solver Pcasso. The implemented system turns out to be scalable for the multi-core architecture. Hence iterative partitioning is interesting for future parallel SAT solvers. The implemented solvers participated in international SAT competitions. In 2013 and 2014 Pcasso showed a good performance. Riss in combination with Copro- cessor won several first, second and third prices, including two Kurt-Gödel-Medals. Hence, the introduced algorithms improved modern SAT solving technology.

No description available.

Le développement et l’utilisation de systèmes complexes multi-utilisateurs, ou encore la mise en réseau de systèmes d’observation ou d’information pose des problèmes complexes de partage de ressources entre les utilisateurs. La particularité de ces systèmes, impliquant plusieurs utilisateurs humains ou entités organisationnelles est que le partage des ressources doit satisfaire les préférences souvent antagonistes des utilisateurs et répondre à des exigences d’équité. Ce travail de thèse a pour objet l’étude des problèmes de partage de ressources indivisibles entre des agents ayant des préférences complexes sur ces ressources.Nous nous intéressons plus particulièrement à la modélisation de problèmes de partage en univers risqué.En effet, dans de nombreux problèmes d’allocation de ressources réels, la part revenant réellement à chaque agent après le partage de la ressource dépend de facteurs exogènes. C’est le cas par exemple dans les systèmes d’observation (satellitaires, capteurs embarqués,...), dans lesquels la réalisation d’une requête donnée dépend non seulement des conditions climatiques sur le secteur à observer, mais aussi du bon fonctionnement du capteur, de l’absence de brouillage du signal, etc. L’introduction de risque dans les problèmes de partage implique la redéfinition des notions classiques de choix social (utilité, absence d’envie, ...), et l’agrégation collective des préférences des agents s’en trouve compliquée. Au cours de ce travail de thèse, nous nous sommes tout d’abord intéressés à l’étude de cette extension au risque du formalisme associé aux problèmes de partage classiques : nous proposons un modèle simple de problèmes de partages de biens indivisibles en présence de risque, toutefois assez général pour rester proche des applications réelles considérées, et nous introduisons une extension générale des méthodes d’évaluation non risquées pour de tels partages. La seconde partie de ce travail de thèse porte sur l’algorithmique associée à ces problèmes, dont la résolution est notablement complexifiée par la présence de ressources risquées. Pour plusieurs critères d’évaluation (choisis car visant à garantir une certaine équité des solutions qu’ils suggèrent), nous proposons des algorithmes de résolution exacte et approchée des problèmes de partage associés. / The development and use of complex multi-user systems, or the networking of observation ou information systems raises complex resource allocation problems. The particularity of these systems, which involve several human users or organisational entities, rests in the fact that the share of resources must satisfy the often conflicting preferences of users and comply with equity exigences. This thesis deals with the problem of fairly allocating indivisible goods to a set of agents having complex preferences over these goods.We are more particularly interested in the modeling of fair allocation problems in a risky setting. In numerous real-world resource allocation problems, the actual share each agent receives after the allocation often depends on exogenous factors. This is for instance the case with the observation systems (satellites, embedded sensons, etc.) where the realisation of a request not only depends on weather conditions over the observation area, but also on the potential sensor malfunction, on the absence of jamming of the signal, etc. Introducing the risk in allocation problems implies the redefinition of classical social choice notions such as utility or envy-freeness for instance, and the collective aggregation of agents preferences becomes more complicated. We have studied in this thesis the extension of allocation problem formalism to a risky setting : we present a simple model for risky indivisible goods allocation problems, yet general enough to encompass most of the real-world applications, and we introduce a general extension of risk-free evalution methods for such allocations. The second part of the work concerns the algorithmical issues related to theses problems, whose resolution is significantly complexified because of the risky setting. Forseveral evaluation criteria (selected for the equity of the solutions they suggest) we present both exact and approached resolution algorithms for the related allocation problems.

The main result is a new original algorithm: CONDOR ("COnstrained, Non-linear, Direct, parallel Optimization using trust Region method for high-computing load, noisy functions"). The aim of this algorithm is to find the minimum x* of an objective function F(x) (x is a vector whose dimension is between 1 and 150) using the least number of function evaluations of F(x). It is assumed that the dominant computing cost of the optimization process is the time needed to evaluate the objective function F(x) (One evaluation can range from 2 minutes to 2 days). The algorithm will try to minimize the number of evaluations of F(x), at the cost of a huge amount of routine work. CONDOR is a derivate-free optimization tool (i.e. the derivatives of F(x) are not required. The only information needed about the objective function is a simple method (written in Fortran, C++,) or a program (a Unix, Windows, Solaris, executable) which can evaluate the objective function F(x) at a given point x. The algorithm has been specially developed to be very robust against noise inside the evaluation of the objective function F(x). This hypotheses are very general, the algorithm can thus be applied on a vast number of situations. CONDOR is able to use several CPU's in a cluster of computers. Different computer architectures can be mixed together and used simultaneously to deliver a huge computing power. The optimizer will make simultaneous evaluations of the objective function F(x) on the available CPU's to speed up the optimization process. The experimental results are very encouraging and validate the quality of the approach: CONDOR outperforms many commercial, high-end optimizer and it might be the fastest optimizer in its category (fastest in terms of number of function evaluations). When several CPU's are used, the performances of CONDOR are currently unmatched (may 2004). CONDOR has been used during the METHOD project to optimize the shape of the blades inside a Centrifugal Compressor (METHOD stands for Achievement Of Maximum Efficiency For Process Centrifugal Compressors THrough New Techniques Of Design). In this project, the objective function is based on a 3D-CFD (computation fluid dynamic) code which simulates the flow of the gas inside the compressor. / Doctorat en sciences appliquées / info:eu-repo/semantics/nonPublished

Dans ce travail, une étude est réalisée sur le développement d'une méthodologie permettant la génération et l'évaluation de nouvelles trajectoires de valorisation pour des déchets. Ainsi, pour répondre à cette problématique, trois sous problèmes ont été identifiés. Le premier concerne un cadre de modélisation permettant la représentation structurée et homogène de chaque trajectoire, ainsi que les indicateurs choisis pour l'évaluation de ces dernières, permettant une sélection ultérieure. Le deuxième se concentre sur le développement d'une méthodologie puis la réalisation d'un outil permettant la génération de nouvelles trajectoires en s'appuyant sur d'autres connues. Enfin, le dernier sous problème concerne le développement d'un second outil développé pour modéliser et estimer les trajectoires générées. La partie de création d'un cadre de modélisation cherche à concevoir des structures globales qui permettent la catégorisation des opérations unitaires sous plusieurs niveaux. Trois niveaux de décomposition ont été identifiés. La Configuration générique de plus haut niveau, qui décrit la trajectoire sous de grandes étapes de modélisation. Le second niveau, Traitement générique propose des ensembles de structures génériques de traitement qui apparaissent régulièrement dans les trajectoires de valorisation. Enfin, le plus bas niveau se focalise sur la modélisation des opérations unitaires. Un second cadre a été créé, plus conceptuel et comportant deux éléments : les blocs et les systèmes. Ces cadres sont ensuite accompagnés par un ensemble d'indicateurs choisis à cet effet. Dans une volonté d'approche de développement durable, un indicateur est sélectionné pour chacune de des composantes : économique, environnemental et social. Dans notre étude, l'impact social se limite à l'estimation du nombre d'emplois créés. Afin de calculer cet indicateur, une nouvelle approche se basant sur les résultats économiques d'une entreprise a été proposée et validée.L'outil de génération de nouvelles trajectoires s'appuie sur l'utilisation de la connaissance en utilisant un système de raisonnement à partir de cas (RàPC). Pour être adapté à notre problématique, la mise en œuvre de ce dernier a impliqué la levée de plusieurs points délicats. Tout d'abord, la structuration des données et plus largement la génération de cas sources sont réalisées par un système basé sur des réseaux sémantiques et l'utilisation de mécanismes d'inférences. Le développement d'une nouvelle méthode de mesure de similarité est réalisé en introduisant la notion de définition commune qui permet de lier les états, qui sont des descriptions de situations, à des états représentant des définitions générales d'un ensemble d'états. Ces définitions communes permettent la création d'ensembles d'états sous différents niveaux d'abstraction et de conceptualisation. Enfin, un processus de décompositions des trajectoires est réalisé afin de résoudre un problème grâce à la résolution de ses sous-problèmes associés. Cette décomposition facilite l'adaptation des trajectoires et l'estimation des résultats des transformations. Basé sur cette méthode, un outil a été développé en programmation logique, sous Prolog. La modélisation et l'évaluation des voies de valorisation se fait grâce à la création d'outil spécifique. Cet outil utilise la méta-programmation permettant la réalisation dynamique de modèle de structure. Le comportement de ces structures est régi par la définition de contraintes sur les différents flux circulants dans l'ensemble de la trajectoire. Lors de la modélisation de la trajectoire, ces contraintes sont converties par un parser permettant la réalisation d'un modèle de programmation par contraintes cohérent. Ce dernier peut ensuite être résolu grâce à des solveurs via une interface développée et intégrée au système. De même, plusieurs greffons ont été réalisés pour analyser et évaluer les trajectoires à l'aide des critères retenus. / In this work, a study is realised about the creation of a new methodology allowing the generation and the assessment of new waste recovery processes. Three elements are proposed for that. The first one is the creation of a modelling framework permitting a structured and homogeneous representation of each recovery process and the criteria used to asses them. The second one is a system and a tool generating new recovery processes from others known. Finally, the last element is another tool to model, to estimate and to asses the generated processes. The creation of a modelling framework tries to create some categories of elements allowing the structuring of unit operations under different levels of description. Three levels have been identified. In the higher level, the Generic operation which describes global structure of operations. The second one is Generic treatment which is an intermediate level between the two others. It proposes here too categories of operations but more detailed than the higher level. The last one is the Unit operation. A second framework has been created. It is more conceptual and it has two components : blocs and systems. These frameworks are used with a set of selected indicators. In a desire of integrating our work in a sustainable development approach, an indicator has been chosen for each of its components: economical, environmental and social. In our study, the social impact is limited to the number of created jobs. To estimate this indicator, we proposed a new method based on economical values of a company. The tool for the generation of new waste recovery processes used the methodology of case-based reasoning CBR which is based on the knowledge management. Some difficult points are treated here to adapt the CBR to our problem. The structuring of knowledge and generally the source case generation is realised by a system based on connections between data and the use of inference mechanisms. The development of a new method for the similarity measure is designed with the introduction of common definition concept which allows linking states, simply put description of objects, to other states under different levels of conceptualizations and abstractions. This point permits creating many levels of description. Finally, recovery process is decomposed from a main problem to some sub-problems. This decomposition is a part of the adaptation mechanism of the selected source case. The realisation of this system is under logic programming with Prolog. This last one permits the use of rules allowing inferences and the backtracking system allowing the exploration to the different possible solution. The modelling and assessment of recovery processes are done by a tool programmed in Python. It uses the meta-programming to dynamically create model of operations or systems. Constraint rules define the behaviour of these models allowing controlling the flux circulating in each one. In the evaluation step, a parser is used to convert theses rules into a homogeneous system of constraint programming. This system can be solved by the use of solvers with an interface developed for that and added to the tool. Therefore, it is possible for the user to add solvers but also to add plug-ins. This plug-ins can make the assessment of the activity allowing to have different kinds of evaluation for the same criteria. Three plug-ins are developed, one for each selected criterion. These two methods are tested to permit the evaluation of the proposed model and to check the behaviour of them and their limits . For these tests, a case-base on waste has been created Finally, for the modelling and assessment tool, a study case about the recovery process of used tyres in new raw material is done.

The central theme of the thesis is to study linear and non linear SVM formulations in the presence of uncertain observations. The main contribution of this thesis is to derive robust classfiers from partial knowledge of the underlying uncertainty. In the case of linear classification, a new bounding scheme based on Bernstein inequality has been proposed, which models interval-valued uncertainty in a less conservative fashion and hence is expected to generalize better than the existing methods. Next, potential of partial information such as bounds on second order moments along with support information has been explored. Bounds on second order moments make the resulting classifiers robust to moment estimation errors. Uncertainty in the dataset will lead to uncertainty in the kernel matrices. A novel distribution free large deviation inequality has been proposed which handles uncertainty in kernels through co-positive programming in a chance constraint setting. Although such formulations are NP hard, under several cases of interest the problem reduces to a convex program. However, the independence assumption mentioned above, is restrictive and may not always define a valid uncertain kernel. To alleviate this problem an affine set based alternative is proposed and using a robust optimization framework the resultant problem is posed as a minimax problem. In both the cases of Chance Constraint Program or Robust Optimization (for non-linear SVM), mirror descent algorithm (MDA) like procedures have been applied.

Cette thèse se situe dans le contexte de la programmation par contraintes (CP). Plus précisément, nous nous sommes intéressés au problème de satisfaction de contraintes pondérées (WCSP). De nombreuses approches ont été proposées pour traiter ce problème d’optimisation. Les méthodes les plus efficaces utilisent des cohérences locales souples sophistiquées comme par exemple la cohérence d’arc directionnelle complète FDAC∗, la cohérence d’arc directionnelle existentielle EDAC∗, etc. Établies grâce à des opérations de transferts de coût préservant l’équivalence des réseaux, l’utilisation de ces cohérences permet généralement d’accélérer la résolution en réduisant l’espace de recherche via la suppression de valeurs et le calcul de bornes inférieures utiles en pratique. Cependant, l’utilisation de ces méthodes pose un problème lorsque l’arité des contraintes augmente de manière significative. L’efficacité des techniques du cadre du problème de satisfaction de contraintes (CSP) étant avérée, nous pensons que l’intégration de techniques CSP peut être très utile à la résolution d’instances WCSP. Dans cette thèse, nous proposons tout d’abord un algorithme de filtrage établissant la cohérence d’arc souple généralisée GAC∗ sur des contraintes tables souples de grande arité. Cette approche combine la technique de réduction tabulaire simple (STR), issue du cadre CSP, et le principe de transfert de coûts. Notre approche qui est polynomiale calcule efficacement pour chaque valeur les coûts minimaux dans les tuples explicites et implicites des contraintes tables souples. Ces coûts minimaux sont ensuite utilisés pour transférer les coûts afin d’établir GAC∗. Dans un second temps, nous proposons une approche alternative aux méthodes de résolution habituelles du problème WCSP. Elle consiste à résoudre une instance WCSP en résolvant une séquence d’instances CSP classiques obtenues depuis cette instance WCSP. À partir d’une instance CSP dans laquelle toutes les contraintes de l’instanceWCSP d’origine sont durcies au maximum, les instances CSP suivantes correspondent à un relâchement progressif de contraintes de l’instance WCSP déterminées par l’extraction de noyaux insatisfaisables minimaux (MUC) depuis les réseaux insatisfaisables de la séquence. Nos résultats expérimentaux montrent que notre première approche est compétitive avec l’état de l’art, tandis que la deuxième représente une approche alternative aux méthodes de résolutionhabituelles d’instances WCSP. / This thesis is in the context of constraint programming (CP). Specifically, we are interested in the Weighted Constraint Satisfaction Problem (WCSP). Many approaches have been proposed to handle this optimization problem. The most effective methods use sophisticated soft local consistencies such as, for example, full directional arc consistency FDAC∗, existential directional arc consistency EDAC∗, etc. Established by equivalence preserving transformations (cost transfer operations), the use of these consistencies generally allows both to accelerate the resolution by reducing the search space through the elimination of values and to compute lower bounds useful in practice. However, these methods reach theirlimits when the arity of constraints increases significantly. The techniques of the Constraint Satisfaction Problem framework (CSP) having proved efficienty, we believe that the integration of CSP techniques can be very useful for solving WCSP instances. In this thesis, we first propose a filtering algorithm to enforce a soft version of generalized arc consistency (GAC∗) on soft table constraints of large arity. This approach combines the techniques of simple tabular reduction (STR), from the CSP framework, with the techniques of cost transfer. Our approach, proved polynomial, efficiently calculates for each value the minimum cost of the explicit and implicit tuples from soft table constraints. The minimum costs are thenused to transfer costs to establish GAC∗. In a second step, we propose an alternative approach to the usual techniques to solve WCSP. The principle is to solve a WCSP instance by solving a sequence of classical CSP instances obtained from this WCSP instance. From a CSP instance containing all the constraints hardened to the maximum from the WCSP instance, the next CSP instances correspond to a progressive relaxation of constraints defined by extraction of minimal unsatisfiable cores (MUC) from unsatisfiable networks of the sequence. Our experimental results show that our first approach is competitive with the state-of-the-art, whereas the second one represents an alternative approach to the usual methods to solve WCSP instances.