Current grid computing architectures have been based on cluster management and batch queuing systems, extended to a distributed, federated domain. These have shown shortcomings in terms of scalability, stability, and modularity. To address these problems, this dissertation applies architectural styles from the Internet and Web to the domain of generic computational grids. Using the REST style, a flexible model for grid resource interaction is developed which removes the need for any centralised services or specific protocols, thereby allowing a range of implementations and layering of further functionality. The context for resource interaction is a generalisation and formalisation of the Condor ClassAd match-making mechanism. This set theoretic model is described in depth, including the advantages and features which it realises. This RESTful style is also motivated by operational experience with existing grid infrastructures, and the design, operation, and performance of a proto-RESTful grid middleware package named DIRAC. This package was designed to provide for the LHCb particle physics experiment’s “off-line” computational infrastructure, and was first exercised during a 6 month data challenge which utilised over 670 years of CPU time and produced 98 TB of data through 300,000 tasks executed at computing centres around the world. The design of DIRAC and performance measures from the data challenge are reported. The main contribution of this work is the development of a REST model for grid resource interaction. In particular, it allows resource templating for scheduling queues which provide a novel distributed and scalable approach to resource scheduling on the grid.

The lack of a method for developing programs from Z specifications is a difficulty that is now widely recognised. As a contribution to solving this problem, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows its style and conventions. Other refinement techniques have been proposed for Z; ZRC builds upon some of them, but distinguishes itself in that it is completely formalised. As several other refinement techniques, ZRC is formalised in terms of weakest preconditions. In order to define the semantics of its language, ZRC-L, we construct a weakest precondition semantics for Z based on a relational semantics proposed by the Z standards panel. The resulting definition is not unexpected, but its construction provides evidence for its suitability and, additionally, establishes connections between predicate transformers and two different relational models. The weakest precondition semantics of the remaining constructs of ZRC-L justify several assumptions that permeate the formalisation of Morgan's refinement calculus. Based on the semantics of ZRC-L, we derive all laws of ZRC. Typically the refinement of a schema in ZRC begins with the application of a conversion law that translates it to a notation convenient for refinement, and proceeds with the application of refinement laws. The conversion laws of ZRC formalise the main strategies and rules of translation available in the literature; its set of refinement laws is extensive and includes support for procedures, parameters, recursion, and data refinement. Morgan and Back have proposed different formalisations of procedures and parameters in the context of refinement techniques. We investigate a surprising and intricate relationship between these works and the substitution operator that renames the free variables of a program, and reveal an inconsistency in Morgan's calculus, Back's approach does not suffer from this inconsistency, but he does not present refinement laws. We benefit from both works and use a model based on Back's formalism to derive refinement laws similar to those in Morgan's calculus. Furthermore, we derive additional laws that formalise Morgan's approach to recursion. Three case studies illustrate the application of ZRC. They show that ZRC can be useful as a technique of formal program development, but are by no means enough to ascertain the general adequacy of its conversion and refinement laws. Actually, since Z does not enforce a specific style of structuring specifications, it is likely that new laws will be proved useful for particular system specifications: two of our case studies exemplify this situation. Our hope is that ZRC and its formalisation will encourage further investigation into the refinement of Z specifications and the proper justification of any emerging strategies or techniques.

