Control and Localisation for the ISePorto Robotic Soccer Team

International Conference on Advanced Robotics, Coimbra, Portugal, Julho 2003

Decision Support for Energy Contracts Negotiation with Game Theory and Adaptive Learning

This paper presents a decision support methodology for electricity market players’ bilateral contract negotiations. The proposed model is based on the application of game theory, using artificial intelligence to enhance decision support method’s adaptive features. This model is integrated in AiD-EM (Adaptive Decision Support for Electricity Markets Negotiations), a multi-agent system that provides electricity market players with strategic behavior capabilities to improve their outcomes from energy contracts’ negotiations. Although a diversity of tools that enable the study and simulation of electricity markets has emerged during the past few years, these are mostly directed to the analysis of market models and power systems’ technical constraints, making them suitable tools to support decisions of market operators and regulators. However, the equally important support of market negotiating players’ decisions is being highly neglected. The proposed model contributes to overcome the existing gap concerning effective and realistic decision support for electricity market negotiating entities. The proposed method is validated by realistic electricity market simulations using real data from the Iberian market operator—MIBEL. Results show that the proposed adaptive decision support features enable electricity market players to improve their outcomes from bilateral contracts’ negotiations.

Matrix fractional systems

This paper addresses the matrix representation of dynamical systems in the perspective of fractional calculus. Fractional elements and fractional systems are interpreted under the light of the classical Cole–Cole, Davidson–Cole, and Havriliak–Negami heuristic models. Numerical simulations for an electrical circuit enlighten the results for matrix based models and high fractional orders. The conclusions clarify the distinction between fractional elements and fractional systems.

Initial dilemmas in IST research: design science and design research, a clarification of concepts

The inter-disciplinarity of information systems, applied discipline and activity of design, and the study from different paradigms perspectives explains the diversity of problems addressed. The context is broad and includes important issues beyond technology, as the application, use, effectiveness, efficiency and their organizational and social impacts. In design science, the research interest is in contributing to the improvement of the processes of the design activity itself. The relevance of research in design science is associated with the result obtained for the improvement of living conditions in organizational, inter-organizational and Society contexts. In the research whose results are artifacts, the adoption of design research as a process of research is crucial to ensure discipline, rigor and transparency. Based on a literature review, this paper clarifies the terms of design science and design research. This is the main motivation for presenting this paper, determinant for the phase in research in technologies and information systems which are the three research projects presented. As a result the three projects are discussed in relation to the concepts of design science and design research.

Interpretative research in information systems: two qualitative research design projects

In a scientific research project is important to define the underlying philosophical orientation of the project, because this will influence the choices made in respect of scientific methods used, as well as the way they will be applied. It is crucial, therefore, that the philosophy and research design strategy are consistent with each other. These questions become even more relevant in qualitative research. Historically, the interpretive research philosophy is more associated to the scientific areas of social sciences and humanities where the subjectivity inherent to human intervention is more explicitly defined. Information systems field are, primarily, trapped in computer science field, though it also integrates issues related with management and organizations field. This shift from a purely technological guidance for the consideration of the problems of management and organizations has fostered the rise of research projects according to the interpretive philosophy and using qualitative methods. This paper explores the importance of alignment between the epistemological orientation and research design strategy, in qualitative research projects. As a result, it is presented two PhD projects, with different research design strategies, that are being developed in the technology and information systems field, in the light of the interpretive paradigm.

Middleware for Large-scale Distributed Systems

