Un système GALS (Globalement Asynchrone, Localement Synchrone) est un ensemble de composants synchrones qui évoluent en même temps, chacun à propre rythme, et qui communiquent de manière asynchrone. Cette thèse propose un environnement formel de modélisation et de vérification dédié aux systèmes GALS, en se focalisant sur le comportement asynchrone.Notre environnement s’appuie sur un langage formel que nous avons conçu nommé GRL (GALS Représentation Language). GRL permet la spécification comportementale des composants synchrones, de la communication asynchrone, et des contraintes sur les rythmes des composants ainsi que sur les valeurs que prennent les entrées des composants. Pour analyser les spécifications GRL, nous utilisons CADP, une boîte à outils logicielle permettant la vérification de processus concurrents asynchrones par des techniques d'exploration d’espaces d’états. Dans ce but, nous avons défini une traduction de GRL vers LNT, un langage de spécification supporté par CADP. La traduction est implémentée dans un outil appelé GRL2LNT, permettant ainsi la génération automatique d’espaces d'états à partir de spécifications GRL.Pour permettre la vérification formelle des spécifications GRL, nous avons conçu un langage de propriétés nommé muGRL, qui est interprété sur les espaces d’états de GRL. Le langage muGRL est basé sur un ensemble de patrons qui capturent les propriétés des systèmes concurrents et des systèmes GALS, réduisant ainsi la complexité d'utiliser les logiques temporelles classiques. La sémantique de muGRL est définie par traduction vers MCL, le langage de logique temporelle fourni par CADP. Enfin, nous illustrons l’usage de GRL, muGRL et CADP pour la modélisation et la vérification d’applications GALS concrètes, comprenant des études de cas industrielles. / A GALS (Globally Asynchronous, Locally Synchronous) system consists of several synchronouscomponents that evolve concurrently, each with its own pace, and communicatealtogether asynchronously. This thesis proposes a formal modelling and verificationframework dedicated to GALS systems, with a focus on the asynchronous behaviour.As a cornerstone of our framework, we have designed a formal language, named GRL(GALS Representation Language). GRL enables the behavioural specification of synchronouscomponents, asynchronous communication, and constraints involving bothcomponent paces and the data carried by component inputs. To analyse GRL specifications,we took advantage of the CADP software toolbox for the verification of asynchronousconcurrent processes, using state space exploration techniques. For this purpose,we defined a translation from GRL to the LNT specification language supportedby CADP. The translation was implemented by a tool named GRL2LNT, thus enablingstate spaces to be automatically derived from GRL specifications.To enable the formal verification of GRL specifications, we designed a property specificationlanguage, named muGRL, which is interpreted on GRL state spaces. The muGRLlanguage is based on a set of patterns capturing properties of concurrent and GALSsystems, which reduces the complexity of using full-fledged temporal logics. The semanticsof muGRL are defined by a translation into the MCL temporal logic supported byCADP. Finally, we illustrated how GRL, muGRL, and CADP can be applied to modeland verify concrete GALS applications, including industrial case-studies.