(Brief abstract written by the author in 2011 since I don't have the original to hand.) This thesis introduced much of the theory for Hoare's CSP, including the failures and failures-divergences model and methods of proving properties of processes based on metric, order and topological structures. The final chapter investigates the structures underlying operational semantics.

Orientador: Marcelo Messias / Banca: marcio Ricardo Alves Gouveia / Banca: Cristiane Nespoli Morelato França / Resumo: No presente trabalho estudamos um sistema de equações diferenciais ordinárias de um modelo biológico de câncer que apresenta caos. Para o estudo faz-se necessário o conhecimento a respeito de bifurcações, em especial a bifurcação de Hopf e a de período duplo ("flip"), também de uma noção básica de dinâmica simbólica. O modelo é analisado de duas formas. No decorrer da primeira análise são fixados os parâmetros envolvidos, deixando variar somente um deles, a taxa de crescimento das células saudáveis. Para determinado valor crítico deste parâmetro, em torno do ponto de equilíbrio de coexistência entre as três populações celulares em estudo (células saudáveis, células do sistema imune e células tumorais), ocorre o surgimento de um ciclo limite, originado de uma bifurcação de Hopf. Em seguida, há uma bifurcação de duplicação de período de tal ciclo limite, conduzindo as soluções ao comportamento caótico. Numa segunda abordagem, são variados dois parâmetros, a taxa de inativação das células efetoras pelas células tumorais e a taxa de inativação das células tumorais pelas células efetoras. Encontra-se um regime paramétrico no qual as soluções que possuem comportamento caótico têm suas trajetórias tendendo a um comportamento ordenado, o que é verificado através do cálculo da entropia topológica, expoentes de Lyapunov e previsibilidade. / Abstract: In this work we study a system of ordinary differential equations which represent a mathematical model of cancer which has chaotic dynamics. In the study we use the bifurcation theory, especially the Hopf bifurcation and the period doubling bifurcation (flip), we also use the basic notion of symbolic dynamics. The model is analyzed from two points of view. In the first one we consider all the parameters as being fixed and vary only one of them, which is related to the growth rate of the healthy cells. For a determined critical value of this parameter, a Hopf bifurcation occurs in the equilibrium point representing the coexistence of the three types of cells (healthy cells, immune system cells and tumor cells), giving rise to the existence of a limit cycle. Studying the continuation of this limit cycle, we detect the occurrence of a cascade of period doubling bifurcations which, in the limit, leads to the chaotic behaviour of the solutions. In a second analysis, we vary two of the parameters of the model, representing the inactivation of the immune system cells by the tumor cells and the inactivation of the tumor cells by the immune system cells. In this analysis we determined certain parameter values for which the solutions having chaotic behavior tend to a regular regime, which is obtained by the calculation of the topological entropy, the Lyapunov exponents and predictability. / Mestre

Made available in DSpace on 2014-06-11T19:27:08Z (GMT). No. of bitstreams: 0 Previous issue date: 2013-03-15Bitstream added on 2014-06-13T20:35:13Z : No. of bitstreams: 1 costa_cg_me_prud.pdf: 10846333 bytes, checksum: edd825f26c64cc382ef405066dbf048d (MD5) / Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP) / As equações diferenciais parciais hiperbólicas tem recebido uma atenção especial nos últimos anos devido sua grande aplicabilidade em diversas áreas da ciência e pelas dificuldades numéricas que elas impõem. O presente projeto leva em conta a importância do termo fonte e as implicações que isto representa na solução numérica das equações hiperbólicas, em especial nas leis de conservação. Todo o trabalho é focado no caso bidimensional das leis de conservação hiperbólicas, considerando termos fonte stiff. Este tipo de termo fonte impõe diferença de escala de propagação das ondas e das escalas advindas do próprio termo fonte. A equação hiperbólica com termo fonte deve ser tratada de forma especial. Utilizando os métodos mais recomendados na prática, resolvemos tal equação separando-a em duas ou mais partes, e depois acoplamos as partes na solução final. Os métodos utilizados em cada parte separada tem grande influência na solução... / The hyperbolic partial differential equations has had special attention in recent years due to their wide application in various areas of science and the numerical difficulties they impose. This project takes into account the importance of the font term and the implications this represents in the numerical solution of hyperbolic equations, especially in conservation laws. All work is focused on the case of two-dimensional hyperbolic conservation laws, considering the font terms stiff. This type of font term imposes difference in scale propagation of waves and those scales that comes from the font term. The hyperbolic equation with font term should be treated in a special way. Using the methods recommended in practice, we solve this equation by separating it into two or more parts, and then put the parties together in the final solution. The methods used... (Complete abstract click electronic access below)

