No description available.

Diversos treballs en el camp de la modelització d'aplicacions cientí¬fiques, tecnològiques i industrials requereixen la resolució de sistemes d'equacions lineals i problemes lineals de mí¬nims quadrats densos de gran dimensió. Davant tals necessitats, l'objectiu plantejat en aquesta tesi ha estat dissenyar, desenvolupar i avaluar una col·lecció de rutines altament eficients per a resoldre sistemes d'equacions lineals i problemes lineals de mínims quadrats de dimensió elevada (matrius amb desenes de milers de files/columnes) sobre arquitectures actuals, fent ús de tècniques out-of-core. Les tècniques out-of-core estenen la jerarquia de memòria per a abastar el nivell de l'emmagatzematge secundari, fent possible la resolució de sistemes d'equacions lineals densos de gran dimensió en plataformes amb una memòria principal de grandària reduïda. En aquesta tesi s'exploten, a més, les característiques dels processadors actuals com les arquitectures multihebra i els processadors gràfics.

Aquest treball de tesi s'adreça a la indústria de procés químic d'operació discontínua tot i que també pot resultar profitós per altres situacions de fabricació per lots. Aquests tipus d'indústries són molt variats i s'inclouen en sectors com el de la química fina, el farmacèutic, l'agroalimentari i, en definitiva, l'elaboració d'especialitats. La seva importància econòmica rau tant en el seu significatiu volum de producció com en l'alt valor afegit que sovint tenen els productes.L'objecte de l'estudi és la gestió dels recursos de fabricació i l'optimització de l'operació de la planta per tal d'ajustar la producció resultant als requeriments de la demanda. La natura discontínua i dinàmica dels processos que hi tenen lloc reclama la presa de decisions en termes d'assignació de tasques a equips (reactors, filtres i altres aparells), de seqüenciació de productes i temporització de les operacions. Es tracta, doncs, d'un problema de programació d'activitats.El primer pas vers la solució d'aquest problema és la modelització del sistema estudiat. Aquest treball proposa un model d'operació detallat que inclou, a més de la compartició per part dels diferents productes de recursos generals (temps, equips, serveis...), aspectes més específics de la indústria química. Són les necessitats de transferència i emmagatzamatge de productes, tant intermedis com acabats, de natura molt probablement fluïda. I són també, les tasques de preparació i neteja que, depenent de la seqüència de productes, cal aplicar als equips emprats.La modelització de l'emmagatzemament també considera la possible inestabilitat de certs intermedis i la conseqüent limitació de l'espera abans de ser processats. De fet, la modelització incorpora un nou esquema conceptual que permet la segmentació de les receptes dels diferents productes en sèries de tasques lligades als intermedis estables. Llavors, la descripció d'un programa d'operacions complex mitjançant una sèrie d'ordres de fabricació d'aquests intermedis proporciona una notable simplificació del problema que redueix el número de restriccions a considerar i facilita el procediment d'optimització.L'optimització mitjançant mètodes rigorosos ja establerts només resulta indicada per problemes molt simples en comparació amb el que es planteja en aquest treball. És per això que s'ha desenvolupat una metodologia heurística general que permet abordar aquest problema patró sota les diferents circumstàncies de cada cas particular. En una primera part es procedeix a la generació d'alternatives de producció considerant els casos possibles i eliminant els ineficients sota una sèrie de criteris preestablerts. Aquestes alternatives s'expressen com seqüències de fabricació d'intermedis estables i posteriorment poden ser millorades sota diferents objectius bé manualment o bé emprant mètodes sistemàtics.La validació de la metodologia proposada és possible gràcies a la comparació amb casos de la literatura. En proposar exemples de major complexitat, la utilització de mètodes estocàstics es demostra molt eficient per resoldre problemes per als quals és difícil trobar regles de solució. Llavors, la validació d'aquest casos és possible estadísticament.En conclusió, d'aquest treball en resulta una metodologia general i flexible que s'adapta a la majoria de característiques d'un tipus de problemes que, de moment i en última instància, han de ser resolts de manera particular. La seva complexitat continua reclamant la nostra intuïció. / This thesis concerns batch chemical process industries, although it may be of interest in other batch processing areas. This kind of industry is diverse and includes a variety of sectors such as fine chemicals, pharmaceuticals, food and agriculture industry and speciality manufacturing. The economical significance of this industrial activity resides on both, its large production volume and its high added value. The thesis is aimed at studying the management of limited resources and the optimization of plant operation in order to have the production meet the demand requirements. The inherent discontinuous and dynamic nature of this kind of processes needs decision-making in terms of unit-to-task assignment (reactors, filters and other apparatuses), in terms of product sequencing and in terms of operation timing. The first step towards the solution of this problem is system modelling. This work proposes a detailed operation model that includes the general sharing of resources (time, equipment, utilities, etc.), as well as more specific aspects related to the chemical industry. These aspects are the special needs for material transfer and storage, both final and intermediate, which are likely to be of fluid nature. Additionally, these aspects also include the special set-up and cleaning tasks that the equipment units require depending on the sequence of tasks performed.Storage modelling also considers the different stability of the intermediate substances and the resulting limitation of the waiting time before processing. Thus, the modelling incorporates a novel conceptual framework allowing the segmentation of the recipes into different series of tasks defined by the stable intermediate products. Hence, the description of a complex operation schedule by a sequence of production orders related to these intermediate products allows a significant problem simplification, which results in the reduction of the number of constraints to be considered and enhances the performance of the search. Optimization via established rigorous methods is only suitable for problems simpler than those addressed in this thesis. This is the reason for the development of a general heuristic methodology. The first part generates production alternative paths through an enumerative procedure that eliminates inefficient options according to given pre-established criteria. These alternative paths are characterized as production sequences of storable intermediate products that are next improved regarding different objective functions either manually or automatically.The validation of the proposed methodology is achieved through a comparative study using cases reported in the literature. For those more complex cases, the use of stochastic methods has demonstrated to be very effective when scheduling rules are not available. For these cases, the assessment and validation is achieved through statistical analysis.In conclusion, this thesis results in a general and flexible methodology that accommodates the most of the features of a kind of scheduling and planning problems that finally require particular solution strategies. The more complex the problem, the more the human intuition is to some extend still required.

