La informació química sobre la composició d'una mostra pot ser molt diversa: des de saber de quins analits es composa un cert material a saber exactament en quina quantitat s'hi troben o de quina forma hi són presents, si estan relacionats estructuralment entre ells, etc. D'acord amb tota aquesta varietat, els mètodes analítics es classifiquen en dos grans grups: els mètodes d'anàlisi qualitativa i els mètodes d'anàlisi quantitativa. Segons les característiques del problema analític es triarà un o altre tipus de mètode d'anàlisi. Quan l'objectiu és saber què hi ha en una mostra desconeguda, un mètode qualitatiu serà el mes adequat. En els darrers temps, aquests mètodes han estat objecte d'estudi, i s'utilitzen avui dia, en molts camps d'aplicació. Per exemple, en l'anàlisi d'aliments és habitual l'ús d'un mètode qualitatiu per determinar si un o més analits es troben presents en la mostra per sobre o per sota d'una determinada concentració. Però si l'interès és saber la quantitat d'un determinat component en una mostra, l'opció d'un mètode quantitatiu serà la més adient. Aquesta tesi s'ha centrat en els mètodes d'anàlisi qualitativa pels nombrosos avantatges que presenten. Aquests mètodes poden ajudar a destriar mostres en funció de si aquestes presenten una quantitat d'un cert analit al voltant d'un valor de concentració prèviament establert, abans de ser quantificades. És a dir, s'utilitzen com a pas previ a l'aplicació del mètode quantitatiu, implicant un estalvi de feina, de temps i de diners important si es tracta de quantificar contaminants, detectar adulteracions o qualsevol altra situació en la que no es pugui sobrepassar una certa concentració. En aquests casos només s'ha de quantificar la mostra que en el mètode qualitatiu revela un resultat en el que es sobrepassa aquesta certa concentració. En d'altres àmbits d'aplicació, els mètodes qualitatius estan perfectament integrats en el procediment estàndard d'operacions, pel que, llevat en situacions molt específiques, un resultat positiu no necessita ser confirmat mitjançant una anàlisi posterior amb un mètode quantitatiu. A més de la importància de triar un mètode analític adequat a cada problemàtica, cal destacar que és igual d'important tenir fiabilitat sobre el resultat trobat i, per tant, sobre el mètode emprat. Això vol dir que qualsevol mètode analític ha de tenir definits els seus requeriments i qualitats analítiques i que s'ha de comprovar que aquests paràmetres prèviament definits, realment tenen el valor que se'ls ha assignat. D'aquesta confirmació se'n diu Validació, i és una condició indispensable per a poder emprar un mètode analític. D'aquesta manera es poden garantir els resultats demanats pels clients/usuaris. A més, des de l'aprovació de la norma ISO 17025 aquesta comprovació del mètode analític i dels seus resultats encara s'ha fet més recomanable. Fins fa poc temps, la validació de mètodes analítics s'ha centrat en els mètodes quantitatius. El resultat ha estat una sèrie de guies/pautes perfectament establertes d'ús molt comú. Però no hi ha cap protocol general per a validar un mètode qualitatiu. Amb aquesta tesi es vol contribuir a millorar aquesta situació. Es comença amb una revisió de les classificacions i de les definicions lligades a aquests mètodes, a més d'un repàs sobre quines institucions han fet esment d'aquest tema. Es segueix amb una proposta de classificació d'aquests mètodes i, finalment, es defineixen aquells paràmetres de qualitat que es consideren més importants en la validació. En les tres aplicacions pràctiques presentades es descriuen les característiques intrínseques del mètode d'anàlisi qualitativa. Després, es defineixen els paràmetres que s'adeqüen millor als requeriments del mètode i, finalment, es proposa un protocol de validació que permet el seu establiment. El cas de la revisió de les classificacions i definicions emprades en aquest àmbit, com en el cas de la presentació de les contribucions corresponents a diferents institucions, s'han traduït en dues publicacions que s'adjunten en la tesi. Pel que fa a les aplicacions pràctiques, una d'elles també s'inclou com a article publicat i les altres dues, s'inclouen com a articles acceptats. / The chemical information about the composition of a sample can be of different nature: which species are in the sample, their concentration or if they are structurally related, etc. In order to fit any of these requirements, either a qualitative or a quantitative analytical method may be used. If the aim is to identify species, a qualitative method will suit the problem at hand. These types of methods have been recently studied and nowadays are being increasingly used in several fields of analysis. For example, it is common to use qualitative methods as far as food analysis is concerned. On the contrary, if the aim is to quantify one or more analytes of a sample, a quantitative method will be very useful. This thesis has focused on qualitative analytical methods because they provide several advantages and they are being increasingly used. These types of methods can screen samples according to the presence or absence of certain analytes with regard to a pre-set level of concentration. That is to say, they are used as a step before the quantitative method and results in lower analysis time and costs because analyte quantification is not required in all situations. There are some particular analysis fields where qualitative methods are used as routine methods. Therefore, analyte quantification is not always necessary. Moreover, it is also important to provide reliable results, that is to say, to assure that the method performs with reliability. Any analytical method must have its requirements and its analytical properties previously defined, and their values must be proven. To confirm that the requirements and the analytical properties are the right ones and to confirm that they have the right values is to validate the analytical method. This is a necessary condition to use an analytical method. In this sense, the reliability of the results given to the clients or to the users is assured. Moreover, the ISO Standard 17025 strongly encourages method validation. Method validation has focused on quantitative methods. Therefore and as a result, there are more standards or guidelines addressed to quantitative methods validation. These guidelines are commonly used by several communities of practitioners. However, there is no generally accepted standard or validation procedure addressed to qualitative methods. In this sense, this thesis aims to contribute with the development of several validation procedures. The starting point is to provide an overview as a result of a bibliographic search concerning qualitative methods validation. This overview includes the criteria existing for qualitative methods classification as well as the institutions committed the validation of these methods. After that, a classification of these methods is suggested and the most relevant performance parameters in the validation process are defined. The subsequent practical applications describe the intrinsic characteristics of the corresponding qualitative analytical method. After that, the performance parameters that best fit the requirements and the characteristics of the method are defined and, finally, a validation strategy is proposed. Bear in mind, that the strategy considers the intrinsic characteristics of the analytical method. The overview including relevant aspects such as qualitative methods classification, performance parameters definitions and the institutions committed to qualitative method validation, among others, are presented as two publications included in the thesis. Regarding the three practical applications, they are presented as three accepted papers.

