Le flux sanguin cérébral (CBF) caractérise la micro-circulation et l'irrigation des tissus. Cette information de perfusion cérébrale est utilisé en clinique pour le diagnostic et le suivi thérapeutique de nombreuses maladies. La technique de mesure de CBF la moins invasive est celle par marquage de spins artériels (ASL) où l'eau du sang fait office de traceur. L'objectif de cette thèse, menée dans le cadre d'une convention CIFRE, consistait à faciliter l'utilisation de séquences ASL continues et pseudo-continues (CASL, pCASL) ainsi qu'à améliorer leur performance en pré-clinique. En effet, la mesure quantitative de CBF par ASL est un protocole complexe qui nécessite plusieurs étapes d'ajustements, d'acquisitions et de traitement de données. Dans le but d'alléger ce protocole, un package CASL a été développé en collaboration avec Bruker. Plusieurs étapes d'ajustements et de post-processing ont été automatisées, rendant la génération de cartes CBF relatives et absolues plus aisée. Le champ magnétique élevé des scanners IRM pré-cliniques présente de nombreux avantages mais est également une source de problèmes en ASL. Nous nous sommes intéressés plus particulièrement à deux d'entre eux : l'instabilité du marquage de spins et l'échauffement induit par les séquences ASL. Pour stabiliser le marquage ASL, une stratégie d'optimisation de la séquence pCASL a été développée et testée chez le rat à 9.4 T. Ceci a permis l'obtention d'un marquage robuste, même en situations de shim dégradé. Le package pCASL a été partagé avec dix autres instituts dans le monde. L'échauffement induit lors de séquences CASL et pCASL par le dépôt d'énergie radiofréquence a été caractérisé globalement et localement, dans le cerveau et au niveau des carotides, pour deux configurations d'antenne d'émission. Pour finir, une séquence pCASL encodée en temps a été développée et appliquée à la souris, dans le cadre d'une collaboration avec des équipes néerlandaises du Leiden University Medical Center. Cet outil permet la mesure simultanée de CBF et du temps de transit artériel, un paramètre pouvant refléter des pathologies vasculaires sous-jacentes. / Cerebral blood flow (CBF) characterizes the blood supply to brain tissue. This perfusion-related parameter contributes in diagnosis and therapeutic follow-up in many diseases. The least invasive technique to measure CBF is arterial spin labeling (ASL), where arterial water is used as tracer. The aim of this PhD project, conducted within a CIFRE agreement (Convention Industrielle de Formation par la REcherche), was to increase the performance and to facilitate the use of continuous and pseudo-continuous arterial spin labeling (CASL, pCASL) tools in preclinical studies. CBF quantification by means of ASL is one of the most challenging MRI modalities in terms of the workflow, since additional adjustments, acquisitions and post-processing steps are required. First, to render the workflow smoother for the user, a CASL package has been developed in collaboration with Bruker. This workflow allows easier relative and absolute CBF measurements, thanks to the integration of automated adjustments and reconstruction steps. In a second step, problems arising at high magnetic field were addressed. A strategy to optimize the pCASL labeling sequence in order to obtain robust results was developed and its robustness towards suboptimal shim conditions was demonstrated at 9.4 T in rats. The developed pCASL-package, consisting of three sequences, was shared with ten other institutes worldwide. Another issue encountered at high magnetic fields is heating due to RF power deposition, which was assessed locally in the brain and in the carotids, as well as globally, for the CASL and pCASL sequences and for two different transmit coil configurations. In a third step, time-encoded pCASL was developed in mice in collaboration with teams of the Leiden University Medical Center. This tool enables the simultaneous mapping of CBF and arterial transit time, a parameter that can reflect underlying pathologies such as increased vessel tortuosity or occlusion.