A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKS En el desarrollo formal de software, la especificación formal se utiliza con fines de verificación y validación. Se han definido diferentes tipos de especificaciones formales. En esta tesis nos centraremos en especificaciones algebraicas. Este tipo de especificaciones formales son especificaciones axiomáticas, que suelen definirse en un lenguaje de especificación que incluye diferentes operadores de estructuración. La semántica de estos operadores se define de una forma que sea lo más independiente posible de la lógica de especificación o institución. Otra etapa fundamental en métodos formales es el diseño de software. Las tareas básicas que suelen realizarse durante esta etapa son la deducción de propiedades a partir de una especificación, el refinamiento de especificaciones o verificar que un programa satisface una especificación. Entendemos por entorno de diseño algebraico a un formalismo que incluye la definición de un lenguaje de especificación algebraica con semántica formal y la definición implícita o explícita de, al menos, las dos primeras de las tres tareas de diseño mencionadas anteriormente. Es importante que la definición de los entornos de diseño algebraico sea tambien lo más independiente posible de la lógica del lenguaje de especificación y, si es el caso, que la definición sea para una clase arbitraria de lenguajes de programación. El entorno de diseño algebraico con el que trabajaremos en esta tesis está basado en un lenguaje de especificación muy sencillo que ha sido utilizado para dar semántica a otros lenguajes de especificación de más alto nivel. El principal objetivo de esta tesis es definir un marco formal que permite reusar demostradores de teoremas para teorías de tipos con tipos dependientes e inductivos para el desarrollo de demostradores de teoremas para entornos de diseño algebraico. El problema puede considerarse interesante por varios motivos. Primero, esperamos que el desarrollo de este tipo de herramientas incrementará el uso de este tipo de métodos formales. Segundo, la investigación a realizar es completamente diferente a los trabajos realizados anteriormente y por último, el trabajo requiere un conocimiento extenso de una familia de formalismos no standard que forman las diferentes teorías de tipos con tipos dependientes que se han definido. En esta tesis, primero presentamos de forma general, las características basicas y las aplicaciones de las diferentes teorías de tipos con tipos dependientes. Estudiamos con más detalle la teoría de tipos que vamos a utilizar en el resto de la tesis, y a continuación presentamos un nuevo principio de codificación de sistemas de demostración finitos para la teoría de tipos escogida que mejora algunas de las limitaciones de otros principios de codificación existentes.Con el fin de comparar de forma abstracta las diferentes semánticas dadas a ciertos operadores de comportamiento del lenguaje de especificación escogido, definimos una institución a la que denominamos institución algebraica de comportamiento. Esta institución es también útil para definir las formas normales de las especificaciones que son necesarias para definir cierta clase de sistemas de demostración. A continuación, presentamos diferentes sistemas de demostración para la deducción de propiedades a partir de especificaciones y para el refinamiento de especificaciones. La principal aportación en esta parteconsiste en rediseñar los sistemas de demostración que no es posible dar representaciones adecuadas en la teoría de tipos escogida por ser sistemas de demostración infinitarios.Finalmente, damos una representación en la teoría de tipos de los sistemas de demostración más significativos de nuestro entorno de diseño algebraico usando el nuevo principio de codificación presentado en la tesis. Esto nos permite reutilizar los demostradores de teoremas de la teoría de tipos escogida para el desarrollo de demostradores de teoremas del entorno de diseño algebraico escogido. A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKSIn software engineering, a formal specification of what a system has to do plays a crucial role in the software development process. Formality is required for verification and validation purposes. Different forms of formal specifications have been developed. This thesis concentrates on the algeraic approach to system specification. In essence, this approach can be characterized by:· Axiomatic specifications which consist of a signature together with a set of axioms in a specification logic which any implementation of the system with that specification has to satisfy.· Operations to combine and modify specifications from subspecifications with an algebraic semantics.· An abstract presentation of the semantics as independent as possible of the specification logic or institution.Another crucial step in the software development process is software design. Some of the usual tasks which are performed during software design are the following: deduction of properties from specifications, refinement of specifications and verification of a program with respect to a specification. We understand by an algebraic design framework a formalism which includes a formal definition of an algebraic specification language including a model-theoretic semantics and the implicit or explicit formal definition of at least the two first software design tasks. The definition of algebraic design frameworks should be for several specification logics or even better for an arbitrary but fixed institution, and if it is the case for an arbitrary class of programming languages. In the literature, there exists a large amount of algebraic specification languages and algebraic design frameworks. The algebraic design framework which we will work in this thesis will be based on a kernel and simple algebraic specification language. The main objective of this thesis is to give an approach to reuse theorem provers for type theories with dependent and inductive types for the development of theorem provers for algebraic design frameworks. The problem can be considered interesting for several reasons. First, we believe that the development of tools in type-theoretic theorem provers will help to spread the use of algebraic techniques. Note that these kind of theorem provers have been widely used and applied. Second, the work to be done is completely different to the work done before and finally this work requires a thorough understanding of a non-standard family of formalisms which are type theories. In this thesis, first we give an overall view of type theories together with their apllications and then we present a new principle of encoding in an expressive type theory which solves some of the limitations of previous principle of encodings. In order to give a generic presentation of the framework of ASL for different specification logics, we give an abstract semantic framework in which the semantics of the the behavioural operators of ASL can be uniformly instantiated in first-order and higher-order logic. We also redesign the different proof systems for deduction and refinement when it is not possible to give adequate encodings in the type theory because they are infinatary proof systems. In some cases, different solutions are given for first and higher-order logics. Finally, the main proof systems of the algebraic design framework for ASL have been encoded in UTT using the new principle of encoding presented in the thesis. This allows us to take advantage of the current implementation of theorem provers for UTT to implement proof checkers for the proof systems of our chosen algebraic design framework.