Dans le cadre de la thèse portant sur l’optimisation et simulation de la chaîne logistique agricole, c'est l'activité de collecte qui est concernée, la période de moisson étant primordiale en matière de quantité et qualité de production, i.e. des revenus pour les agri-culteurs et des richesses pour le territoire. Plus spécifiquement, celle-ci implique les opérations de récolte, transport et stockage des céréales, réalisées par plusieurs exploitations agricoles, dispersées géographiquement. En vue d'aborder la complexité et la nature dyna-mique de la chaîne logistique d’une coopérative agricole française dans son intégralité, nous avons développé un système d'aide à la décision, qui s'inscrit dans la cadre de la recherche opérationnelle (RO) et plus précisément se réfère à l'optimisation linéaire, robuste et stochastique; la simulation de flux à évènements discrets; ainsi qu'à leur couplage. De plus, la synergie créée entre les outils de la RO, le système d’information géographique, la statistique inférentielle et prédictive rend le système d'aide à la décision compétitif et performant, capable de répondre convenablement au besoin de l’industriel / To overcome the new challenges facing agricultural sector, imposed by globalisation, changing market demands and price instability, the crop production supply chain must particularly be very reactive, flexible, with a high yield and at low cost. Its improving and eventual re-configuration can lead to an upgrade in efficiency, responsiveness, business integration and make it able to confront the market competitiveness. The thesis is thus placed in this particular context and aims to support decision making in crop harvesting activity, which is considered the pivotal stage in the cereal production circuit owing to its high cost and impact on the returns earned. Managing the harvest activity involves gathering, transportation and storage operations, performed by a collection of agricultural holdings geographically dispersed. Besides its practical relevance, this thesis forms part of the Operational Research (OR) and more specifically, refers to the linear and stochastic programming, discrete event simulation, and their coupling. In addition, the synergy created between OR, inferential and predictive statistics, geographical information system tools makes the decision support system competitive, efficient and responsive

Les travaux de cette thèse concernent la modélisation et l'optimisation de chaînes d’approvisionnement en biomasses pour de futures bio-raffineries. En effet, des chaînes d'approvisionnement efficaces sont essentielles pour fournir aux installations de conversion, de façon régulière, des quantités suffisantes de biomasse de qualité à des prix raisonnables. Le problème est tout d'abord décrit puis modélisé.Un modèle de réseau et un modèle de données sont ensuite développés pour permettre de décrire la structure de la chaîne d'approvisionnement et ses données, sans affecter le modèle mathématique sous-jacent. Ce dernier (MILP) combine pour la première fois divers aspects, soit originaux, soit gérés séparément dans la littérature. A partir des demandes de la raffinerie, une résolution exacte précise les activités logistiques dans le réseau et les équipements nécessaires, afin de minimiser le coût total composé des coûts de récoltes, de transport et de stockage. Des études de cas sont décrites pour illustrer ce modèle de planification tactique multi-biomasse et multi-période. Un modèle plus compact est aussi élaboré pour traiter des instances de très grandes tailles. Il est illustré par une étude de cas réelle pour une bio-raffinerie prévue près de Compiègne. Pour finir, les développements effectués pour la mise en place d’un prototype logiciel d’aide à la décision sont présentés et des recommandations d’un futur logiciel commercial sont proposées / The research works of this thesis address the problem of modeling and optimizing biomass supply chains for biorefineries. Indeed, efficient supply chains are essential to provide conversion facilities with sufficient quantities of quality biomass at reasonable prices. The problem is described and modeled.A network model and a data model are developed to allow to describe the structure of the supply chain and its data, without affecting the underlying mathematical model. The latter is a mixed-integer linear programming that combines for the first time various aspects, either original or tackled separately in the literature. For given refinery needs, its exact resolution by CPLEX specifies the logistic activities in the network (amounts harvested, baled, transported, stored etc.) and the necessary equipment, in order to minimize a total cost including harvesting costs, transport costs and storage costs. Case studies are described to illustrate this multi-biomass and multi-period tactical planning model.A more compact model is also elaborated to cope with large-scale instances. It is illustrated using a real case study for a bio-refinery planned near Compiègne, France.Finally, the developments conducted for the implementation of a prototype of decision-support application are presented and recommendations for coming to a commercial software are proposed