Made available in DSpace on 2014-12-17T15:48:02Z (GMT). No. of bitstreams: 1 SamaraPCM.pdf: 423447 bytes, checksum: 456d500c5d740d1624cc15f51c602aa1 (MD5) Previous issue date: 2006-05-19 / The interval datatype applications in several areas is important to construct a interval type reusable, i.e., a interval constructor can be applied to any datatype and get intervals this datatype. Since the interval is, of certain form, a set of elements limited for two bounds, left and right, with a order notions, then it s reasonable that interval constructor enclose datatypes with partial order. On the order hand, what we want is work with interval of any datatype like this we work with this datatype then. it s important to guarantee the properties of the datatype when maps to interval of this datatype. Thus, the interval constructor get a theory to parametrized interval type, i.e., a interval with generics parameters (for example rational, real, complex). Sometimes, the interval application in some algebras doesn t guarantee the mainutenance of their properties, for example, when we use interval of real, that satisfies the field properties, it doesn t guarantee the distributivity propertie. A form to surpass this problem Santiago introduced the local equality theory that weakened the notion of strong equality, and thus, allowing some properties are local keeped, what can be discard before. The interval arithmetic generalization aim to apply the interval constructor on ordered algebras weakened for local equality with the purpose of the keep their properties. How the intervals are important in applications with continuous data, it s interesting specify that theory using a specification language that supply a system development using intervals of form disciplined, trustworth and safe. Currently, the algebraic specification language, based in math models, have been use to that intention often. We choose CASL (Common Algebraic Specification Language) among others languages because CASL has several characteristics excellent to parametrized interval type, such as, provide parcialiy and parametrization / O uso do tipo intervalar em v?rias ?reas favorece a id?ia de se ter uma estrutura b?sica reutiliz?vel, ou seja, um construtor intervalar que seja aplicado a um tipo de dados para se obter os intervalos desse tipo. Como um intervalo, intuitivamente ? o conjunto de elementos que est?o entre dois extremos, sua constru??o presup?e a no??o de ordem, e portanto ? razo?vel que este construtor trabalhe sobre tipos munidos de uma ordem parcial. Por outro lado, como o que se quer ? operar com intervalos de objetos de um certo tipo como se opera com esses objetos, ent?o tamb?m ? razo?vel querer que as propriedades alg?bricas desses objetos sejam preservadas no seu tipo intervalar. Assim, o construtor intervalar fornece uma fundamenta??o te?rica para o tipo intervalo parametrizado, ou seja, intervalos cujo par?metro ? generalizado podendo ser, por exemplo, n?meros reais, complexos, etc. A aplica??o do intervalo em certas estruturas alg?bricas nem sempre garante a preserva??o de suas caracter?sticas, por exemplo, quando se trabalha com intervalos de n?meros reais, seria conveniente que estes pudessem se comportar como se fossem os reais. Isto n?o acontece pois os reais satisfazem as propriedades alg?bricas de corpo, j? os intervalos de reais n?o (por exemplo, n?o suporta a propriedade distributiva). Para superar esta dificuldade Santiago introduziu a teoria da igualdade local numa forma de enfraquecer a no??o de igualdade forte fazendo com que propriedades satisfeitas localmente sejam relevantes, propriedades estas que antes poderiam ser descartadas. A generaliza??o da aritm?tica intervalar prop?e a aplica??o do construtor intervalar em estruturas alg?bricas ordenadas e enfraquecidas pela igualdade local, objetivando a manuten??o de suas propriedades alg?bricas. Como os intervalos s?o importantes em aplica??es que trabalhem com dados cont?nuos, ? interessante descrever esta teoria usando uma linguagem de especifica??o que permita o desenvolvimento de sistemas computacionais que usem tipos intervalares de modo disciplinado, confi?vel e seguro. Atualmente, as linguagens de especifica??es alg?bricas, que se baseiam em modelos matem?ticos, t?m sido muito usadas para este proposito. Dentre as v?rias linguagens deste tipo existentes, foi escolhida CASL (Common Algebraic Specification Language) por conter diversas caracter?sticas relevantes para especifica??o do tipo intervalar parametrizado como, por exemplo, admitir parametriza??o e parcialidade