Els mètodes de punt interior per a programació lineal proporcionen algorismes de complexitat polinòmica, que els fa ser molt eficients en l’optimització a gran escala. Aquests algorismes utilitzen el mètode de Newton per a convertir les equacions d’òptim del problema, que són no lineals, en un sistema d’equacions lineals, que solen resoldre’s aplicant factorizacions de matrius esparses. En aquells casos particulars en els quals el problema té una estructura especial, com ara en els problemes d’optimització en xarxes multiarticle, es pot aprofitar per millorar l’eficiència de l’algorisme. Aquests problemes de xarxes pertanyen a la família més general de problemes primals bloc-angulars. El punt de partida d’aquesta tesi va ser un fet empíric: l’observació del millor comportament computacional d’un algorisme especialitzat de punt inferior per a problemes bloc-angulars quan en la funció objectiu figurem termes quadràtics. Aquest algorisme utilitza factoritzacions de matrius per resoldre la part de les equacions associades a la zarza i el mètode del gradient conjugat precondicional per resoldre les equacions asociadse a les restriccions d’acoblament. Llavors l’objectiu original va ser buscar alguna forma d’aproximar un problema lineal per un quadràtic de manera que s’explotés el fet experimental observat sense perjudicar la convergència del problema. Posteriorment el plantejament inicial es va amplificar amb el nou objectiu de demostrar la convergència del mètode, entre altres resultats teòrics. El marc teòric usat per poder formular matemàticament aquesta idea ha estat la regularització de la funció de barrera logarítmica associada al problema d’optimització, entenent com a tal la transformació de la funció de barrera original per una altra que inclou un terme quadràtic variable de pertorbació, que disminueix progressivament conforme l’algorisme s’atansa a l’òptim. Aqueste terme quadràtic converteix el problema lineal original en un de quadràtic, de forma que en les primeres iteracions aprofitem el comportament empíric abans esmentat i, a mesura que progressa l’algorisme, el terme quadràtic esdevé negligible, i el problema amb regularització quadràtica s’atansa al problema lineal original. La barrera regularitzada resulta ser auto-concordant, assegurant així la convergència del mètode de punt interior.