El EMBU (64 ítems) es un cuestionario de autoinforme que evalúa el recuerdo de las personas adultas sobre el estilo educativo con que fueron criadas. Consta de cuatro escalas: Rechazo, Calidez Emocional, Sobreprotección/Control y Favoritismo y ha sido adaptado en un amplio número de países e idiomas. Además, existe una forma corta, S-EMBU (22 ítems), que incluye las tres primeras escalas. Ambos han sido validados en España, donde se han desarrollado tres nuevos formatos, preguntando a niños (EMBU-C), adolescentes (EMBU-A) y progenitores (EMBU-P) sobre el estilo educativo percibido en la actualidad. Estas tres nuevas versiones únicamente han sido evaluadas en muestras comunitarias. El objetivo general de este trabajo es estudiar las propiedades psicométricas de las versiones en castellano del EMBU-C (41 ítems), EMBU-A (64 ítems) y el EMBU-P (52 ítems) en una muestra clínica.Se incluyeron en el estudio a 174 niños y 284 adolescentes procedentes de los servicios ambulatorios de salud mental de centros de asistencia primaria de la red pública de la provincia de Barcelona, así como a sus progenitores. Estos niños y adolescentes padecían algún trastorno según criterios DSM-IV valorados por la adaptación española de la Entrevista Diagnostica para Niños y Adolescentes (EDNA-IV). Los participantes contestaron individualmente la versión del EMBU correspondiente y también se les administró el Protocolo de Factores de Riesgo (PFR). La estructura interna y la invariancia factorial de las respuestas a los cuestionarios se evaluaron con análisis factorial confirmatorio. Para la versión de niños (EMBU-C) el modelo con un mejor ajuste fue el de 34 ítems y tres factores, excluyendo la escala de Favoritismo. Para la versión de adolescentes (EMBU-A) y de progenitores (EMBU-P) el ajuste del modelo de 22 ítems, comparable a la versión corta de adultos, fue satisfactorio. En cuanto a las respuestas relativas al estilo educativo paterno y materno, en los tres instrumentos se verificó la misma estructura interna y equivalencia de la mayoría de los parámetros entre ambos grupos de respuestas. Respecto a la consistencia interna de las tres versiones, las escalas de Rechazo y Calidez Emocional mostraron un comportamiento satisfactorio y la escala de Sobreprotección/Control obtuvo índices más discretos, resultados similares a los obtenidos en estudios previos. La influencia del sexo del hijo y del progenitor en las puntuaciones fue irrelevante, mientras que se halló una relación inversa entre la edad del hijo y la puntuación de Calidez Emocional por parte de los niños pequeños y de los progenitores. Las puntuaciones de Rechazo y Calidez Emocional de los tres cuestionarios se relacionaron de la forma prevista con las variables de ajuste familiar como la disciplina dura, la falta de supervisión adulta, de apoyo familiar y de afecto. Asimismo, las puntuaciones del EMBU-A discriminaron entre los adolescentes con una mala o buena relación con sus progenitores, mientras que las puntuaciones del EMBU-P diferenciaron entre los progenitores que manifestaron haber tenido problemas para educar a su hijo y los que no. El acuerdo entre las respuestas de los hijos y las de sus progenitores resultó bajo.Los resultados del EMBU-C, EMBU-A y EMBU-P en la muestra clínica estudiada, que podemos considerar representativa de la población infantojuvenil con psicopatología, indican unas propiedades psicométricas aceptables. El hecho de disponer de un mismo formato corto del EMBU-A y el EMBU-P, idéntico al de la versión de adultos, permite paliar los problemas de comparabilidad directa que existían hasta el momento. Sin embargo, el diferente formato del actual EMBU-C impide la comparabilidad directa entre las diversas versiones, por lo que se propone la revisión de algunos ítems de la versión de niños, para solventar este problema ante diseños con datos combinados. / The EMBU (64 items) is a self-report questionnaire that assesses adults' memories of their upbringing. It comprises four scales: Rejection, Emotional Warmth, Overprotection/Control Attempts and Favouring Subjects, and has been adapted in a large number of countries and languages. In addition, a short version, S-EMBU (22 items) is available, that includes the three first scales. Both have been validated in Spain, where three new formats were developed, asking to children (EMBU-C), adolescents (EMBU-A) and parents (EMBU-P) about their current perceptions of rearing style. These three new versions have only been evaluated in community samples.The general objective of this study is to examine the psychometric properties of the Spanish versions of the EMBU-C (41 items), EMBU-A (64 items) and EMBU-P (52 items) in a clinical sample.The sample comprised 174 children and 284 adolescents recruited from public primary mental health care centres in the Barcelona area, along with their parents. These children and adolescents suffered from a psychopathological disease diagnosed according to DSM-IV criteria evaluated in the Spanish adaptation of the DICA-IV (Structured Diagnostic Interview for Children and Adolescents). Participants answered the corresponding version of EMBU individually and the Schedule for Risk Factors (SRF) was also administered. Internal structure and factorial invariance of responses to the questionnaires were evaluated through confirmatory factor analysis.For the child version (EMBU-C) the model with a best goodness-of-fit was the 34-item and 3-factor model, when removing the Favouring Subjects scale. For the adolescent version (EMBU-A) and the parent version (EMBU-P) satisfactory fit to data of the 22-item model, comparable to the adult short version, was obtained. Regarding paternal and maternal ratings, the same internal structure was observed for all three questionnaires, and most of the parameters were equivalent across both groups of responses. In relation to the internal consistency reliability of the three versions, scales of Rejection and Emotional Warmth achieved satisfactory levels and the scale of Overprotection/Control Attempts showed lower values, as in previous studies. The influence of the gender of the children/adolescents and parents on scale scores was inappreciable, whereas an inverse relation was found between the age of the child and the score of Emotional Warmth for the younger children and parents. As predicted, the scores for Rejection and Emotional Warmth from the three questionnaires were related to variables of family adjustment, such as harsh discipline, lack of parental supervision, absence of family support or affection. Moreover, EMBU-A scores significantly differentiated between adolescents with good and bad relationships with their parents. EMBU-P scores also distinguished between those parents who expressed having problems with educating their children and those who did not. Agreement between children's and parents' responses was low.The results of the EMBU-C, EMBU-A and EMBU-P in the clinical sample studied, which we can consider as representative of a child-adolescent population with psychopathology, indicate acceptable psychometric properties. Having the same short format for EMBU-A and EMBU-P, as is the case for the adult version, helps to overcome the problems of direct comparability that have existed until now. However, the different format for current EMBU-C prevents direct comparability between the several versions. We propose the revision of some items of the child version so as to solve this problem in designs with combined data.