Nos últimos anos o aumento exponencial da utilização de dispositivos móveis e serviços disponibilizados na “Cloud” levou a que a forma como os sistemas são desenhados e implementados mudasse, numa perspectiva de tentar alcançar requisitos que até então não eram essenciais. Analisando esta evolução, com o enorme aumento dos dispositivos móveis, como os “smartphones” e “tablets” fez com que o desenho e implementação de sistemas distribuidos fossem ainda mais importantes nesta área, na tentativa de promover sistemas e aplicações que fossem mais flexíveis, robutos, escaláveis e acima de tudo interoperáveis. A menor capacidade de processamento ou armazenamento destes dispositivos tornou essencial o aparecimento e crescimento de tecnologias que prometem solucionar muitos dos problemas identificados. O aparecimento do conceito de Middleware visa solucionar estas lacunas nos sistemas distribuidos mais evoluídos, promovendo uma solução a nível de organização e desenho da arquitetura dos sistemas, ao memo tempo que fornece comunicações extremamente rápidas, seguras e de confiança. Uma arquitetura baseada em Middleware visa dotar os sistemas de um canal de comunicação que fornece uma forte interoperabilidade, escalabilidade, e segurança na troca de mensagens, entre outras vantagens. Nesta tese vários tipos e exemplos de sistemas distribuídos e são descritos e analisados, assim como uma descrição em detalhe de três protocolos (XMPP, AMQP e DDS) de comunicação, sendo dois deles (XMPP e AMQP) utilzados em projecto reais que serão descritos ao longo desta tese. O principal objetivo da escrita desta tese é demonstrar o estudo e o levantamento do estado da arte relativamente ao conceito de Middleware aplicado a sistemas distribuídos de larga escala, provando que a utilização de um Middleware pode facilitar e agilizar o desenho e desenvolvimento de um sistema distribuído e traz enormes vantagens num futuro próximo.

Heterogeneous sensor database framework for the sensor observation service: integrating remote and in-situ sensor observations at the database backend

Dissertation submitted in partial fulfillment of the requirements for the Degree of Master of Science in Geospatial Technologies.

Sustainability of systems interoperability in dynamic business networks

Dissertação para obtenção do Grau de Doutor em Engenharia Electrotécnica e de Computadores

Positive solutions to find a job: Cultural mismatches between companies and employees

A Work Project, presented as part of the requirements for the Award of a Masters Degree in Management from the NOVA – School of Business and Economics

The role of s-nitrosothiols and rho-kinase 1 in glucose and lipid metabolism