Presented in this study is a wide-ranging investigation into the use of properties of balance in an operational numerical weather prediction context. Initially, a joint numerical and observational study is undertaken. We used the Unified Model (UM), the suite of atmospheric and oceanic prediction software used at the UK Met Office (UKMO), to locate symmetric instabilities (SIs), an indicator of imbalanced motion. These are areas of negative Ertel potential vorticity (in the Northern hemisphere) calculated on surfaces of constant potential temperature. Once located, the SIs were compared with satellite and aircraft observational data. As a full three-dimensional calculation of Ertel PV proved outwith the scope of this study we calculated the two-dimensional, vertical component of the absolute vorticity, to assess the inertial stability criterion. We found that at the synoptic scale in the atmosphere, if there existed a symmetric instability, it was dominated by an inertial instability. With the appropriate observational data, evidence of inertial instability from the vertical component of the absolute vorticity, predicted by the UM was found at 12km horizontal grid resolution. Varying the horizontal grid resolution allowed the estimation of a grid length scale, above which, the inertial instability was not captured by the observational data, of approximately 20km. Independently, aircraft data was used to estimate that horizontal grid resolutions above 20-25km should not model any features of imbalance providing a real world estimate of the lower bound of the grid resolution that should be employed by a balanced atmospheric prediction model. A further investigation of the UM concluded that the data assimilation scheme and time of initialisation had no effect on the generation of SIs. An investigation was then made into the robustness of balanced models in the shallow water context, employing the contour-advective semi-Lagrangian (CASL) algorithm, Dritschel & Ambaum (1997), a novel numerical algorithm that exploits the underlying balance observed within a geophysical flow at leading order. Initially two algorithms were considered, which differed by the prognostic variables employed. Each algorithm had their three-time-level semi-implicit time integration scheme de-centred to mirror the time integration scheme of the UM. We found that the version with potential vorticity (PV), divergence and acceleration divergence, CA[subscript(δ,γ)], as prognostic variables preserved the Bolin-Charney balance to a much greater degree than the model with PV, divergence and depth anomaly CA[subscript(tilde{h},δ)], as prognostic variables. This demonstrated that CA[subscript(δ,γ)] was better equipped to benefit from de-centring, an essential property of any operational numerical weather prediction (NWP) model. We then investigate the robustness of CA[subscript(δ,γ)] by simulating flows with Rossby and Froude number O(1), to find the operational limits of the algorithm. We also investigated increasing the efficiency of CA[subscript(δ,γ)] by increasing the time-step Δt employed while decreasing specific convergence criteria of the algorithm while preserving accuracy. We find that significant efficiency gains are possible for predominantly mid-latitude flows, a necessary step for the use of CA[subscript(δ,γ)] in an operational NWP context. The study is concluded by employing CASL in the non-hydrostatic context under the Boussinesq approximation, which allows weak stratification to be considered, a step closer to physical reality than the shallow water case. CASL is compared to the primitive equation pseudospectral (PEPS) and vorticity-based pseudospectral (VPS) algorithms, both as the names suggest, spectral-based algorithms, which again differ by the prognostic variables employed. This comparison is drawn to highlight the computational advantages that CASL has over common numerical methods used in many operational forecast centres. We find that CASL requires significantly less artificial numerical diffusion than its pseudospectral counterparts in simulations of Rossby number ~O(1). Consequently, CASL obtains a much less diffuse, more accurate solution, at a lower resolution and therefore lower computational cost. At low Rossby number, where the flow is strongly influence by the Earth's rotation, it is found that CASL is the most cost-effective method. In addition, CASL also preserves a much greater proportion of balance, diagnosed with nonlinear quasigeostrophic balance (NQG), another significant advantage over its pseudospectral counterparts.

This thesis describes a theoretical study and an industrial application in the area of formal systems development, verification and formal testing using the specification language CSP-CASL. The latter is a comprehensive specification language which allows to describe systems in a combined algebraic / process algebraic notation. To this end it integrates the process algebra CSP and the algebraic specification language CASL. In this thesis we propose various formal development notions for CSP-CASL capable of capturing informal vertical and horizontal software development which we typically find in industrial applications. We provide proof techniques for such development notions and verification methodologies to prove interesting properties of reactive systems. We also propose a theoretical framework for formal testing from CSP-CASL specifications. Here, we present a conformance relation between a physical system and a CSP-C ASL specification. In particular we study the relationship between CSP-CASL development notions and the implemented system. The proposed theoretical notions of formal system development, property verification and formal testing for CSP-CASL, have been successfully applied to two industrial application: an electronic payment system called EP2 and the starting system of the BR725 Rolls- Royce jet engine control software.