En el procés de convergència i construcció de l'Espai Europeu d'Educació Superior (EEES) les competències transversals es situen en el centre del disseny dels plans d'estudi. Al costat de l'adquisició de les competències específiques de cada àmbit professional s'han d'adquirir competències genèriques o transversals, comuns a moltes professions. En aquesta tesi ens centrem en la competència transversal de treball en equip, per la seva rellevància en qualsevol lloc de treball. Actualment hi ha molta investigació científica en quant a la comprensió i estructura dels equips, com també s’investiga en quina és la millor manera de fer l’aprenentatge per adquirir la competència. En definitiva, s'ha intensificat la investigació empírica i la necessitat de comprendre com funcionen els equips de treball per determinar les dimensions a ensenyar. Però ensenyar competències transversals no és una tasca fàcil. I encara més complex és avaluar la seva adquisició. Per això en aquesta tesi proposem determinar quina és l’estructura de la competència de treball en equip i es preten crear i validar una eina d'avaluació de la competència en els nivells de formació superior de grau i màster en els ensenyaments de ciències socials i en entorns laborals. L'eina d'avaluació dissenyada en aquesta tesi és una rúbrica o matriu de valoració. Les rúbriques són instruments de mesura en els quals s'estableixen critèris i estàndards per nivells, mitjançant la disposició d'escales, que permeten determinar la qualitat de l'execució dels estudiants en unes tasques específiques. Amb les rúbriques es facilita la qualificació de l'acompliment de l'estudiant en les competències que són complexes, imprecises i subjectives i a l’hora la comprensió del significat de la competència. El mètode seguit per a la creació i validació de l'eina ha estat el següent. Creació de la rúbrica. a) Revisió de la literatura sobre els equips de treball i treball en equip. Categorització i establiment dels critèris essencials de la competència: dimensions, components i elements. b) Construcció de la rúbrica de valoració especificant indicadors de la competència per als diferents elements. c) Creació de l'escala, descrivint els quatre nivells a observar i avaluar per a cada una dels indicadors. Validació de la rúbrica. S'han seguit dos processos paral·lels per assegurar la validesa tant interna com externa de l'eina, a través de: a) Grups de discussió per a la creació dels critèris, components, elements i indicadors, així com dels quatre nivells per a cada indicador (7 investigadors). I una prova de jutges de la rúbrica completa, mitjançant qüestionari, entrevista i posterior grup de discussió (7 experts). b) Anàlisi factorial exploratori per facilitar una reducció dels elements de l’eina i per analitzar la consistència de la mateixa, en definitiva per poder dur a terme la validació del constructe (277 qüestionaris). I l’avaluació 360º , per analitzar el potencial de l’eina en quant al sistema d’avaluació. Es conclou amb una eina, que en principi es va projectar amb un volum d’elements considerable 34, i s’ha reduït a 15, permetent de manera indirecta fer una reducció d’indicadors i per tant permetre amb aquesta eina definitiva una aplicació molt més còmoda i precisa. En relació als resultats, disposem d'una eina d'avaluació de la competència de Treball en Equip aplicable tant en entorns formatius com laborals, que permet avaluar i autoavaluar amb una elevada precisió la disposició personal de la competència. / En el proceso de convergencia y construcción del Espacio Europeo de Educación Superior (EEES) las competencias transversales se sitúan en el centro del diseño de los planes de estudio. Junto a la adquisición de las competencias específicas de cada ámbito profesional deben adquirirse competencias genéricas o transversales, comunes a muchas profesiones. En esta tesis nos centramos en la competencia transversal de Trabajo en Equipo, por su releváncia en cualquier lugar de trabajo. Actualmente existen muchas investigaciones científicas que hacen hincapié en la comprensión y estructura de los equipos, como también se investiga en el proceso de aprendizaje para adquirir la competencia. En definitiva, se ha intensificado la investigación empírica y la necesidad de comprender como funcionan los equipos de trabajo para determinar las dimensiones a enseñar. Pero enseñar competencias transversales no es tarea fácil. Y aún más complejo es evaluar su adquisición. Por ello en esta tesis proponemos determinar cual es la estructura de la competencia de trabajo en equipo y se pretende crear y validar una herramienta de evaluación de la competencia en los niveles de formación superior de grado y máster en las enseñanzas de ciencias sociales y en entornos laborales. La herramienta de evaluación diseñada en esta tesis es una rúbrica o matriz de valoración. Las rúbricas son instrumentos de medición en los cuales se establecen criterios y estándares por niveles, mediante la disposición de escalas, que permiten determinar la calidad de la ejecución de los estudiantes en unas tareas específicas. Con las rúbricas se facilita la calificación del desempeño del estudiante en las competencias que son complejas, imprecisas y subjetivas y a la vez la comprensión del significado de la competencia. El método seguido para la creación y validación de la herramienta ha sido el siguiente. Creación de la rúbrica. a) Revisión de la literatura sobre los equipos de trabajo y trabajo en equipo. Categorización y establecimiento de los criterios esenciales de la competencia: dimensiones, componentes y elementos. b) Construcción de la matriz de valoración especificando indicadores de la competencia para los distintos elementos. c) Creación de la escala, describiendo los cuatro niveles a observar y evaluar para cada una de los indicadores. Validación de la rúbrica. Se han seguido dos procesos paralelos para asegurar la validez interna y externa de la herramienta, a través de: a) Grupos de discusión para la creación de los criterios, componentes, elementos e indicadores, así como de los cuatro niveles para cada indicador (7 investigadores). Y una prueba de jueces de la rúbrica completa, mediante cuestionario, entrevista y posterior grupo de discusión (7 expertos). b) Análisis factorial exploratorio para facilitar una reducción de los elementos de la herramienta y para analizar la consisténcia de la misma, en definitiva para poder llevar a cabo la validación del “constructe” (277 cuestionarios). Y la evaluación 360º, para analizar el potencial de la herramienta en cuanto al sistema de evaluación. Se concluye con una herramienta, que en principio se proyecto con un volúmen de elementos considerable, 34, y se ha reducido a 15, permitiendo de manera indirecta hacer una reducción de indicadores, obteniendo como resultado una herramienta con una aplicación más comoda y precisa. En relación con los resultados, disponemos de una herramienta de evaluación de la competencia de Trabajo en equipo aplicable tanto en entornos formativos como laborales, que permite evaluar y autoevaluar con una elevada precisión la disposicón personal de la competencia. / L'Enseignement Supérieur (EEES) les compétences transversales se situent au centre des plans d’études. Parallèlement à l'acquisition de compétences spécifiques des milieux professionnels on doit acquérir des compétences génériques communes à de nombreuses professions. Dans cette thèse nous nous concentrons sur les compétences transversales du travail d'équipe, pour leurs pertinences dans un lieu de travail. Actuellement il y a beaucoup de recherches scientifiques sur la compréhension et la structure des équipes, on enquête aussi sur le meilleur moyen d'apprendre à acquérir des compétences. En définitive, on a intensifiée la recherche empirique et la nécessité de comprendre comment les équipes de travail pour déterminer les dimensions à enseigner. Mais l'enseignement de compétences transversales n'est pas une tâche facile et c’est encore plus complexe évaluer son acquisition. Voilà pourquoi nous proposons dans cette thèse de déterminer la structure de la compétence du travail d'équipe, et on cherche à créer et valider un outil pour évaluer la compétence qui englobe l'enseignement supérieur de premier cycle et la maîtrise en sciences sociales et les environnements de travail. L'outil d'évaluation conçu dans cette thèse est une rubrique ou une matrice d’évaluation. Les rubriques sont des instruments de mesure qui fixent des critères et des normes par niveaux, en fournissant des échelles pour déterminer la qualité de la performance des élèves dans des tâches spécifiques. Avec les rubriques on facilite la qualification de l’accomplissement de l’élève dans les compétences qui sont complexes, imprécises et subjectives, tout en comprenant le sens de la compétence. La méthode suivie pour la création et la validation de l'outil se présente comme suit. Création de la rubrique. a) Révision de la littérature sur les équipes de travail et le travail d'équipe. Catégorisation et établissement des critères essentiels de la compétence: la dimension, des composants et des éléments. b) Construction de la rubrique d’évaluation en spécifiant les indicateurs de la compétence pour les différents éléments. c) Création de l'échelle, en décrivant les quatre niveaux à observer et à évaluer pour chacun des indicateurs. Validation de la rubrique. On a suivi deux procédés parallèles pour assurer la validité interne et externe de l'outil, à travers: a) Un Groupe d’entente pour la création des critères, des composants, des sous-composant, des indicateurs et des 4 niveaux des indicateurs (7 chercheurs). Et une preuve de juge de la rubrique complète, au moyen d'un questionnaire, d’une entrevue et d’un groupe de discussion (7 experts). b) une analyse factorielle exploratoire afin de faciliter une réduction des éléments de l’outil et pour analyser la cohérence de celui-ci, en fin de compte de procédes à la validation de la “constructe” (277 questionnaires). Et l’évaluation à 360º, l’analyse du potentiel de l’outil en termes de systèmes d’évaluation. On conclut avec un outil, qui a initialement été conçu avec un volume considérable d'éléments, 34, et on a été réduit à 15, pour permettre indirectement une réductiondes indicateurs et donc facilite une application finale avec cet util plus confortable et précis. Par rapport aux résultats nous pouvons disposer d'un outil d'évaluation applicable dans des environnements formatifs et aussi dans des environnements de travail, et ainsi permettre évaluer et d’auto-évaluer avec une précision élevée la disposition personnelle de la compétence.

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.