Antecedentes: aunque por estudios en animales se conoce que el incremento de la ingesta proteica favorece el crecimiento renal y que el Insulin-like Growth Factor (IGF-1) puede ser el mediador de este proceso, no existen ensayos clínicos controlados en humanos que aporten evidencia científica a estas teorías. Metodología: este ensayo multicéntrico Europeo (EU Childhood Obesity Project) examinó a los 6 meses de vida a 601 lactantes sanos asignados aleatoriamente durante las 8 primeras semanas de vida (mediana=14 días) a consumir una fórmula infantil con mayor o menor contenido proteicos. Estos lactantes fueron comparados con un grupo alimentado con lactancia materna. Conclusiones principales: a los 6 meses, la ingesta proteica se asociaba de forma directa al tamaño renal y corporal, así como la secreción de IGF-1. IGF-1 puede ser un mediador del crecimiento corporal y renal inducido por la proteína dietética, posiblemente mediante un mecanismo hiperplásico. . / Background: Protein intake has been associated with kidney growth and function in human observational studies, and Insulin-like Growth Factor (IGF-1) has been postulated as a mediator of this process. Although this mechanism has been shown by animal models, randomized control trials have not been published in healthy infants. Methods: this multicenter European clinical trial (EU Childhood Obesity Project) examined 601 healthy 6-month-old formula-fed infants randomly assigned within the first 8 weeks of life (median 14 days) to receive an infant formula with higher or lower protein content. For comparison, 204 breastfed infants were also followed. Conclusions: higher protein content of infant formula increases kidney size at 6 months of life, whereas a lower protein supply achieves a normal kidney size relative to healthy breastfed infants. Protein intake has a direct significant relation with IGF-1 secretion. IGF-1 is a mediator of body and kidney growth, induced by protein intake