L’innovation technologique est considérée comme un élément clef dans la constitution des économies, dites du savoir, ou de la connaissance. Ce cadre économique stimule une forte croissance des investissements immatériels dans l’objectif de création de valeur et de construction d’un avantage compétitif défendable sur le long terme. Néanmoins, l’innovation est un processus continu qui requiert un horizon de long terme pour transformer l’ensemble des connaissances, et des efforts de Recherche et Développement (R&D) en un produit ayant de la valeur économique. La dimension temporelle de l’innovation technologique renforce son caractère risqué et augmente l’incertitude quant à sa réussite. De même, les problèmes d’asymétrie d’information créés par le processus d’innovation s’accentuent. Cette thèse s’intéresse à la relation entre le capital-connaissances et la performance financière des entreprises, dans un premier temps, pour se pencher ensuite sur la question de la valeur de marché de l’actif intangible. Pour ce faire, nous élaborons une base de données unique, à partir des brevets européens et proposons de nouvelles mesures qualitatives au capital intangible, basées sur les caractéristiques des brevets. Cette thèse mesure empiriquement la valeur économique du capital-connaissances représenté par sa « matière première », à savoir les dépenses R&D et par son « produit fini » à savoir les brevets. Nous construisons, également un indice composite de la qualité de l’innovation afin de mieux représenter la valeur privée de l’immatériel. Enfin, cette thèse s’intéresse à la question d’écart entre valeur comptable et valeur de marché des entreprises en présence d’investissements immatériels. Pour ce faire, elle contient une étude prévisionnelle et causale de la performance opérationnelle par les dépenses R&D et l’indice composite de qualité. Ce dernier est proposé en tant qu’outil non-financier d’analyse et de prévision de performance. / Technological innovation is considered as a key element in the knowledge-based economies, where the share of intangible assets continues to grow significantly. The development of innovation is enhanced mainly in the purpose of value creation and the obtaining of a competitive advantage. Nevertheless, innovating is a long process where the lag between the investments in Research and Development (R&D) activities, considered as its input, and the obtaining of a valuable output, often estimated by the patent application, is large. The long character is emphasized by the uncertainty and the riskiness of the process which are at the root of important problems of information asymmetry between investors and the insiders. This dissertation studies the impact of intangible investments on the financial performance of companies in Europe. Therefore, we use a unique database of European patents and suggest a set of qualitative measures to innovation, based on the patents’ attributes. Moreover, this thesis estimates the market value of intangibles as measured by the R&D expenses, the patent applications but also the qualitative attributes. In this framework, we construct a composite quality index of innovation in order to better estimate its private economic value. The increasing lag between financial and book values in the presence of R&D investments leads us to undertake a causal study of innovation on the financial performance of companies. We suggest our composite index as non-financial metric to predict the future earnings and examine the effect of R&D on the growth and volatility of future operating incomes.

No description available.

Les travaux de cette thèse s’articulent autour des « problèmes d’ordonnancement multiagent avec une fonction objectif globale ». Ces modèles considèrent différents agents associés à des sous-ensembles de travaux disjoints, chacun d’eux vise à minimiser un objectif qui ne dépend que de ses propres travaux. Un critère global est aussi considéré, qui est appliqué à la totalité des travaux. La résolution de ces problèmes revient à trouver les meilleurs compromis entre les critères des agents et le critère global. Ces problèmes sont une classe particulière des problèmes d’ordonnancement « multi-agents » qui ont connu une grande expansion, reflétant leurs intérêts dans le domaine de l’ordonnancement. / This thesis addresses the multi-agent scheduling problems with a global objective function. We consider the problems featured by various agents, each of which is associated with a distinct subset of jobs. Each agent aims at minimizing a certain objective function, which only operates on its assigned jobs. A global criterion associated with a global agent is applied on the whole set of the jobs. Solving these problems involves finding the best compromises between the requirements of agents and that of the global agent. These problems belong to a particular class of multi-criteria scheduling problems. Such a class has drawn a significant interest to researchers in the area of scheduling and operational research.