The numerical simulation model presented is based on the integration of the fluid conservation equations (continuity, momentum and energy) in the whole compressor domain (compression chamber, valves, manifolds, mufflers, connecting tubes, parallel paths, etc.) using instantaneous local mean values for the different variables. It is interesting to remark how momentum equation has been taken into account in all compressor parts and the possibility to solve parallel paths, resonators, etc. Effective flow areas are evaluated considering multidimensional models based on modal analysis of fluid interaction in the valve. Then, second and third order vibration models of valve are also considered. The possibility to use compound bound has been also implemented.The force balances in the crankshaft connecting rod mechanical system are simultaneously solved at each time-step considered in the thermal and fluid dynamic compressor model. It allows to evaluate the instantaneous compression chamber volume and the different forces in the crankshaft connecting rod mechanical system. Mechanical system forces allows to know important information to predict possibleover-stresses in piston, piston pin, crankshaft, connecting rod, etc.The thermal analysis of the solid elements is based on global energy balances at each macro volume considered (shell, muffler, tubes, cylinder head, crankcase, motor, etc.). Some improvements can be implemented (shell conduction, heat transfer coefficient evaluation, etc.).The resulting governing equations (fluid flow, valve dynamics, conduction heat transfer in solids, etc.) are discretized by means of a fully implicit control volume formulation. The complete set of algebraic equations are coupled using the segregated he complete set of algebraic equations are coupled using the segregated pressure based algorithm Semi-Implicit Method for Pressure-Linked Equations(SIMPLEC) extended to compressible flow. Second and third time order schemes have been implemented for the transient terms.An extensive hermetic reciprocating compressor experimental validation has been presented and the experimental know-how acquired has been highlighted. Furthermore, two commercial hermetic reciprocating compressor have been instrumented in detail to obtain the thermal temperatures map and the pressure fluid evolutions along compressor for different working conditions. It is interesting to remark as a novelty, the use of very small absolute pressure transducers, instead of the standard relative transducers. They allow to know instantaneous absolute pressure inside compressor chamber, without the necessity of measurement an absolute pressure outside the compression chamber (as is usual in this kind of experimental works). The global comparative results have allowed to check the possibilities of the numerical simulation presented above and its accuracy compared with experimental data. After that, this work show the capabilities offered by the simulation presented and its final objective, a better understanding of the thermal and fluid dynamic compressor behaviour to improve the design of these equipments.Then, the objective has been to review and present different physically meaningful parameters that characterize the reciprocating compressor behaviour (volumetric efficiency, isentropic efficiency, heat transfer efficiency, mechanical, electrical and heat losses, Coefficient of Performance, etc.), their influence detachment and evolution under different working conditions, with the idea to predict the performance of hermetic reciprocating compressors under different working conditions using the above mentioned non-dimensional parameters.Finally, a parametric study of hermetic reciprocating compressors behaviour has been carried out. Results presented show the influence of different aspects (geometry, valves, motor, working conditions, etc.) in the compressor behaviour. The parametric studies and compressor characterization detachment allows also a better implementation of simplest models of the compressors in the thermal and fluid dynamic numerical simulation of vapour compressor cycles together with the rest of elements.

