Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)

Este trabalho apresenta uma técnica de verificação formal de Sistemas de Raciocínio Procedural, PRS (Procedural Reasoning System), uma linguagem de programação que utiliza a abordagem do raciocínio procedural. Esta técnica baseia-se na utilização de regras de conversão entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, são apresentadas regras de conversão de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verificação formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verificação das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional disponível para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de conversão PRS-RPC, podemos ser levados a querer fazer esta conversão de maneira estritamente manual. No entanto, a probabilidade de introdução de erros na conversão é grande, fazendo com que o esforço necessário para garantirmos a corretude da conversão manual seja da mesma ordem de grandeza que a eliminação de eventuais erros diretamente no programa PRS original. Assim, a conversão automatizada é de suma importância para evitar que a conversão manual nos leve a erros indesejáveis, podendo invalidar todo o processo de conversão. A principal contribuição deste trabalho de pesquisa diz respeito ao desenvolvimento de uma técnica de verificação formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de conversão de PRS para RPC. A segunda fase é concernente ao desenvolvimento de um conversor para fazer a transformação de maneira automatizada dos programas PRS para as RPCs. A conversão automática é possível, porque todas as regras de conversão apresentadas seguem leis de formação genéricas, passíveis de serem incluídas em algoritmos

Caracterização infravermelho e distribuição espectral de energia para as estrelas com planetas

Neste trabalho estudamos o comportamento das estrelas pertencentes a sistemas planetários no que diz respeito às suas características infravermelho e à distribuição espectral de energia (SED). Nosso estudo tem como base uma análise detalhada do comportamento da emissão no infravermelho de 48 estrelas com planetas, classificadas como estrelas da seqüência principal, subgigantes ou gigantes. Foram analisados dados de fotometria infravermelho nas bandas 12, 25 e 60µm do catálogo de fontes IRAS puntiformes (IPSC) e nas bandas JHK do projeto 2 Micron All Sky Survey (2MASS). A partir do cálculo da discrepância na posição de apontamento da fonte e do cálculo do índice de cor, selecionamos e localizamos os objetos no diagrama de cor-cor do IRAS. Este diagrama permite-nos identificar possíveis objetos detentores de disco de poeira. Fizemos também uma análise da distribuição espectral de energia onde observamos também traços de excesso de fluxo no infravermelho, com isso, confirmarmos a presença do disco de poeira nos objetos identificados no diagrama de cor. Apesar da atual amostra de estrelas com planetas incluir apenas um subconjunto de estrelas com planetas detectadas na vizinhança solar, a presente análise do fluxo infravermelho nesses objetos oferecem uma possibilidade única de estudar as características infravermelho das estrelas pertencentes aos sistemas planetários extra-solar. Neste contexto, nosso estudo aponta resultados interessantes, entre outros destacamos o fato de algumas estrelas com planetas apresentarem um peculiar fluxo IRAS [60-25], indicando a co-existência de poeira juntamente com os planetas destes sistemas extra solar

Histerese térmica de sistemas magnéticos nanoestruturados

We report a theoretical investigation of thermal hysteresis in magnetic nanoelements. Thermal hysteresis originates in the existence of meta-stable states in temperature intervals which may be tuned by small values of the external magnetic field, and are controlled by the systems geometric dimensions as well as the composition. Two systems have been investigated. The first system is a trilayer consisting of one antiferromagnetic MnF2 film, exchange coupled with two Fe lms. At low temperatures the ferromagnetic layers are oriented in opposite directions. By heating in the presence of an external magnetic field, the Zeeman energy induces a gradual orientation of the ferromagnets with the external field and the nucleation of spin- op-like states in the antiferromagnetic layer, leading eventually, in temperatures close to the Neel temperature, to full alignment of the ferromagnetic films and the formation of frustrated exchange bonds in the center of the antiferromagnetic layer. By cooling down to low temperatures, the system follows a different sequence of states, due to the anisotropy barriers of both materials. The width of the thermal hysteresis loop depends on the thicknesses of the FM and AFM layers as well as on the strength of the external field. The second system consists in Fe and Permalloy ferromagnetic nanoelements exchange coupled to a NiO uncompensated substrate. In this case the thermal hysteresis originates in the modifications of the intrinsic magnetic