Die erweiterte CSP-CASL Syntax wird dazu verwendet, sowohl positive als auch negative Testfälle zu generieren. Auf diese Weise wird sichergestellt, dass erwartetes und unerwünschtes Verhalten in den Testfäallen enthalten ist. Ferner werden Testterminologien für die CSP-CASL Spezifikation beschrieben, welche Softwareverfeinerungen und Erweiterungen untersuchen. Anschliessend wird die formale Definition von Softwareeigenschaften verwendet, um die Wiederverwendbarkeit von Testbestandteilen zu überprüfen. Diese Definitionen beschreiben die grundlegenden Eigenschaften im vorgeschlagenen Produkt und Prozessqualitäts- Framework. Ferner wird die Möglichkeit untersucht, die vorgeschlagenen Formalismus für die Entwicklung eines CMMI Prozesskonformen Frameworks zu verwenden. Dabei werden die Kernaspekte des CMMI Prozessmodells berücksichtigt. Das CMMI Compliance Bewertungssystem wurde entwickelt, um den Grad der Konformit ät der eingesetzten Softwareentwicklungsmethoden mit formalen Methoden zu bewerten. Ein generischer Algorithmus wird vorgeschlagen, um das Compliance Level der CMMI Prozessfelder und ihrer Komponenten zu ermitteln. Das Framework wird durch ein Tool unterstützt. Dieses Tool erlaubt es, die theoretischen Aspekte der vorgeschlagenen Theoreme praktisch zu unterstützen. Die Verwendbarkeit des vorgeschlagenen Frameworks wird an einem Anwendungsbeispiel aus der Medizintechnik gezeigt. Im Rahmen dieser Arbeit wird das Verständnis der Anwendung von formalen Methoden auf das Organisatorische Prozessmodell CMMI erweitert. Das komplette Framework wird repräsentiert durch die formale Spezifikationssprache CSP- CASL sowie der Prozessmodell CMMI. Ähnliche Ergebnisse können auch mit anderen formalen Methoden und Prozessverbesserungsmodellen erzielt werden. Diese Forschungsarbeit dagegen bildet einen Startpunkt für eine Prozessmodellkonformit ät mit einen auf formalen Methoden basierenden Softwaresystems sowie deren Entwicklung und Wartung. / The proposed formalisms and the other properties of formal methods are used to propose a framework of CMMI process model compliance. The core aspects of the CMMI process model are the process areas. A process area is a collection of best practices in a selected area. The CMMI compliance grading scheme is developed to evaluate the level of compliance with formal method based software development. A compliance algorithm is proposed to evaluate the process model through the evaluation of its components. The CMMI process areas are evaluated with a proposed algorithm. The compliance evaluation result is presented in the thesis. The complete framework is supported with a developed tool. This tool allows us to practically support our theoretical concepts. As a proof of concept, we explore our proposed framework for a medical instrument development and maintenance. In this thesis, the understanding of formal methods applicability is extended to the organizational process model, CMMI. The complete framework is presented for a formal specification language, CSP-CASL and process model, CMMI. However, similar result can be achieved with other formal methods for the compliance of other process models. This research is a starting point of process model compliance with formal methods. This has significant potential to automate the achievement of process and product quality goals of software systems.

Made available in DSpace on 2014-12-17T15:47:46Z (GMT). No. of bitstreams: 1 KatianeRL.pdf: 489064 bytes, checksum: 41384102e2da87fcb34b32c311dab535 (MD5) Previous issue date: 2004-04-16 / Na computa??o cient?fica ? necess?rio que os dados sejam o mais precisos e exatos poss?vel, por?m a imprecis?o dos dados de entrada desse tipo de computa??o pode estar associada ?s medidas obtidas por equipamentos que fornecem dados truncados ou arredondados, fazendo com que os c?lculos com esses dados produzam resultados imprecisos. Os erros mais comuns durante a computa??o cient?fica s?o: erros de truncamentos, que surgem em dados infinitos e que muitas vezes s?o truncados", ou interrompidos; erros de arredondamento que s?o respons?veis pela imprecis?o de c?lculos em seq??ncias finitas de opera??es aritm?ticas. Diante desse tipo de problema Moore, na d?cada de 60, introduziu a matem?tica intervalar, onde foi definido um tipo de dado que permitiu trabalhar dados cont?nuos,possibilitando, inclusive prever o tamanho m?ximo do erro. A matem?tica intervalar ? uma sa?da para essa quest?o, j? que permite um controle e an?lise de erros de maneira autom?tica. Por?m, as propriedades alg?bricas dos intervalos n?o s?o as mesmas dos n?meros reais, apesar dos n?meros reais serem vistos como intervalos degenerados, e as propriedades alg?bricas dos intervalos degenerados serem exatamente as dos n?meros reais. Partindo disso, e pensando nas t?cnicas de especifica??o alg?brica, precisa-se de uma linguagem capaz de implementar uma no??o auxiliar de equival?ncia introduzida por Santiago [6] que ``simule" as propriedades alg?bricas dos n?meros reais nos intervalos. A linguagem de especifica??o CASL, Common Algebraic Specification Language, [1] ? uma linguagem de especifica??o alg?brica para a descri??o de requisitos funcionais e projetos modulares de software, que vem sendo desenvolvida pelo CoFI, The Common Framework Initiative [2] a partir do ano de 1996. O desenvolvimento de CASL se encontra em andamento e representa um esfor?o conjunto de grandes expoentes da ?rea de especifica??es alg?bricas no sentido de criar um padr?o para a ?rea. A disserta??o proposta apresenta uma especifica??o em CASL do tipo intervalo, munido da aritm?tica de Moore, afim de que ele venha a estender os sistemas que manipulem dados cont?nuos, sendo poss?vel n?o s? o controle e a an?lise dos erros de aproxima??o, como tamb?m a verifica??o alg?brica de propriedades do tipo de sistema aqui mencionado. A especifica??o de intervalos apresentada aqui foi feita apartir das especifica??es dos n?meros racionais proposta por Mossakowaski em 2001 [3] e introduz a no??o de igualdade local proposta por Santiago [6, 5, 4]