Objetivo: Analizar propiedades psicométricas de la versión española del Screening for Somatoform Symptoms (SOMS-2) en muestra de pacientes de Atención Primaria de España. Método: Se administró la traducción Española de la versión original de la SOMS-2 junto con la Entrevista Psiquiátrica Estructurada Polivalente (EPEP) a una muestra 165 pacientes de Atención Primaria. 74 pacientes realizaron un tratamiento cognitivo-conductual de 10 sesiones semanales de hora y media de duración. Se evaluó la fiabilidad test-retest a 6 y 12 meses de finalizar el tratamiento. Resultados: La SOMS-2 de 53 ítems y con punto de corte de 4 presenta sensibilidad del 97%, especificidad de 68%, Valor Predictivo Positivo (VPP) de 85% y Valor Predictivo Negativo (VPN) de 92% y α de Cronbach de 0,82. Conclusiones: La versión española de la SOMS-2 muestra buena consistencia interna, sensibilidad y especificidad. Resulta un instrumento de cribaje útil para evaluar el trastorno de somatización en Atención Primaria.

L'anàlisi qualitatiu ha estat sempre molt important en el control antidopatge i constitueix cada cop més una part molt significativa de l'activitat diària d'altres tipus de laboratoris. Tanmateix, no existeixen guies o documents específics per ajudar els laboratoris a implantar sistemes de qualitat quan es disposa d'aquest tipus de mètodes. L'objectiu general d'aquesta tesi ha estat el desenvolupament de les eines necessàries per assegurar la qualitat i fiabilitat dels resultats produïts per mètodes d'anàlisi qualitatius, treballant en tres aspectes fonamentals per a l'assegurament de la qualitat dels resultats als laboratoris d'anàlisi: la validació de mètodes, el control intern de la qualitat, i els exercicis d'intercomparació.S'ha elaborat un protocol de validació, s'ha implantat un sistema de control intern de la qualitat per a mètodes d'anàlisi qualitatius i, finalment, s'han elaborat protocols per a la preparació de mostres que seran utilitzades com a materials d'assaig en exercicis d'intercomparació o com a materials de referència, i per realitzar estudis d'homogeneïtat i d'estabilitat, que han estat aplicats a l'estudi de l'estabilitat de substàncies d'interès en control antidopatge. / Qualitative analysis has been very important in antidoping control and its becoming a significant part of the daily activity of other type of laboratories. However, there is a lack of guidance or specific documents to help laboratories to implement quality assurance systems when using these type of methods. The aim of this thesis has been the development of the necessary tools to ensure the quality and reliability of results released by qualitative analytical methods, working in the three main aspects of quality assurance in the analytical laboratory: method validation, internal quality control and intercomparison exercises.A protocol for method validation has been proposed and an internal quality control system for qualitative methodologies has been established. Finally, protocols for the preparation of samples to be used in intercomparison exercises or as reference materials, including homogeneity and stability studies, have been prepared. These protocols have been applied to study the stability of substances with especial interest in antiodoping control.

