Interpretação de imagens multitemporais de sensoriamento remoto.

Estudos multitemporais de dados de sensoriamento remoto dedicam-se ao mapeamento temático de uso da terra em diferentes instâncias de tempo com o objetivo de identificar as mudanças ocorridas em uma região em determinado período. Em sua maioria, os trabalhos de classificação automática supervisionada de imagens de sensoriamento remoto não utilizam um modelo de transformação temporal no processo de classificação. Pesquisas realizadas na última década abriram um importante precedente ao comprovarem que a utilização de um modelo de conhecimento sobre a dinâmica da região (modelo de transformação temporal), baseado em Cadeias de Markov Fuzzy (CMF), possibilita resultados superiores aos produzidos pelos classificadores supervisionados monotemporais. Desta forma, o presente trabalho enfoca um dos aspectos desta abordagem pouco investigados: a combinação de CMF de intervalos de tempo curtos para classificar imagens de períodos longos. A área de estudo utilizada nos experimentos é um remanescente florestal situado no município de Londrina-PR e que abrange todo o limite do Parque Estadual Mata dos Godoy. Como dados de entrada, são utilizadas cinco imagens do satélite Landsat 5 TM com intervalo temporal de cinco anos. De uma forma geral, verificou-se, a partir dos resultados experimentais, que o uso das Cadeias de Markov Fuzzy contribuiu significativamente para a melhoria do desempenho do processo de classificação automática em imagens orbitais multitemporais, quando comparado com uma classificação monotemporal. Ainda, pôde-se observar que as classificações com base em matrizes estimadas para períodos curtos sempre apresentaram resultados superiores aos das classificações com base em matrizes estimadas para períodos longos. Também, que a superioridade da estimação direta frente à extrapolação se reduz com o aumento da distância temporal. Os resultados do presente trabalho poderão servir de motivação para a criação de sistemas automáticos de classificação de imagens multitemporais. O potencial de sua aplicação se justifica pela aceleração do processo de monitoramento do uso e cobertura da terra, considerando a melhoria obtida frente a classificações supervisionadas tradicionais.

Restauração de imagens de microscopia de força atômica com uso da regularização de Tikhonov via processamento em GPU

A Restauração de Imagens é uma técnica que possui aplicações em várias áreas, por exemplo, medicina, biologia, eletrônica, e outras, onde um dos objetivos da restauração de imagens é melhorar o aspecto final de imagens de amostras que por algum motivo apresentam imperfeições ou borramentos. As imagens obtidas pelo Microscópio de Força Atômica apresentam borramentos causados pela interação de forças entre a ponteira do microscópio e a amostra em estudo. Além disso apresentam ruídos aditivos causados pelo ambiente. Neste trabalho é proposta uma forma de paralelização em GPU de um algoritmo de natureza serial que tem por fim a Restauração de Imagens de Microscopia de Força Atômica baseado na Regularização de Tikhonov.

Estudo em Escala Piloto de Parâmetros de Monitoramento e Operação de Biopilhas no Tratamento de Solos Contaminados por Hidrocarbonetos de Petróleo