No description available.

Aquest treball de tesis doctoral tracta de la Optimització de la fase d'engreix. L'objectiu és determinar les condicions d'enviament a sacrifici d'un lot d'animals des d'un punt de vista operatiu. En primer lloc es fa una anàlisi de la cadena de producció de carn porcina, resaltant-ne els canvis del sector que han influit en la fase d'engreixament. La conclusió d'aquesta anàlisi és el plantejament d'un model per prendre decisions degut al canvi de paradigma que s'evidencia: els productors de porcs en la fase d'engreix cal que orientin la gestió del paràmetres operatius i els productes finals a les exigències i gustos dels seus clients. Seguidament, es presenta el sistema d'ajut a la decisió basat en un model biològic que explica l'evolució de les variables productives (pes i consum de pinso). A més també prediu les variables associades a característiques de la canal, com són el percentatge de magre, la proporció de peces, el rendiment i el greix intramuscular. El sistema té en compte tres mercats de carn porcina alternatius: 1) basat en pes viu, 2) basat en mèrits de la canal (percentatge de magre) y 3) basat en el valor de les peces nobles resultants de l'especejament de l'animal. L'objetiu del sistema és determinar la millor estratègia d'enviament per a cadascun dels genotips que s'han estudiat (alternatives de producció) depenent del mercat on seran enviats els animals. A més, també ha estat estudiat l'efecte de la variabilitat biològica dels animals dins del lot sobre els valors econòmics. També s'ha considerat l'opció d'enviar els animals en diverses etapes per tal d'homogeneitzar el pes dels animals enviats. Aquest problema ha estat estudiat seguint l'enfocament de programació dinàmica. En els darrers capítols es presenten quatre aplicacions del model que s'han desenvolupat al llarg del treball. En un futur els mercats de carn porcina tindran la tendència a ser més definits, per tant la producció en la fase d'engreixament porcí hauria d'integrar i tenir en compte les demandes i les exigències del consumidor. / This PhD Thesis is related to optimisation of pig fattening phase under an operative point of view. Firstly it has been an analysis of the Pork Chain in order to establish a framework. The objective is to highlight the changes in the sector which have influenced on fattening phase. The result was the necessity of satisfying the consumer demands. In the following chapters a Decision Support was developed based on the consumers requirements. Based on a biological model, a managerial model has been developed to analyse the fattening phase. The decision support system takes into account three alternative pig meat markets: Live body weight pricing, carcass merit pricing, and components or cuts pricing system. Apart from the alternatives markets, its objective is to determine the best marketing strategy for each different genotypes (production alternatives) depending on the market where they will be sent. In addition, the effect of animal variability on economic figures has been studied. Also it has been considered the option of marketing the animals in different stages in order to homogenise the weight of animal sent. This problem has been treated under dynamic programming framework. In near future pig meat markets are going to be more defined, therefore the fattening phase of pork production must take consumer demands into account.