Es va determinar el risc d'asma i la seva associació amb les exposicions laborals, així com la càrrega d'asma relacionat amb el treball, entre professionals sanitaris. Després de validar un qüestionari nou, es va administrar una enquesta a 5600 metges, infermers, i tècnics en teràpia respiratòria i ocupacional a Texas (tasa de resposta-66%). S'evidencia un risc elevat d'asma desprès d'haver començat a treballar per tasques de neteja general, desinfecció d'instruments mèdics, l'ús de guants de làtex i l'administració de medicaments en aerosol. També s'evidencien associacions significatives entre símptomes de hiperreactivitat bronquial i l'ús de productes generals de neteja, l'administració de medicaments en aerosol, l'aplicació de productes adhesius/dissolvents, i en persones amb antecedents d'exposició a un vessament químic. El risc per làtex desaparegué desprès de l'any 2000. Les exposicions laborals contribueixen de manera important a l'asma en el personal sanitari, justificant tant la implementació de controls adequats com la recerca addicional. / The magnitude of asthma risk, its associations with occupational exposures, and the burden of work-related asthma was estimated in healthcare professionals. After validating a new asthma questionnaire, a cross-sectional survey was conducted among 5600 Texas physicians, nurses, respiratory therapists and occupational therapists (response rate, 66%). Elevated risks of asthma after entry into the profession were found for general cleaning tasks, medical instrument cleaning, use of powdered latex gloves, and administration of aerosolized medications. Significant associations were also found between bronchial hyperresponsiveness-related symptoms and use of general cleaning products, administration of aerosolized medications, use of adhesives or solvents as products in patient care, and with a history of acute exposure to a chemical spill. The risk associated with latex disappeared after the year 2000. Occupational exposures contribute importantly to asthma among healthcare professionals and are not trivial, meriting both further study and implementation of appropriate controls.