Pour accompagner le développement des fermes urbaines professionnelles et des circuits courts et de proximité dans les grandes métropoles, nous proposons des outils à base de programmes mathématiques d'aide à la conception de fermes maraîchères diversifiées ciblant les demandes de différents types de clients en fruits et légumes frais locaux. Les solutions techniques de culture en ville se développent rapidement, mais compte-tenu des contraintes fortes de la production agricole urbaine (foncier limité, coûts opérationnels élevés), la définition de modèles économiques viables pour des fermes pérennes est un vrai défi pour les maraîchers urbains. Trois modèles en programmation linéaire mixte sont présentés et confrontés aux résultats du terrain : un modèle de dimensionnement stratégique annuel, un modèle de sélection de la meilleure combinaison de clients et un modèle de dimensionnement stratégique pluri-annuel des fermes maraîchères. Des résultats numériques et les performances des modèles sont présentés à partir de cas concrets multi-produits, multi-techniques et multi-périodes. Nos contributions résident dans la prise en compte de la périssabilité des produits frais dans le dimensionnement stratégique des systèmes de production, incluant le dimensionnement de la main d’œuvre agricole. / To support the urban farm emergence trend in large metropolises, we propose decision support tools based on mathematical programs to design market gardening farms targetting the demands of different categories of clients in local fresh fruits and vegetables. Technical solutions develop rapdily, but the strong constraints linked to urban farming, such as limited surface and high operating costs, make difficult to define viable and sustainable business models for urban market gardeners. Three mixed integer linear programming models are presented: An annual strategic sizing model, a client combination selection model and a plurennial strategic sizing model for diversified fruit and vegetable farms. Numerical results and model performances are presented, based on multi-products, multi-techniques and multi-periods real cases. Our main contributions are the consideration of the perishable nature of fruits and vegetables in strategic production systems sizing models, including notably the investments and workforce sizing.

No description available.

No description available.

La mémoire transactionnelle est un mécanisme de plus en plus populaire pour la programmation parallèle et concurrente. Dans la plupart des implantations, l’emboîtement de transactions n’est pas possible ce qui pénalise la modularité. Plutôt que les transactions, qui sont un choix possible d’implantation, nous considérons directement la notion de section atomique. Dans un objectif d’améliorer la modularité et l’expressivité, nous considérons un langage impératif simple étendu avec des instructions de parallélisme avec lancement et attente de processus légers et une instruction de section atomique à portée syntaxique, depuis laquelle des processus légers peuvent s’échapper. Dans ce contexte notre première contribution est la définition précise de l’atomicité et de la bonne synchronisation. Nous prouvons que pour des traces bien formées, la dernière implique la forme forte de la première. Ceci est fait sur des traces d’exécution abstraites dans le sens où nous ne définissons par précisément la syntaxe et la sémantique opérationnelle d’un langage de programmation. Cette première partie de notre travail peut être considérée comme une spécification pour un tel langage. Nous avons utilisé l’assistant de preuve Coq pour modéliser et prouver nos résultats. Notre deuxième contribution est la définition formelle du langage Atomic Fork Join (AFJ). Nous montrons que les traces de sa sémantique opérationnelle vérifient effectivement les conditions de bonne formation définies précédemment. La troisième contribution est la compilation de programmes AFJ en programmes Lock Unlock Fork Join (LUFJ) un langage avec processus léger et verrous mais sans sections atomiques. Nous étudions la correction de la compilation de AFJ vers LUFJ. / Transactions are becoming a popular mechanism for parallel and concurrent programming. In most implementations the nesting of transactions is not supported which hinders modularity. Rather than transactions, which are an implementation choice, we consider directly the notion of atomic section. For the sake of modularity with we consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our first contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. This is done on execution traces without being specific to a language syntax and operational semantics. This first part of our work could be considered as a specification for the design and implementation of such a parallel language. A formalisation of our results in the Coq proof assistant is also available. Our second contribution is a formal definition of the Atomic Fork Join (AFJ) language and its operational semantics. We show that it indeed satisfies the conditions previously defined. The third contribution of our work is a compilation procedure of AFJ programs to programs another language with threads and locks but without atomic sections, named Lock Unlock Fork Join (LUFJ). We study the correctness of the compilation from AFJ to LUFJ.