Made available in DSpace on 2014-06-11T19:27:08Z (GMT). No. of bitstreams: 0 Previous issue date: 2013-04-24Bitstream added on 2014-06-13T18:55:34Z : No. of bitstreams: 1 merejolli_r_me_prud.pdf: 1357578 bytes, checksum: 415c634c0e40bf216c3855bc04b34cf3 (MD5) / Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP) / Neste trabalho é apresentado um método numérico para simular escoamentos viscoelásticos axissimétricos com superfícies livres modelados pela equação constitutiva PTT (Phan-Thien-Tanner). As equações governantes para escoamentos axissimétricos transientes incompressíveis de um fluido PTT são resolvidas utilizando o método de diferenças finitas numa malha deslocada. As derivadas temporais da equação do momento e da equação constitutiva são integradas pelo método de Euler explícito. Os termos convectivos são aproximados pelo método de alta ordem CUBISTA (Convergent and Universally Bounded Interpolation Scheme for the Treament of Advection), os termos difusivos e as derivadas espaciais são aproximados por diferenças centrais. O fluido é modelado utilizando a técnica Marker-and-Cell (MAC) o que permite visualizar e localizar a superfície livre do fluido. O método numérico descrito neste trabalho foi implementado na plataforma de alto desempenho denominada FREEFLOW-AXI e verificado comparando-se os resultados numéricos obtidos da simulação do escoamento totalmente desenvolvido em um tubo com a solução analítica deste problema. Foram obtidos alguns resultados numéricos para escoamentos axissimétricos com superfícies livres utilizando um fluido PTT, tais como, o impacto de uma gota esférica de fluido viscoelástico numa superfície rígida (Impacting Drop), o impacto de uma gota esférica numa superfície líquida (Splashing Drop) e o problema do inchamento do extrudado (Dieswell). Nestas simulações, o foco principal foi estudar numericamente os efeitos dos parâmetros do modelo PTT e nestes escoamentos / In this work is presented a numerical method for simulating axisymmetric viscoelastic free surface flows modeled by the constitutive equation PTT (Phan-Thien-Tanner). The governing equations for incompressible transient axisymmetric flows of a PTT fluid are solved using the finite difference method in a staggered grid. The time derivatives on momentum and constitutive equations are integrated by forward Euler method. The convective terms are approximated by the high order method CUBISTA (Convergent and Universally Bounded Interpolation Scheme for the Treament of Advection), the diffusive terms and the spatial derivatives are approximated by central differences. The fluid is modeled using the strategy “Marker-and-Cell” (MAC) which allows to view and locate the free surface of the fluid. The numerical method described in this work was implemented on the high performance platform called FREEFLOW-AXI and verified by comparing the numerical results of fully developed tube flow with the analytic solution of this problem. Some numerical results for axisymmetric free surface flows using a PTT fluid were obtained, such as, impacting drop, splashing drop and the dieswell problems. In these simulations, the numerical studies about the influence that the parameters of the PTT model and exert on the flows were the main focus

Made available in DSpace on 2014-06-11T19:27:09Z (GMT). No. of bitstreams: 0 Previous issue date: 2013-06-20Bitstream added on 2014-06-13T20:47:45Z : No. of bitstreams: 1 bender_c_me_prud.pdf: 610555 bytes, checksum: 8e81ee36de6af02140ca041f2ba2ee4b (MD5) / Este trabalho apresenta um estudo sobre a monotonicidade de zeros de polinômios ortogonais clássicos de variável contínua e de variável discreta em relação aos seus parâmetros. São também apresentados limitantes para os zeros de alguns destes polinômios / This work presents a study about the monotonicity of zeros of classical orthogonal polynomials of continuous and discrete variable with respect to its parameters. It is also given bounds for the zeros of some of these polynomials

Made available in DSpace on 2014-06-11T19:27:09Z (GMT). No. of bitstreams: 0 Previous issue date: 2013-06-05Bitstream added on 2014-06-13T19:06:50Z : No. of bitstreams: 1 verri_ja_me_prud.pdf: 7130871 bytes, checksum: 40212cfd999c344f6165b927a8d582c2 (MD5) / Nesta dissertação fazemos um estudo de modelos biológicos do tipo Lotka-Volterra, utilizando como ferramenta principal a teoria qualitativa das equações diferenciais ordinárias. Abordamos, no plano e no espaço, alguns modelos do tipo predador-presa. Analisamos os comportamentos das soluções sob a variação dos parâmetros e tratamos com detalhes a bifurcação de Hopf, que dá origem a uma órbita periódica isolada (ciclo limite). Estudamos também um teorema devido a Li e Muldowney [16] sobre a estabilidade global de um ponto de equilíbrio para um sistema x˙ = f(x), x ∈ Rn. Aplicamos este resultado no estudo de um modelo de HIV tridimensional, provando a estabilidade global de um ponto de equilíbrio, para certos valores dos parâmetros. Para o mesmo modelo, verificamos a ocorrência de uma dupla bifurcação de Hopf, que leva ao surgimento e posterior desaparecimento de um ciclo limite, ao variarmos um dos parâmetros envolvidos no sistema. As bifurcações de Hopf ocorrem simultaneamente à perda de estabilidade global do ponto de equilíbrio / In this work we present a study of biological models of Lotka-Volterra type, using as main tool the qualitative theory of ordinary differential equations. We analyze some two and three dimensional predator-prey models. The behavior of the solutions are studied under the variation of parameters and it is shown that a Hopf bifurcation occurs, leading to the creation of an isolated periodic orbit (limit cycle). We also study a theorem due to Li and Muldowney [16] about the global stability of an equilibrium point of a system x˙ = f(x), x ∈ Rn. We apply this result in the analysis of a three dimensional model of HIV with treatment, showing the global stability of an equilibrium point, for certain parameter values. For the same model, we prove the occurrence of two Hopf bifurcations, leading to the birth and subsequent death of a limit cycle, when we vary one of the parameters of the model. The Hopf bifurcations occurs simultaneously to the lack of global stability of the equilibrium point