Analytical chemistry can be split into two main types, qualitative and quantitative. Most modern analytical chemistry is quantitative. Popular sensitivity to health issues is aroused by the mountains of government regulations that use science to, for instance, provide public health information to prevent disease caused by harmful exposure to toxic substances. The concept of the minimum amount of an analyte or compound that can be detected or analysed appears in many of these regulations (for example, to discard the presence of traces of toxic substances in foodstuffs) generally as a part of method validation aimed at reliably evaluating the validity of the measurements.The lowest quantity of a substance that can be distinguished from the absence of that substance (a blank value) is called the detection limit or limit of detection (LOD). Traditionally, in the context of simple measurements where the instrumental signal only depends on the amount of analyte, a multiple of the blank value is taken to calculate the LOD (traditionally, the blank value plus three times the standard deviation of the measurement). However, the increasing complexity of the data that analytical instruments can provide for incoming samples leads to situations in which the LOD cannot be calculated as reliably as before.Measurements, instruments and mathematical models can be classified according to the type of data they use. Tensorial theory provides a unified language that is useful for describing the chemical measurements, analytical instruments and calibration methods. Instruments that generate two-dimensional arrays of data are second-order instruments. A typical example is a spectrofluorometer, which provides a set of emission spectra obtained at different excitation wavelengths.The calibration methods used with each type of data have different features and complexity. In this thesis, the most commonly used calibration methods are reviewed, from zero-order (or univariate) to second-order (or multi-linears) calibration models. Second-order calibration models are treated in details since they have been applied in the thesis.Concretely, the following methods are described:- PARAFAC (Parallel Factor Analysis)- ITTFA (Iterative Target Transformation Analysis)- MCR-ALS (Multivariate Curve Resolution-Alternating Least Squares)- N-PLS (Multi-linear Partial Least Squares)Analytical methods should be validated. The validation process typically starts by defining the scope of the analytical procedure, which includes the matrix, target analyte(s), analytical technique and intended purpose. The next step is to identify the performance characteristics that must be validated, which may depend on the purpose of the procedure, and the experiments for determining them. Finally, validation results should be documented, reviewed and maintained (if not, the procedure should be revalidated) as long as the procedure is applied in routine work.The figures of merit of a chemical analytical process are 'those quantifiable terms which may indicate the extent of quality of the process. They include those terms that are closely related to the method and to the analyte (sensitivity, selectivity, limit of detection, limit of quantification, ...) and those which are concerned with the final results (traceability, uncertainty and representativity) (Inczédy et al., 1998). The aim of this thesis is to develop theoretical and practical strategies for calculating the limit of detection for complex analytical situations. Specifically, I focus on second-order calibration methods, i.e. when a matrix of data is available for each sample.The methods most often used for making detection decisions are based on statistical hypothesis testing and involve a choice between two hypotheses about the sample. The first hypothesis is the "null hypothesis": the sample is analyte-free. The second hypothesis is the "alternative hypothesis": the sample is not analyte-free. In the hypothesis test there are two possible types of decision errors. An error of the first type occurs when the signal for an analyte-free sample exceeds the critical value, leading one to conclude incorrectly that the sample contains a positive amount of the analyte. This type of error is sometimes called a "false positive". An error of the second type occurs if one concludes that a sample does not contain the analyte when it actually does and it is known as a "false negative". In zero-order calibration, this hypothesis test is applied to the confidence intervals of the calibration model to estimate the LOD as proposed by Hubaux and Vos (A. Hubaux, G. Vos, Anal. Chem. 42: 849-855, 1970).One strategy for estimating multivariate limits of detection is to transform the multivariate model into a univariate one. This strategy has been applied in this thesis in three practical applications:1. LOD for PARAFAC (Parallel Factor Analysis).2. LOD for ITTFA (Iterative Target Transformation Factor Analysis).3. LOD for MCR-ALS (Multivariate Curve Resolution - Alternating Least Squares)In addition, the thesis includes a theoretical contribution with the proposal of a sample-dependent LOD in the context of multivariate (PLS) and multi-linear (N-PLS) Partial Least Squares. / La Química Analítica es pot dividir en dos tipus d'anàlisis, l'anàlisi quantitativa i l'anàlisi qualitativa. La gran part de la química analítica moderna és quantitativa i fins i tot els govern fan ús d'aquesta ciència per establir regulacions que controlen, per exemple, nivells d'exposició a substàncies tòxiques que poden afectar la salut pública. El concepte de mínima quantitat d'un analit o component que es pot detectar apareix en moltes d'aquestes regulacions, en general com una part de la validació dels mètodes per tal de garantir la qualitat i la validesa dels resultats.La mínima quantitat d'una substància que pot ser diferenciada de l'absència d'aquesta substància (el que es coneix com un blanc) s'anomena límit de detecció (limit of detection, LOD). En procediments on es treballa amb mesures analítiques que són degudes només a la quantitat d'analit present a la mostra (situació d'ordre zero) el LOD es pot calcular com un múltiple de la mesura del blanc (tradicionalment, 3 vegades la desviació d'aquesta mesura). Tanmateix, l'evolució dels instruments analítics i la complexitat creixent de les dades que generen, porta a situacions en les que el LOD no es pot calcular fiablement d'una forma tan senzilla. Les mesures, els instruments i els models de calibratge es poden classificar en funció del tipus de dades que utilitzen. La Teoria Tensorial s'ha utilitzat en aquesta tesi per fer aquesta classificació amb un llenguatge útil i unificat. Els instruments que generen dades en dues dimensions s'anomenen instruments de segon ordre i un exemple típic és l'espectrofluorímetre d'excitació-emissió, que proporciona un conjunt d'espectres d'emissió obtinguts a diferents longituds d'ona d'excitació.Els mètodes de calibratge emprats amb cada tipus de dades tenen diferents característiques i complexitat. En aquesta tesi, es fa una revisió dels models de calibratge més habituals d'ordre zero (univariants), de primer ordre (multivariants) i de segon ordre (multilinears). Els mètodes de segon ordre estan tractats amb més detall donat que són els que s'han emprat en les aplicacions pràctiques portades a terme. Concretament es descriuen:- PARAFAC (Parallel Factor Analysis)- ITTFA (Iterative Target Transformation Analysis)- MCR-ALS (Multivariate Curve Resolution-Alternating Least Squares)- N-PLS (Multi-linear Partial Least Squares)Com s'ha avançat al principi, els mètodes analítics s'han de validar. El procés de validació inclou la definició dels límits d'aplicació del procediment analític (des del tipus de mostres o matrius fins l'analit o components d'interès, la tècnica analítica i l'objectiu del procediment). La següent etapa consisteix en identificar i estimar els paràmetres de qualitat (figures of merit, FOM) que s'han de validar per, finalment, documentar els resultats de la validació i mantenir-los mentre sigui aplicable el procediment descrit.Algunes FOM dels processos químics de mesura són: sensibilitat, selectivitat, límit de detecció, exactitud, precisió, etc. L'objectiu principal d'aquesta tesi és desenvolupar estratègies teòriques i pràctiques per calcular el límit de detecció per problemes analítics complexos. Concretament, està centrat en els mètodes de calibratge que treballen amb dades de segon ordre.Els mètodes més emprats per definir criteris de detecció estan basats en proves d'hipòtesis i impliquen una elecció entre dues hipòtesis sobre la mostra. La primera hipòtesi és la hipòtesi nul·la: a la mostra no hi ha analit. La segona hipòtesis és la hipòtesis alternativa: a la mostra hi ha analit. En aquest context, hi ha dos tipus d'errors en la decisió. L'error de primer tipus té lloc quan es determina que la mostra conté analit quan no en té i la probabilitat de cometre l'error de primer tipus s'anomena fals positiu. L'error de segon tipus té lloc quan es determina que la mostra no conté analit quan en realitat si en conté i la probabilitat d'aquest error s'anomena fals negatiu. En calibratges d'ordre zero, aquesta prova d'hipòtesi s'aplica als intervals de confiança de la recta de calibratge per calcular el LOD mitjançant les fórmules d'Hubaux i Vos (A. Hubaux, G. Vos, Anal. Chem. 42: 849-855, 1970)Una estratègia per a calcular límits de detecció quan es treballa amb dades de segon ordre es transformar el model multivariant en un model univariant. Aquesta estratègia s'ha fet servir en la tesi en tres aplicacions diferents::1. LOD per PARAFAC (Parallel Factor Analysis).2. LOD per ITTFA (Iterative Target Transformation Factor Analysis).3. LOD per MCR-ALS (Multivariate Curve Resolution - Alternating Least Squares)A més, la tesi inclou una contribució teòrica amb la proposta d'un LOD que és específic per cada mostra, en el context del mètode multivariant PLS i del multilinear N-PLS.

El objetivo principal de esta tesis es evaluar la efectividad de un programa de gestión de casos frente a un programa de atención estándar en personas con esquizofrenia. El objetivo principal se operacionalizó en tres objetivos consecutivos. Del objetivo preliminar surge el Estudio 1 que revisa la literatura sobre la gestión de casos. La gestión de casos ha experimentado importantes cambios y los modelos tradicionales están en desuso. Los resultados de las revisiones metanalíticas sobre la eficacia de la gestión de casos son heterogéneos. Las características de los pacientes y la fidelidad al programa podrían estar asociadas a los efectos de la gestión de casos. Se sugiere el desarrollo de estrategias de gestión de casos que ofrezcan diferentes grados de intensidad según las necesidades del paciente. Del objetivo intermedio surgen los estudios 2, 3 y 4. Estos estudios se han centrado en la validación, en población con esquizofrenia, de la World Health Organization Quality of Life Brief Version, la Disability Assessment Schedule Short Form y la DUKE-UNC Functional Social Support Questionnaire. Las tres escalas muestran puntuaciones fiables y válidas, y son instrumentos útiles para la valoración psicosocial de esta población. Del objetivo específico se derivan los estudios 5 y 6. El estudio 5 incide en el conocimiento de las necesidades de los pacientes con esquizofrenia asignados a un programa de gestión de casos. Se hace una propuesta de criterios y de variables a considerar cuando se incluya a un paciente en dicho programa así como de reconfiguración del mismo. El estudio 6 analiza la efectividad de un programa de gestión de casos frente a un programa de atención estándar. El grupo de pacientes en gestión de casos muestra peor funcionamiento y mayor uso de servicios que el grupo en programa estándar en la evaluación inicial. Al seguimiento, ambos grupos mejoran y el grupo en gestión de casos alcanza niveles similares a los del grupo en atención estándar en la mayoría de variables. Esta tesis profundiza en el conocimiento de dos modalidades de tratamiento comunitario del Servicio Catalán de Salud. Ambas son efectivas y podrían ofrecerse consecutivamente según necesidades del paciente. / The psychiatric deinstitutionalization leaded to an increase of community resources for persons with Severe Mental Illness (SMI). These resources include the so-called case management programs that aim to organize, coordinate and integrate the resources available for patient care through continuous contact with one or more key workers. The Mental Health Strategy of the Spanish National Health System (2007) recommends case management programs for the coordination, access and use of mental health resources. However, these programs are not implemented throughout and there are differences between Autonomous Communities. In Catalonia, these programs are available at Adult Mental Health Mental Health Care Centres of the State Mental Health Network of the Catalan Health Service. Specifically, the Severe Mental Illness Specific Care Program, known as PAE-TMS, covers the health care for most patients with SMI so it is particularly important to assess its effectiveness. This PhD thesis addresses this issue and its main objective is to assess the effectiveness of the PAE-TMS versus a standard treatment program (STP) in persons with schizophrenia. This objective was operationalized in three consecutive objectives: 1) preliminary objective: literature review of case management; 2) intermediate objective: validation of assessment instruments in persons with schizophrenia, and 3) specific objective: to improve knowledge of the needs of patients with schizophrenia included in the PAE-TMS and analyze its effectiveness. Each goal is associated with one or more studies. The preliminary objective leads to study 1. It reviews the literature regarding the origins, principles, tasks, models and effects of case management programs. This study shows that case management has undergone major changes over time and that the traditional models seem not to be in use, as evidenced by the most recent models. The results of meta-analytic reviews of the effectiveness of case management programs are diverse. Recent studies suggest that some variables, such as patient characteristics and fidelity to the program, may be associated with the effectiveness of case management. It is suggested, therefore, the development of case management strategies that may offer different degrees of intensity depending on patients’ needs. The intermediate goal leads to studies 2, 3 and 4. These studies are psychometric and have focused on the validation in persons with schizophrenia of the following instruments: the World Health Organization Quality of Life Brief Version, the Disability Assessment Schedule Short Form and the DUKE-UNC Functional Social Support Questionnaire. The three instruments showed good psychometric properties. Their scores are reliable and valid and, therefore, are useful and appropriate for the assessment of quality of life, disability and social support in persons with schizophrenia. The specific goal leads to studies 5 and 6. The study 5 provides a better understanding of the needs of patients with schizophrenia assigned to the PAE-TMS or the STP. We suggest criteria and variables that may be considered when assigning a patient to the PAE-TMS. Considering these variables, we suggest a reconfiguration of the program by means of the addition of evidence-based elements. The study 6 assesses the effectiveness of the PAE-TMS versus the STP. At baseline, the group of patients in the PAE-TMS showed a profile characterized by worse clinical and psychosocial functioning and greater use of services than patients in the STP. At one year follow-up, both groups improved and the group in the PAE-TMS achieved a similar level to that in the STP group in most outcomes. This PhD thesis provides a deeper insight into two modalities of care that target the care of most of persons with SMI in the Catalan Health Service. The PAE-TMS and the STP are effective and could be offered consecutively according to patients’ needs.