Java is a very commonly used computer programming language, although its use amongst the scientific and High Performance Computing (HPC) communities remains relatively low. In this thesis, the option of using Java for developing scientific applications intended for execution in HPC environments is investigated. The data reduction pipeline for the Gaia space astronomy mission is an example of a large software project that has been written in Java, and will run in HPC environments. The efficient execution of the Gaia data reduction pipeline was one of the main motivations behind this thesis, although this thesis largely remains a general investigation into the use of Java in HPC. HPC is a fast changing field, in terms of hardware, software, and the scale of the problems that are being tackled. Amongst the most significant trends in HPC in recent years have been the increase in the number of cores per computing node, and the increase in the size of datasets that must be processed. A significant challenge in HPC is ensuring that data is made available in a particular node, when a core is ready to process it, thereby avoiding deadtime and providing high throughput. One danger to throughput is a decrease in the performance of shared storage devices, as the number of concurrent processes that are accessing those devices increases. Given the trends mentioned above, efficient data communication is very important for many applications running in HPC environments. In this thesis, we present an investigation into the current options for providing efficient data communication to Java applications in HPC environments. We investigate a number of implementations of Message Passing in Java (MPJ) and compare their performance. We present a new communication middleware application, called MPJ-Cache. This middleware makes use of an underlying implementation of Message-Passing in Java (MPJ), and adds prefetching, caching, and file-splitting functionality. It presents application developers with a high-level API, thus providing high-performance, as well as enabling high productivity amongst application developers. We compare the aggregate data rate that can be achieved though the use of this middleware, against that which can be achieved though direct access of a high performance shared storage device (GPFS), while distributing data amongst the nodes of a computer cluster. The use of MPJ-Cache has shown to provide an aggregate data rate of up to 103Gbps. Java applications are executed within a Java Virtual Machine (JVM), which is a managed runtime environment. The execution of applications within such a runtime environment is very different from the execution of native code, that was compiled ahead-of-time. The Java runtime environment consists of several sophisticated components, including the core runtime system, a garbage collector and a Just-In-Time (JIT) compiler. Modern JVMs strive to provide out-of-the-box high-performance, however in some situations, users may want to tune the JVM to better suit the behaviour and needs of a particular application. In order to do this, a profile of the target application should be obtained.

Els paradigmes cel·lulars, com les xarxes neuronals cel·lulars (CNN, en anglès) i els autòmats cel·lulars (CA, en anglès), són una eina excel·lent de càlcul, al ser equivalents a una màquina universal de Turing. La introducció de la màquina universal CNN (CNN-UM, en anglès) ha permès desenvolupar hardware, el nucli computacional del qual funciona segons la filosofia cel·lular; aquest hardware ha trobat aplicació en diversos camps al llarg de la darrera dècada. Malgrat això, encara hi ha moltes preguntes a obertes sobre com definir els algoritmes d'una CNN-UM i com estudiar la dinàmica dels autòmats cel·lulars. En aquesta tesis es tracten els dos problemes: primer, es demostra que es possible acotar l'espai dels algoritmes per a la CNN-UM i explorar-lo gràcies a les tècniques genètiques; i segon, s'expliquen els fonaments de l'estudi dels CA per mitjà de la dinàmica no lineal (segons la definició de Chua) i s'il·lustra com aquesta tècnica ha permès trobar resultats innovadors. / Los paradigmas celulares, como las redes neuronales celulares (CNN, eninglés) y los autómatas celulares (CA, en inglés), son una excelenteherramienta de cálculo, al ser equivalentes a una maquina universal deTuring. La introducción de la maquina universal CNN (CNN-UM, eninglés) ha permitido desarrollar hardware cuyo núcleo computacionalfunciona según la filosofía celular; dicho hardware ha encontradoaplicación en varios campos a lo largo de la ultima década. Sinembargo, hay aun muchas preguntas abiertas sobre como definir losalgoritmos de una CNN-UM y como estudiar la dinámica de los autómatascelular. En esta tesis se tratan ambos problemas: primero se demuestraque es posible acotar el espacio de los algoritmos para la CNN-UM yexplorarlo gracias a técnicas genéticas; segundo, se explican losfundamentos del estudio de los CA por medio de la dinámica no lineal(según la definición de Chua) y se ilustra como esta técnica hapermitido encontrar resultados novedosos. / Cellular paradigms, like Cellular Neural Networks (CNNs) and Cellular Automata (CA) are an excellent tool to perform computation, since they are equivalent to a Universal Turing machine. The introduction of the Cellular Neural Network - Universal Machine (CNN-UM) allowed us to develop hardware whose computational core works according to the principles of cellular paradigms; such a hardware has found application in a number of fields throughout the last decade. Nevertheless, there are still many open questions about how to define algorithms for a CNN-UM, and how to study the dynamics of Cellular Automata. In this dissertation both problems are tackled: first, we prove that it is possible to bound the space of all algorithms of CNN-UM and explore it through genetic techniques; second, we explain the fundamentals of the nonlinear perspective of CA (according to Chua's definition), and we illustrate how this technique has allowed us to find novel results.