Made available in DSpace on 2014-06-11T19:27:09Z (GMT). No. of bitstreams: 0 Previous issue date: 2013-09-06Bitstream added on 2014-06-13T18:55:35Z : No. of bitstreams: 1 othechar_pfs_me_prud.pdf: 662877 bytes, checksum: 8f3953cd38a014baaeb066abad521aa2 (MD5) / Neste trabalho, analisamos métodos de diferenças finitas para solução numérica da equação de Poisson em domínios irregulares com condições do tipo Dirichlet, fazendo um estudo detalhado de cada um desses métodos numéricos. Em particular, analisamos o Método das Interfaces Imersas (MII), Métodos Clássicos usando interpolações linear (MCL) e quadrática (MCQ) e um Método do tipo Fronteiras Imersas modificado (MFIM). Inicialmente, comparamos os resultados obtidos por esses métodos na solução numérica de uma equação elíptica unidimensional, envolvendo uma interface localizada em um ponto que não coincide com a malha. No caso unidimensional provamos que o MCL e o MFIM são equivalentes. Posteriormente, analisamos os resultados obtidos por esses métodos na solução numérica de problemas elípticos bidimensionais, com condições de contorno definida sobre geometrias irregulares. Em geral, os métodos foram consistentes com a solução exata. No caso unidimensional o MII e o MCQ apresentaram resultados semelhantes, com ordem de precisão quadrática, enquanto que o MCL e o MFIM são menos precisos para esses testes. Após isso, realizamos testes preliminares envolvendo geometrias bidimensionais irregulares. Os resultados apontam que o MFIM e o MII são mais acurados e possuem ordem de convergência quadrática / In this work, we study finite difference methods for the numerical solution of PoissonŠs equation on irregular domains with Dirichlet-type boundary conditions, performing a detailed study of these schemes. In particular, we analyze the Immersed Interfaces method (IIM), the classical method with linear (CML) and quadratic (CMQ) interpolation and the modified immersed boundary method (MIBM). Firstly, we compare the results obtained from these methods for solving a one-dimensional elliptic equation. In this equation, an interface is located at an irregular grid point. In general, all methods have been found consistent to the exact solution. In the one-dimensional case, IIM and CMQ have showed similar results, with second-order accuracy while MBIM and CML have presented less accurate results. Finally, we conduct preliminary results for two-dimensional irregular geometries. The results show that IIM and MIBM are more accurate than the classical method with linear interpolation

Made available in DSpace on 2014-06-11T19:27:09Z (GMT). No. of bitstreams: 0 Previous issue date: 2013-03-28Bitstream added on 2014-06-13T18:07:06Z : No. of bitstreams: 1 fermino_ms_me_prud.pdf: 1320105 bytes, checksum: 783a313a3f9ea07255cc0289181db2f8 (MD5) / No sensoriamento remoto, o desenvolvimento dos sistemas sensores e inerente ao fornecimento de dados com maior quantidade, qualidade e variabilidade, fazendo do processamento digital de imagens um meio para aplicação de m etodos matem aticos que aprimoram os resultados já obtidos. Uma característica dos sistemas sensores e a resolução espacial de imagens pancromáticas superior a resolucão espacial das imagens multiespectrais. Uma característica dos sistemas sensores e o fornecimento imagens pancromáticas com resolução espacial superior as imagens multiespectrais, cuja fusão busca melhor resolução espacial com menor perda do conteúdo multiespectral. Existem inúmeros métodos de fusão de imagens bem conhecidos, dentre os quais podemos elencar IHS, YUV e métodos baseados em transformadas multiescala. Os méetodos tipo IHS baseados na transformada wavelet têm gerado excelentes resultados na busca por minorar a distorção das cores no resultado do processo de fusão... / In remote sensing, the development of sensor systems is inherent in the provision of data with greater quantity, quality and variability, making the digital image processing a way for an application of mathematical methods to improve the results already achieved. A feature of the sensors systems is to provide panchromatic images with a better spatial resolution than its multispectral images, whose merger preserves spatial details without multispectral content loss. There are numerous widely known fusion methods, among which we can list IHS, YUV and mustiscale transform based methods. IHS type methods based on wavelet transform has generated excellent results in the search for minimizing color distortions in the merger... (Complete abstract click electronic access below)