RESUMO: Na sociedade contemporânea a diabetes tipo 2 e a obesidade estão a aumentar exponencialmente, representando um grave problema de saúde pública. De acordo com a IDF “A diabetes e a obesidade são o principal problema de saúde pública do século XXI’. Para além destas duas patologias, a prevalência de esteatose hepática não-alcoólica (NAFLD), entre a população obesa e diabética, é de cerca de 90%. O aumento da obesidade, diabetes e NAFLD tem uma forte correlação com o aumento do consumo de gorduras e açúcares, acompanhado de um decréscimo acentuado da actividade física. A obesidade, diabetes e NAFLD tem sido escrupolosamente investigada mas as terapêuticas disponíveis continuam a ser muito limitadas. Tendo em conta o número crescente e alarmante de obesos e diabéticos o conhecimento detalhado da patofisiologia da obesidade, diabetes e NAFLD, tendo em vista a necessidade extrema de desenvolvimento de novas estratégias terapêuticas, é da mais elevada urgência. O fígado é reconhecido como um orgão primordial no controlo da homeostase. No estado pós-prandial, o fígado converte a glucose em glicogénio e lípidos. Em contraste, no estado de jejum, o fígado promove a produção de glucose. Sistemas neuronais e hormonais, bem como o estado metabólico do fígado, controlam de forma muito precisa a alternância entre os diferentes substratos metabólicos, dependente do estado prandial. A insulina tem um papel central no controlo do metabolismo energético no fígado; se, por um lado, inibe a produção hepática de glucose e corpos cetónicos, por outro, promove a glicólise e a lipogénese. O metabolismo energético no fígado é também regulado por vários factores de transcrição e co-reguladores que, por sua vez, são regulados pela insulina, glucagina e outras hormonas metabólicas. Em conjunto, todos estes factores e reguladores vão controlar de forma muito estreita a gluconeogénese, a β-oxidação e a lipogénese, no fígado. Para além dos já conhecidos reguladores do metabolismo hepático, novas moléculas têm sido estudadas como tendo um papel fundamental na regulação do metabolismo energético no fígado. Qualquer desequilíbrio no metabolismo hepático vai contribuir para a insulino-resistência, NAFLD e diabetes tipo 2. O principal objectivo do trabalho de investigação aqui apresentado é o contributo para o estudo detalhado da patogénese da diabetes e obesidade, num contexto de dietas ricas em açúcares e gorduras, e com a perspectiva de explorar novas estratégias terapêuticas. Os objectivos específicos deste trabalho eram: primeiro, determinar se o tratamento com glutationo (GSH) e óxido nítrico (NO) era suficiente para melhorar a insulino-resistência associada ao elevado consumo de sacarose; segundo, determinar o papel da Rho-kinase 1 (ROCK1) na regulação do metabolismo hepático da glucose e dos lípidos; e terceiro, estudar o efeito do metilsulfonilmetano (MSM) em doenças metabólicas associadas à obesidade. Na primeira parte deste trabalho de investigação foram utilizados ratos Wistar machos sujeitos a uma dieta rica em sacarose (HS). Tal como esperado, estes animais apresentavam insulino-resistência e hiperinsulinémia. A dieta HS levou ao aumento dos níveis hepáticos de NO e ao decréscimo dos níveis de GSH no fígado. Em jejum, a administração intraportal de GSH e NO, a animais saudáveis promoveu um aumento significativo da sensibilidade à insulina. Também nestes animais, a administração intravenosa de S-nitrosotióis, compostos orgânicos que contém um grupo nitroso acoplado a um átomo de enxofre de um tiol, promoveu o aumento significativo da sensibilidade à insulina. Pelo contrário, em animais sujeitos à dieta HS, as doses padrão de GSH + NO e de S-nitrosotióis não conseguiram promover o aumento da sensibilidade à insulina. No entanto, ao aumentar a dose de S-nitrosotióis administrados por via intravenosa, foi possível observar o aumento da sensibilidade à insulina dependente da dose, indicando um possível papel dos S-nitrosotióis como sensibilizadores de insulina. O estudo detalhado do papel dos S-nitrosotióis na via de sinalização da insulina revelou que há um aumento da fosforilação do receptor da insulina (IR) e da proteína cinase B (Akt), sugerindo um efeito dos S-nitrosotióis nesta via de sinalização. Os resultados apresentados nesta primeira parte sugerem que os S-nitrosotióis promovem a correcta acção da insulina, podendo vir a ser importantes alvos terapêuticos. Na segunda parte deste trabalho de investigação utilizámos murganhos, com uma delecção específica da ROCK1 no fígado, e sujeitos a uma dieta rica em lípidos (HFD). Foi possível concluir que a ausência da ROCK1 no fígado previne a obesidade, melhora a sensibilidade à insulina e protege contra a esteatose hepática. A ausência de ROCK1 no fígado levou a um decréscimo significativo da expressão génica de genes associados à lipogénese, com uma diminuição acentuada do fluxo metabólico associado a esta via. Pelo contrário, a sobreexpressão de ROCK1, exclusivamente no fígado, promove a insulino-resistência e a esteatose hepática no contexto de obesidade induzida pela dieta. Para além disto, a delecção da ROCK1 no fígado de animais obesos e diabéticos, os murganhos deficientes em leptina, corroborou os dados obtidos no primeiro modelo animal, com a franca melhoria da hiperglicémia, hiperinsulinémia e esteatose hepática. Os dados que compõem esta parte do trabalho de investigação sugerem que a ROCK1 tem um papel crucial na regulação do metabolismo lipídico. Na terceira e última parte deste trabalho de investigação foi investigado o efeito do composto metilsulfunilmetano (MSM), um composto organosulfúrico naturalmente presente em plantas e utilizado também como suplemento dietético, em murganhos obesos e insulino-resistentes, por exposição a uma dieta rica em lípidos (DIO). O tratamento com MSM melhorou a insulino-resistência e protegeu contra a esteatose hepática. O conteúdo hepático em triglicéridos e colesterol também diminuíu de forma significativa nos animais DIO sujeitos ao tratamento com MSM, bem como a expressão génica associada à lipogénese. Para além disto, o tratamento com MSM levou a uma diminuição da expressão génica associada à inflamação. De realçar que o tratamento com MSM levou a uma melhoria do perfil hematopoiético destes animais, tanto na medula óssea como no sangue. Para comprovar o efeito benéfico do MSM na obesidade e insulino-resistência utilizámos murganhos deficientes no receptor da leptina, e por isso obesos e diabéticos, tendo observado um perfil semelhante ao obtido para murganhos sujeitos a uma dieta rica em lípidos e tratados com MSM. Concluímos, através dos dados recolhidos, que o MSM como suplemento pode ter efeitos benéficos na hiperinsulinémia, insulino-resistência e inflamação que caracterizam a diabetes tipo 2. Em resumo, os dados obtidos neste trabalho de investigação mostram que os S-nitrosotióis podem ter um papel importante como sensibilizadores da insulina, promovendo um aumento da sensibilidade à insulina num contexto de dietas ricas em sacarose. Para além disto, estudos in vitro, sugerem que os S-nitrosotióis regulam, especificamente, a via de sinalização da insulina. Este trabalho teve também como objectivo o estudo da ROCK1 como regulador do metabolismo da glucose e dos lípidos no fígado. Através do estudo de animais com uma delecção ou uma sobreexpressão da ROCK1 no fígado mostrou-se que esta tem um papel crucial na patogénese da obesidade e diabetes tipo 2, especificamente através do controlo da lipogénese de novo. Finalmente, foi também objectivo deste trabalho, explorar o efeito do MSM em animais DIO e deficientes em leptina. O tratamento com MSM protege de forma evidente contra a obesidade e insulino-resistência, com especial enfâse para a capacidade que esta molécula demonstrou ter na protecção contra a inflamação. Em conjunto os vários estudos aqui apresentados mostram que tanto os S-nitrosotióis como a ROCK1 têm um papel na patogénese da obesidade e diabetes tipo 2 e que a utilização de MSM como suplemento às terapêuticas convencionais pode ter um papel no tratamentos de doenças metabólicas.-------------------------------ABSTRACT: In modern western societies type 2 diabetes and obesity are increasing exponentially, representing a somber public concern. According to the International Diabetes Federation (IDF) ‘Diabetes and Obesity are the biggest public health challenges of the 21st century’. Aside from these the prevalence of nonalcoholic fatty liver disease (NAFLD), among the diabetic and obese population, is as high as 90%. It is now well established that the increase in obesity, diabetes and NAFLD strongly correlates with an increase in fat and sugar intake in our diet, alongside physical inactivity. The pathogenesis of obesity, diabetes and NAFLD has been thoroughly studied but the treatment options available are still narrow. Considering the alarming number in the obese and diabetic population the complete understanding of the pathogenesis, keeping in mind that new therapeutic strategies need to be attained, is of the highest urgency. The liver has been well established as a fundamental organ in regulating whole-body homeostasis. In the fed state the liver converts the glucose into glycogen and lipids. Conversely, in the fasted state, glucose will be produced in the liver. Neuronal and hormonal systems, as well as the hepatic metabolic states, tightly control the fast to fed switch in metabolic fuels. Insulin has a central role in controlling hepatic energy metabolism, by suppressing glucose production and ketogenesis, while stimulating glycolysis and lipogenesis. Liver energy metabolism is also regulated by various transcription factors and coregulators that are, in turn, regulated by insulin, glucagon and other metabolic hormones. Together, these regulators will act to control gluconeogenesis, β-oxidation and lipogenesis in the liver. Aside from the well-established regulators of liver energy metabolism new molecules are being studied has having a role in regulating hepatic metabolism. Any imbalance in the liver energy metabolism is a major contributor to insulin resistance, NAFLD and type 2 diabetes. The overall goal of this research work was to contribute to the understanding of the pathogenesis of diabetes and obesity, on a setting of high-sucrose and high-fat diets, and to explore potential therapeutic options. The specific aims were: first, to determine if treatment with glutathione (GSH) and nitric oxide (NO) was sufficient to ameliorate insulin resistance induced by high-sucrose feeding; second, to determine the physiological role of rho-kinase 1 (ROCK1) in regulating hepatic and lipid metabolism; and third, to study the effect of methylsulfonylmethane (MSM) on obesity-linked metabolic disorders. In the first part of this research work we used male Wistar rats fed a high-sucrose (HS) diet. As expected, rats fed a HS diet were insulin resistant and hyperinsulinemic. HS feeding increased hepatic levels of NO, while decreasing GSH. In fasted healthy animals administration of both GSH and NO, to the liver, was able to increase insulin sensitivity. Intravenous administration of S-nitrosothiols, organic compounds containing a nitroso group attached to the sulfur atom of a thiol, in fasted control animals also increased insulin sensitivity. Under HS feeding the standard doses of GSH + NO and S-nitrosothiols were unable to promote an increase in insulin sensitivity. However, the intravenous administration of increasing concentrations of S-nitrosothiols was able to restore insulin sensitivity, suggesting that S-nitrosothiols have an insulin sensitizing effect. Investigation of the effect of S-nitrosothiols on the insulin signaling pathway showed increased phosphorylation of the insulin receptor (IR) and protein kinase B (Akt), suggesting that S-nitrosothiols may have an effect on the insulin signaling pathway. Together, these data showed that S-nitrosothiols promote normal insulin action, suggesting that they may act as potential pharmacological tools. In the second part of this research work we used liver-specific ROCK1 knockout mice fed a high-fat (HF) diet. Liver-specific deletion of ROCK1 prevented obesity, improved insulin sensitivity and protected against hepatic steatosis. Deficiency of ROCK1 in the liver caused a significant decrease in the gene expression of lipogenesis associated gene, ultimately leading to decreased lipogenesis. Contrariwise, ROCK1 overexpression in the liver promoted insulin resistance and hepatic steatosis in diet-induced obesity. Furthermore, liver-specific deletion of ROCK1 in obese and diabetic mice, the leptin-deficient mice, improved the typical hyperglycemia, hyperinsulinemia and liver steatosis. Together, these data identify ROCK1 as a crucial regulator of lipid metabolism. In the third and final part of this research work we investigated the effect of MSM, an organosulfur compound naturally found in plants and used as a dietary supplement, on diet-induced obese (DIO) and insulin resistant mice. MSM treatment ameliorated insulin resistance and protected against hepatosteatosis. Hepatic content in triglycerides and cholesterol was significantly decreased by MSM treatment, as well as lipogenesis associated gene expression. Furthermore, MSM treated mice had decreased inflammation associated gene expression in the liver. Importantly, FACS analysis showed that MSM treatment rescued the inflammatory hematopoietic phenotype of DIO mice in the bone marrow and the peripheral blood. Moreover, MSM treatment of the obese and diabetic mice, the leptin-deficient mice, resulted in similar effects as the ones observed for DIO mice. Collectively, these data suggest that MSM supplementation has a beneficial effect on hyperinsulinemia, insulin resistance and inflammation, which are often found in type 2 diabetes. In conclusion, this research work showed that S-nitrosothiols may play a role as insulin sensitizers, restoring insulin sensitivity in a setting of high-sucrose induced insulin resistance. Furthermore, in vitro studies suggest that S-nitrosothiols specifically regulate the insulin signaling pathway. This research work also investigated the role of hepatic ROCK1 in regulation of glucose and lipid metabolism. Using liver-specific ROCK 1 knockout and ROCK1 overexpressing mice it was shown that ROCK1 plays a role in the pathogenesis of obesity and type 2 diabetes, specifically through regulation of the de novo lipogenesis pathway. Finally, this research work aimed to explore the effect of MSM in DIO and leptin receptor-deficient mice. MSM strongly protects against obesity and insulin resistance, moreover showed a robust ability to decrease inflammation. Together, the individual studies that compose this dissertation showed that S-nitrosothiols and ROCK1 play a role in the pathogenesis of obesity and type 2 diabetes and that MSM supplementation may have a role in the treatment of metabolic disorders.