O objetivo do trabalho foi identificar ferramentas e indicadores adequados ao monitoramento e à otimização de processos de biorremediação, incluindo parâmetros físicos, químicos e microbiológicos definidos em estudos de tratabilidade de solos contaminados por óleo cru em escala de laboratório e comparar estratégias de biorremediação, tais como bioestímulo e bioaumento conduzidas em simulações de biopilhas dinâmicas ou estáticas. Quando três métodos de extração de hidrocarbonetos de petróleo de solo arenoso e franco-argiloso para análise cromatográfica (Soxhlet-SOX, microondas-MARS e extração acelerada por solvente-ASE) foram comparados entre si, concluiu-se que a técnica que promove a melhor recuperação depende da fração de interesse (n-alcanos, HRP, MCNR, HPA), das características texturais do solo (teores de areia, silte e argila) e da idade da contaminação. Dentre os indicadores de densidade populacional microbiana (microrganismos heterotróficos totais-PHT, população de fungos-PF e população microbiana degradadora de óleo (PDO) passíveis de utilização para indicar a taxa de degradação de compostos orgânicos presentes no solo tais como os hidrocarbonetos de petróleo, o PDO mostrou-se o mais adequado em conjunto com a produção de CO2 aferida pelo método respirométrico. Quando a estratégia de biorremediação de solo franco-argiloso contaminado com óleo cru a 3% (m m-1) utilizando bioestímulo (ajuste de pH, umidade e taxa C:N:P) foi comparada ao bioaumento (bioestímulo e adição de inóculo de microrganismos extraídos, enriquecidos e aclimatizados ao óleo cru como fonte de carbono), em sistemas de bancada simulando biopilha dinâmica (microcosmo M) e biopilha estática com aeração forçada (reator B), o tratamento que apresentou melhor remoção (32%) de HTP após 121 dias foi o bioaumento em biopilha estática. Para HPA, o tratamento que alcançou a melhor remoção (33%) foi com bioestímulo também em biopilha estática. A avaliação da taxa de mortalidade (%) de Eisenia andrei exposta tanto a solos recém-contaminados por óleo cru e preparados para bioestímulo (BIOS) e bioaumento (BIOA) a serem tratados em biopilhas dinâmicas e estáticas em escala de laboratório mostrou que após 56 dias de exposição da E. andrei, todos os solos produziram letalidade de 100%, quer fossem os solos recém-contaminados e preparados para os diferentes tratamentos (BIOS M, BIOS B, BIOA M, BIOA B) ou após 121 dias de tratamento. Tal resultado confirma que a biorremediação foi incipiente também do ponto de vista de remoção da ecotoxicidade. Em linhas gerais, a biorremediação de solo franco-argiloso contaminado por óleo cru, contendo tanto contaminação antiga quanto recente, reúne os maiores desafios à biorremediação, tanto do ponto de vista da composição textural do solo quanto da natureza do contaminante. Os processos são aparentemente lentos e requerem ferramentas auxiliares para aceleração dos mesmos. Recomenda-se no futuro, condução de experimentos com o uso de diferentes surfactantes, com ênfase em biosurfactantes

Ancient DNA from South-East Europe Reveals Different Events during Early and Middle Neolithic Influencing the European Genetic Heritage

The importance of the process of Neolithization for the genetic make-up of European populations has been hotly debated, with shifting hypotheses from a demic diffusion (DD) to a cultural diffusion (CD) model. In this regard, ancient DNA data from the Balkan Peninsula, which is an important source of information to assess the process of Neolithization in Europe, is however missing. In the present study we show genetic information on ancient populations of the South-East of Europe. We assessed mtDNA from ten sites from the current territory of Romania, spanning a time-period from the Early Neolithic to the Late Bronze Age. mtDNA data from Early Neolithic farmers of the Starcevo Cris culture in Romania (Carcea, Gura Baciului and Negrilesti sites), confirm their genetic relationship with those of the LBK culture (Linienbandkeramik Kultur) in Central Europe, and they show little genetic continuity with modern European populations. On the other hand, populations of the Middle-Late Neolithic (Boian, Zau and Gumelnita cultures), supposedly a second wave of Neolithic migration from Anatolia, had a much stronger effect on the genetic heritage of the European populations. In contrast, we find a smaller contribution of Late Bronze Age migrations to the genetic composition of Europeans. Based on these findings, we propose that permeation of mtDNA lineages from a second wave of Middle-Late Neolithic migration from North-West Anatolia into the Balkan Peninsula and Central Europe represent an important contribution to the genetic shift between Early and Late Neolithic populations in Europe, and consequently to the genetic make-up of modern European populations.

Caracterização química de um solo contaminado por resíduos sólidos urbanos na estrada Arroio Pavuna em Jacarepaguá no município Rio de Janeiro

Neste trabalho, escolheu-se a estrada canal Arroio Pavuna, em Jacarepaguá, para avaliar quimicamente a qualidade do solo que recebe diariamente resíduos sólidos urbanos. A região deste estudo é também conhecida como estrada do Urubu, sendo este animal um dos principais vetores presente no local. Para uma caracterização química, foram determinados pH, carbono orgânico, matéria orgânica, concentrações dos metais alumínio, cádmio, chumbo, cobre, cromo, ferro, níquel e zinco, utilizando a técnica de Absorção Atômica por Chama, além da identificação dos principais compostos orgânicos através da técnica de Cromatografia Gasosa acoplada a Espectrometria de Massas. Também foi realizado o teste de comportamento com oligoquetas da espécie Eisenia andrei para avaliar a função de habitat do solo analisado. Os resultados obtidos apontaram que a região apresenta um solo ácido na faixa de 5,51 a 6,70, bem como as concentrações de Cobre, Cromo, Níquel e Zinco acima dos valores orientadores de referência de qualidade dos solos, um teor médio de matéria orgânica na faixa de 21,71 g.kg-1 a 29,73 g.kg-1, além de presença de compostos orgânicos com estruturas muito complexas. O solo apresentou função de habitat limitada. E como sugestão para a remediação deste solo, a fitorremediação apresenta bons rendimentos na literatura para remoção parcial ou total desses metais

O uso de fosfatos associado à fitorremediação em solos de Santo Amaro (BA) contaminados por metais tóxicos

A contaminação do solo no município de Santo Amaro (BA) por metais tóxicos provocada pelas atividades da empresa Plumbum Mineração tem gerado impactos sobre a saúde ambiental e humana. O objetivo da presente pesquisa foi avaliar a viabilidade da remediação deste solo contaminado por chumbo e cádmio, utilizando diferentes fontes de fosfatos e fitorremediação com o capim vetiver [Vetiveria zizanioides (L.)]. O estudo foi realizado em colunas de PVC onde amostras de solo foram colocadas com a aplicação de fosfato dihidrogênio de potássio (KH2PO4) (T1); fertilizante fosfato natural reativo (FNR) (T2) e; uma mistura do KH2PO4 e de fertilizante FNR (T3). Amostras de solo contaminado sem tratamento (T0) foram utilizadas como controle. Após 60, 120 e 180 dias, alíquotas do solo foram retiradas das colunas para análises. Ao final de cada período, mudas de capim vetiver [(Vetiveria zizanioides (L.)] foram plantadas em vasos com as amostras de solo: T0, T1, T2 e T3 em triplicata. Para a determinação das concentrações de chumbo e cádmio no solo e tecidos vegetais foi utilizado o ICP-OES. A partir das análises física e química constatou-se que o solo possui textura argilosa e capacidade de troca catiônica (CTC) elevadas. As extrações com solução de ácido dietilenotriaminopentaacético (DTPA) e Toxicity Characteristic Leaching Procedure (TCLP) mostraram que o tratamento T1 seguido do T3 foram os mais eficientes na imobilização de Pb e Cd. Entretanto, todos os tratamentos resultaram em concentrações de metais ainda disponíveis no solo que excediam os limites estabelecidos pela USEPA, sendo o solo, portanto, considerado tóxico mesmo após o tratamento. Com base nas concentrações de metais extraídos através da extração sequencial pelo método BCR após a remediação e a fitorremediação do solo, foi verificado que todos os três tratamentos com fosfatos foram eficientes em imobilizar o Pb e Cd nas formas menos solúveis, porém, o Cd permaneceu mais solúvel e com maior mobilidade do que o Pb. Os ensaios de letalidade utilizando minhoca Eisenia andrei mostraram que a mortalidade observada no solo após 60 dias de tratamento foi significativamente reduzida após 120 e 180 dias de tratamento. A perda de biomassa pelas minhocas também foi reduzida de acordo com o tempo de tratamento. O teste de germinação com alfaces (Lactuca sativa L.) indicou que as amostras de solo tratadas continuam bastante tóxicas, apesar da disponibilidade reduzida do Pb e do Cd como visto nos resultados da extração por TCLP e por BCR. A avaliação de risco ecológico potencial indicou que os tratamentos do solo com fosfatos associado à fitorremediação reduziram a mobilidade do Pb, principalmente nos tratamentos T1 e T3. Para o Cd o risco ecológico potencial aumenta consideravelmente quando comparado com o Pb demonstrando que esse elemento, apesar dos tratamentos com fosfatos mais a fitorremediação continua móvel. O tratamento com KH2PO4 (T1) foi o mais eficiente na redução da mobilidade, disponibilidade e da toxicidade dos metais, seguido pelo T3 e T2 para o Pb e o T3 seguido pelo T1 e T2 para o Cd.

Safe Compositional Network Sketches: NetSketch Tool Implementation

Numerous problems exist that can be modeled as traffic through a network in which constraints exist to regulate flow. Vehicular road travel, computer networks, and cloud based resource distribution, among others all have natural representations in this manner. As these networks grow in size and/or complexity, analysis and certification of the safety invariants becomes increasingly costly. The NetSketch formalism introduces a lightweight verification framework that allows for greater scalability than traditional analysis methods. The NetSketch tool was developed to provide the power of this formalism in an easy to use and intuitive user interface.

Lightweight Formal Methods for the Development of High-Assurance Networking Systems

We survey several of the research efforts pursued by the iBench and snBench projects in the CS Department at Boston University over the last half dozen years. These activities use ideas and methodologies inspired by recent developments in other parts of computer science -- particularly in formal methods and in the foundations of programming languages -- but now specifically applied to the certification of safety-critical networking systems. This is research jointly led by Azer Bestavros and Assaf Kfoury with the participation of Adam Bradley, Andrei Lapets, and Michael Ocean.

Improving the Accessibility of Lightweight Formal Verification Systems

In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, broad accessibility has not been a priority in the design of formal verification tools that can provide these benefits. We propose a few design criteria to address these issues: a simple, familiar, and conventional concrete syntax that is independent of any environment, application, or verification strategy, and the possibility of reducing workload and entry costs by employing features selectively. We demonstrate the feasibility of satisfying such criteria by presenting our own formal representation and verification system. Our system’s concrete syntax overlaps with English, LATEX and MediaWiki markup wherever possible, and its verifier relies on heuristic search techniques that make the formal authoring process more manageable and consistent with prevailing practices. We employ techniques and algorithms that ensure a simple, uniform, and flexible definition and design for the system, so that it easy to augment, extend, and improve.

Safe Compositional Network Sketches: Tool & Use Cases

NetSketch is a tool that enables the specification of network-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system so as to retain sufficient enough details to enable future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis approach based on a strongly-typed, Domain-Specific Language (DSL) to specify network configurations at various levels of sketchiness along with invariants that need to be enforced thereupon. In this paper, we overview NetSketch, highlight its salient features, and illustrate how it could be used in applications, including the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications). In a companion paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch's user-interface when used in "sketch mode", and prove its soundness relative to appropriately-defined notions of validity.

Safe Compositional Network Sketches: The Formal Framework

NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system while retaining sufficient information about it to carry out future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis. The compositional analysis is based on a strongly-typed Domain-Specific Language (DSL) for describing and reasoning about constrained-flow networks at various levels of sketchiness along with invariants that need to be enforced thereupon. In this paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch's user-interface when used in "sketch mode", and prove its soundness relative to appropriately-defined notions of validity. In a companion paper [6], we overview NetSketch, highlight its salient features, and illustrate how it could be used in two applications: the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications).

Verification with Natural Contexts: Soundness of Safe Compositional Network Sketches

In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work [30] we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. In this report we evaluate our proposed design criteria by utilizing within the context of novel research a formal reasoning system that is designed according to these criteria. In particular, we consider how the design and capabilities of the formal reasoning system that we employ influence, aid, or hinder our ability to accomplish a formal reasoning task – the assembly of a machine-verifiable proof pertaining to the NetSketch formalism. NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. It provides capabilities for compositional analysis based on a strongly-typed domain-specific language (DSL) for describing and reasoning about constrained-flow networks and invariants that need to be enforced thereupon. In a companion paper [13] we overview NetSketch, highlight its salient features, and illustrate how it could be used in actual applications. In this paper, we define using a machine-readable syntax major parts of the formal system underlying the operation of NetSketch, along with its semantics and a corresponding notion of validity. We then provide a proof of soundness for the formalism that can be partially verified using a lightweight formal reasoning system that simulates natural contexts. A traditional presentation of these definitions and arguments can be found in the full report on the NetSketch formalism [12].

Lightweight Formal Verification in Classroom Instruction of Reasoning about Functional Code

In college courses dealing with material that requires mathematical rigor, the adoption of a machine-readable representation for formal arguments can be advantageous. Students can focus on a specific collection of constructs that are represented consistently. Examples and counterexamples can be evaluated. Assignments can be assembled and checked with the help of an automated formal reasoning system. However, usability and accessibility do not have a high priority and are not addressed sufficiently well in the design of many existing machine-readable representations and corresponding formal reasoning systems. In earlier work [Lap09], we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. We report on our attempt to evaluate our proposed design criteria by deploying within the classroom a lightweight formal verification system designed according to these criteria. The lightweight formal verification system was used within the instruction of a common application of formal reasoning: proving by induction formal propositions about functional code. We present all of the formal reasoning examples and assignments considered during this deployment, most of which are drawn directly from an introductory text on functional programming. We demonstrate how the design of the system improves the effectiveness and understandability of the examples, and how it aids in the instruction of basic formal reasoning techniques. We make brief remarks about the practical and administrative implications of the system’s design from the perspectives of the student, the instructor, and the grader.

Efficient Support for Common Relations in Lightweight Formal Reasoning Systems

In work that involves mathematical rigor, there are numerous benefits to adopting a representation of models and arguments that can be supplied to a formal reasoning or verification system: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work [Lap09a], we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. This work expands one aspect of the earlier work by considering more extensively an essential capability for any formal reasoning system whose design is oriented around simulating the natural context: native support for a collection of mathematical relations that deal with common constructs in arithmetic and set theory. We provide a formal definition for a context of relations that can be used to both validate and assist formal reasoning activities. We provide a proof that any algorithm that implements this formal structure faithfully will necessary converge. Finally, we consider the efficiency of an implementation of this formal structure that leverages modular implementations of well-known data structures: balanced search trees and transitive closures of hypergraphs.