Influence of constituent yarn systems on the moisture management performance of terry fabrics

Objetivo do presente trabalho foi estudar a influência dos diferentes sistemas de fios (trama, teia de base e teia da argola) no desempenho dos tecidos de felpos, no que concerne às propriedades de absorção, capilaridade e libertação de humidade. Para este estudo usaram-se quatro tipos de combinações destes sistemas de fios, para a mesma estrutura de tecidos de felpo, na teia de base utilizou-se somente fios de Tencel®, na teia de argola e da trama varou-se a composição dos fios entre fios de algodão e de Tencel®. Os resultados obtidos demonstram que quando a utilização fios de Tencel® em qualquer dos sistemas (trama ou teia da argola) favorece a capacidade de difusão de líquidos na estrutura, a utilização de fios de algodão na teia de argola favorece a capacidade de absorção.

The influence of nitrogen and oxygen additions on the thermal characteristics of aluminium-based thin films

The ternary aluminium oxynitride (AlNxOy) system offers the possibility to obtain a wide range of properties by tailoring the ratio between pure Al, AlNx and AlOy and therefore opening a significant number of possible applications. In this work the thermal behaviour of AlNxOy thin films was analysed by modulated infrared radiometry (MIRR), taking as reference the binary AlOy and AlNx systems. MIRR is a non-contact and non-destructive thermal wave measurement technique based on the excitation, propagation and detection of temperature oscillations of very small amplitudes. The intended change of the partial pressure of the reactive gas (N2 and/or O2) influenced the target condition and hence the deposition characteristics which, altogether, affected the composition and microstructure of the films. Based on the MIRR measurements and their qualitative and quantitative interpretation, some correlations between the thermal transport properties of the films and their chemical/physical properties have been found. Furthermore, the potential of such technique applied in this oxynitride system, which present a wide range of different physical responses, is also discussed. The experimental results obtained are consistent with those reported in previous works and show a high potential to fulfil the demands needed for the possible applications of the systems studied. They are clearly indicative of an adequate thermal response if this particular thin film system is aimed to be applied in small sensor devices or in electrodes for biosignal acquisition, such as those for electroencephalography or electromyography as it is the case of the main research area that is being developed in the group.

Biocatalysis in micellar systems

[Excert] Biocatalysis and biotransformations are environmentally friendly, and allow the development of sustainable production processes on a large scale. Thus, these processes are becoming important alternatives to conventional chemistry in the drug, biochemical, and emerging biorenewable energy industries. Biocatalysts are required to function under non-conventional conditions, such as in organic solvents, being competitive in terms of cost and efficiency. In fact, the technological utility of enzymes can be enhanced greatly by using them in the presence of organic solvents, rather than in their natural aqueous reaction media. Multiphase systems are more complex but offer a new field of possibilities. The presence of hydrophobic solvents in biocatalysis allows the conversion of poorly water soluble substrates more efficiently. The accessibility of hydrophobic substrates to enzymes or whole cells presents an interesting challenge for researchers and technologists. In this context, microemulsions are a promising tool in enzyme technology. This chapter presents an overview of the characterization of biphasic and microemulsion systems and their applications in biotransformation processes (...).

Biblioteca de referência de DNA barcodes de bivalves (Mollusca: Bivalvia) e gastrópodes (Mollusca: Gastropoda) da costa Portuguesa

Dissertação de mestrado em Ecologia

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.