Estendendo CRefine para o suporte de táticas de refinamento

The use of increasingly complex software applications is demanding greater investment in the development of such systems to ensure applications with better quality. Therefore, new techniques are being used in Software Engineering, thus making the development process more effective. Among these new approaches, we highlight Formal Methods, which use formal languages that are strongly based on mathematics and have a well-defined semantics and syntax. One of these languages is Circus, which can be used to model concurrent systems. It was developed from the union of concepts from two other specification languages: Z, which specifies systems with complex data, and CSP, which is normally used to model concurrent systems. Circus has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise these application as a refinement tactic, which can then be used as a single transformation rule. CRefine was developed to support the Circus refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. The aim of this work is to provide tool support for refinement tactics. For that, we develop a new module in CRefine, which automates the process of defining and applying refinement tactics that are formalised in the tactic language ArcAngelC. Finally, we validate the extension by applying the new module in a case study, which used the refinement tactics in a refinement strategy for verification of SPARK Ada implementations of control systems. In this work, we apply our module in the first two phases of this strategy

Um método semi-automatizado para elicitação de requisitos de acessibilidade Web

In the context of Software Engineering, web accessibility is gaining more room, establishing itself as an important quality attribute. This fact is due to initiatives of institutions such as the W3C (World Wide Web Consortium) and the introduction of norms and laws such as Section 508 that underlie the importance of developing accessible Web sites and applications. Despite these improvements, the lack of web accessibility is still a persistent problem, and could be related to the moment or phase in which this requirement is solved within the development process. From the moment when Web accessibility is generally regarded as a programming problem or treated when the application is already developed entirely. Thus, consider accessibility already during activities of analysis and requirements specification shows itself a strategy to facilitate project progress, avoiding rework in advanced phases of software development because of possible errors, or omissions in the elicitation. The objective of this research is to develop a method and a tool to support requirements elicitation of web accessibility. The strategy for the requirements elicitation of this method is grounded by the Goal-Oriented approach NFR Framework and the use of catalogs NFRs, created based on the guidelines contained in WCAG 2.0 (Web Content Accessibility Guideline) proposed by W3C

Prevenção de conflitos médico-legais no exercício da medicina

Os conflitos médico-legais que ocorrem no exercício da Cirurgia e da Medicina são motivos de preocupação não só no meio médico, mas também na sociedade como um todo, pois se de um lado geram um maior desgaste emocional ao médico, por outro, os pacientes estão sendo rejeitados. As causas desses conflitos são muitas, envolvendo fatores não assistenciais, como o sistema de saúde distorcido e desorganizado, a falta de participação da sociedade e do médico na melhoria desse sistema, o aparelho formador que lança no mercado grande número de jovens médicos despreparados para o exercício dessa nobre profissão, além da falta do ensino continuado. A solução para esses conflitos não poderá ser por meio de simples criação de leis, e nem pela negativa da existência do erro médico, que ocorre numa freqüência até maior do que os próprios conflitos. Todavia, pode-se afirmar que é muito importante melhorar a relação médico-paciente. É necessário, ainda, que o médico conheça a fundo seus deveres de conduta e que, principalmente, se abstenha de praticar abusos do poder. A sociedade deve também entender que a saúde não é uma questão exclusiva dos médicos e que deve lutar pela melhoria das condições dos níveis de vida.

Poluição sonora: um grave problema na cidade de Mossoró-RN

In the latest decades, we have observed some environment alterations of big proportions in our planet. Sound pollution, visual pollution, water pollution, air pollution, soil pollution, all the principal kinds of environment pollution have raised in the path of economy development. In Mossoró it is not different; the environment has suffered a long and continuous damage caused by predatory abuse. The river is polluted, the ciliar vegetation of Carnauba was totally altered and with it a part of the local fauna disappeared. In fact, the city urban environment has, and continues to be, deeply altered and the sound pollution is a reflex of the urban modifications undergone in the city as time goes by. Through bibliographic review, the gauging of noise and fieldwork, this research project had the objective of analyzing the principal activities that cause sound pollution in the urban perimeter of the city of Mossoró, RN, emphasizing the causes, effects and spacial distribution of the polluter agents, as well as understanding how the environmental laws treat the sound issue in the urban environment of the city. The President Dutra avenue, where popular events of Mossoró take place and an important access for the city, was the chosen place to study this pollution that became, recently, another hindrance that interferes on the life quality of the local population. The results of this brief research emphasizes the urgency to alert society, specially about the importance of law and public organs that are located in our city, therefore solving problems such as the aforementioned above

Percepção e ações educativas em ambientes escolares: enfoques aos documentos legais determinantes em área de proteção ambiental

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior

Fatores de sucesso ou insucesso do turismo ambientalmente sustentável : percepção das autoridades públicas no pólo costa das dunas do Rio Grande do Norte

This study aims to compare the thermal performance of tiles made from recycled material (waste packaging cardboard with aluminized film) with the tiles of fiber and bitumen, fiber cement and red ceramic with the aim of verifying the suitability of tile to be used in hot and humid climate of low latitude. The samples were selected according to the availability from Natal RN market, as they are sold to the consumers. The methodology was based on studies that used experimental apparatus composed of thermal chambers heated by banks of incandescent bulbs, to analyze the thermal performance of materials. The tiles in the study were submitted to analysis of thermal performance, thermophysical properties and absorptance, using chambers of thermal performance, measuring the thermophysical properties and portable spectrometer, respectively. Comparative analysis of thermal performance between two samples of the recycled material with dimple sizes and different amounts of aluminum were made, in order to verify, if these characteristics had some interference on the thermal performance of them; the results showed no significant performance differences between the samples. The data obtained in chambers of thermal performance and confirmed by statistical analysis, showed, that the tile of recycled material have similar thermal performance to the tile of fiber cement. In addition to these tests was carried out the automatic monitoring of a building covered with tiles of recycled material, to verify its thermal performance in a real situation. The results showed that recycled shingles must be used with technical criteria similar to those used for fiber cement tiles, with regard to the heat gain into the building. Within these criteria should be taken into account local characteristics, especially in regions with hot and humid climate, and its use must be associated, according to the literature, to elements of thermal insulation and use of passive techniques such as vented attics, ceilings and right foot higher

Aplicação de resíduo industrial para isolamento térmico: uma proposta para utilização do poliuretano de mamona com agregado de resíduo plástico termofixo

A aplicação de isolantes térmicos em sistemas construtivos promove vantagens com vistas ao conforto térmico de ambientes. E com isso, o aumento da produtividade em locais de trabalho, a sensação de bem-estar e a diminuição dos custos com climatização. A demanda por conforto ambiental, no âmbito da isolação térmica, somada ao advento de novas leis que regulam os requisitos mínimos de conforto, as exigências dos consumidores pela adoção de métodos de produção mais “limpos”, a fiscalização quanto à destinação de resíduos industriais, além da inserção de produtos no mercado com apelos ambientais, incentivaram o desenvolvimento da presente pesquisa. O presente trabalho trata da aplicação do poliuretano, visando comparar o desempenho térmico do derivado de origem vegetal (óleo de mamona) com adição de resíduo plástico termofixo em diferentes proporções (5%, 10%, 15% e 20%), com o poliuretano petrolífero, a lã de vidro e a lã de rocha através da análise de suas propriedades térmicas (condutividade térmica – k, difusividade térmica – e capacidade calorífica – Cp). . Após a realização dos ensaios, os compósitos estudados foram moídos e reutilizados como carga para novos compósitos. Com base nos resultados dos ensaios de propriedades térmicas, constatou-se que o material desenvolvido conduz menos calor que o poliuretano de petróleo, a lã de vidro e a lã de rocha, além de oferecer alta inércia térmica, bom desempenho térmico e baixo custo. Assim como foi comprovada a possibilidade de fabricação de novos compósitos para fins de isolamento, reutilizando os compósitos testados

Controlador adaptativo backstepping a estrutura variável

Neste trabalho, um controlador adaptativo backstepping a estrutura variável (Variable Structure Adaptive Backstepping Controller, VS-ABC) é apresentado para plantas monovariáveis, lineares e invariantes no tempo com grau relativo unitário. Ao invés das tradicionais leis integrais para estimação dos parâmetros da planta, leis chaveadas são utilizadas com o objetivo de aumentar a robustez em relação a incertezas paramétricas e distúrbios externos, bem como melhorar o desempenho transitório do sistema. Adicionalmente, o projeto do novo controlador é mais intuitivo quando comparado ao controlador backstepping original, uma vez que os relés introduzidos apresentam amplitudes diretamente relacionadas com os parâmetros nominais da planta. Esta nova abordagem, com uso de estrutura variável, também reduz a complexidade das implementações práticas, motivando a utilização de componentes industriais, tais como, FPGAs (Field Programmable Gate Arrays ), MCUs (Microcontrollers) e DSPs (Digital Signal Processors). Simulações preliminares para um sistema instável de primeira e segunda ordem são apresentadas de modo a corroborar os estudos. Um dos exemplos de Rohrs é ainda abordado através de simulações, para os dois cenários adaptativos: o controlador backstepping adaptativo original e o VS-ABC

Controlador adaptativo backstepping a estrutura variavel com Observadores de estado

This research aims at developing a variable structure adaptive backstepping controller (VS-ABC) by using state observers for SISO (Single Input Single Output), linear and time invariant systems with relative degree one. Therefore, the lters were replaced by a Luenberger Adaptive Observer and the control algorithm uses switching laws. The presented simulations compare the controller performance, considering when the state variables are estimated by an observer, with the case that the variables are available for measurement. Even with numerous performance advantages, adaptive backstepping controllers still have very complex algorithms, especially when the system state variables are not measured, since the use of lters on the plant input and output is not something trivial. As an attempt to make the controller design more intuitive, an adaptive observer as an alternative to commonly used K lters can be used. Furthermore, since the states variables are considered known, the controller has a reduction on the dependence of the unknown plant parameters on the design. Also, switching laws could be used in the controller instead of the traditional integral adaptive laws because they improve the system transient performance and increase the robustness against external disturbances in the plant input

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

Excitações elementares em super-redes quasiperiódicas com simetria espelho

In this thesis, we investigated the magnonic and photonic structures that exhibit the so-called deterministic disorder. Speci cally, we studied the effects of the quasiperiodicity, associated with an internal structural symmetry, called mirror symmetry, on the spectra of photonics and magnonics multilayer. The quasiperiodicity is introduced when stacked layers following the so-called substitutional sequences. The three sequences used here were the Fibonacci sequence, Thue-Morse and double-period, all with mirror symmetry. Aiming to study the propagation of light waves in multilayer photonic, and spin waves propagation in multilayer magnonic, we use a theoretical model based on transfer matrix treatment. For the propagation of light waves, we present numerical results that show that the quasiperiodicity associated with a mirror symmetry greatly increases the intensity of transmission and the transmission spectra exhibit a pro le self-similar. The return map plotted for this system show that the presence of internal symmetry does not alter the pattern of Fibonacci maps when compared with the case without symmetry. But when comparing the maps of Thue-Morse and double-time sequences with their case without the symmetry mirror, is evident the change in the pro le of the maps. For magnetic multilayers, we work with two di erent systems, multilayer composed of a metamagnetic material and a non-magnetic material, and multilayers composed of two cubic Heisenberg ferromagnets. In the rst case, our calculations are carried out in the magnetostatic regime and calculate the dispersion relation of spin waves for the metamgnetic material considered FeBr2. We show the e ect of mirror symmetry in the spectra of spin waves, and made the analysis of the location of bulk bands and the scaling laws between the full width of the bands allowed and the number of layers of unit cell. Finally, we calculate the transmission spectra of spin waves in quasiperiodic multilayers consisting of Heisenberg ferromagnets. The transmission spectra exhibit self-similar patterns, with regions of scaling well-de ned in frequency and the return maps indicates only dependence of the particular sequence used in the construction of the multilayer

Estimativa de expoentes críticos em Percolação

In Percolation Theory, functions like the probability that a given site belongs to the infinite cluster, average size of clusters, etc. are described through power laws and critical exponents. This dissertation uses a method called Finite Size Scaling to provide a estimative of those exponents. The dissertation is divided in four parts. The first one briefly presents the main results for Site Percolation Theory for d = 2 dimension. Besides, some important quantities for the determination of the critical exponents and for the phase transistions understanding are defined. The second shows an introduction to the fractal concept, dimension and classification. Concluded the base of our study, in the third part the Scale Theory is mentioned, wich relates critical exponents and the quantities described in Chapter 2. In the last part, through the Finite Size Scaling method, we determine the critical exponents fi and. Based on them, we used the previous Chapter scale relations in order to determine the remaining critical exponents

On Fuzzy Implication Classes - Towards Extensions of Fuzzy Rule-Based Systems

Atualmente, há diferentes definições de implicações fuzzy aceitas na literatura. Do ponto de vista teórico, esta falta de consenso demonstra que há discordâncias sobre o real significado de "implicação lógica" nos contextos Booleano e fuzzy. Do ponto de vista prático, isso gera dúvidas a respeito de quais "operadores de implicação" os engenheiros de software devem considerar para implementar um Sistema Baseado em Regras Fuzzy (SBRF). Uma escolha ruim destes operadores pode implicar em SBRF's com menor acurácia e menos apropriados aos seus domínios de aplicação. Uma forma de contornar esta situação e conhecer melhor os conectivos lógicos fuzzy. Para isso se faz necessário saber quais propriedades tais conectivos podem satisfazer. Portanto, a m de corroborar com o significado de implicação fuzzy e corroborar com a implementação de SBRF's mais apropriados, várias leis Booleanas têm sido generalizadas e estudadas como equações ou inequações nas lógicas fuzzy. Tais generalizações são chamadas de leis Boolean-like e elas não são comumente válidas em qualquer semântica fuzzy. Neste cenário, esta dissertação apresenta uma investigação sobre as condições suficientes e necessárias nas quais três leis Booleanlike like — y ≤ I(x, y), I(x, I(y, x)) = 1 e I(x, I(y, z)) = I(I(x, y), I(x, z)) — se mantém válidas no contexto fuzzy, considerando seis classes de implicações fuzzy e implicações geradas por automorfismos. Além disso, ainda no intuito de implementar SBRF's mais apropriados, propomos uma extensão para os mesmos

Iinterpretação conjunta de dados de GPR e medidas de permeabilidade sobre um análogo de reservatório siliciclástico falhado na bacia de Tucano, no NE do Brasil

It is presented an integrated geophysical investigation of the spatial distribution of faults and deformation bands (DB´s) in a faulted siliciclastic reservoir analogue, located in Tucano Basin, Bahia State, northeastern Brazil. Ground Penetrating Radar (GPR) and permeability measurements allowed the analysis of the influence of DB´s in the rock permeability and porosity. GPR data were processed using a suitable flow parametrization in order to highlight discontinuities in sedimentary layers. The obtained images allowed the subsurface detection of DB´s presenting displacements greater that 10 cm. A good correlation was verified between DB´s detected by GPR and those observed in surface, the latter identified using conventional structural methods. After some adaptations in the minipermeameter in order to increase measurement precision, two approaches to measure permeabilities were tested: in situ and in collected cores. The former approach provided better results than the latter and consisted of scratching the outcrop surface, followed by direct measurements on outcrop rocks. The measured permeability profiles allowed to characterize the spatial transition from DB´s to undeformed rock; variation of up to three orders of magnitude were detected. The permeability profiles also presented quasi-periodic patterns, associated with textural and granulometric changes, possibly associated to depositional cycles. Integrated interpretation of the geological, geophysical and core data, provided the subsurface identification of an increase in the DB´s number associated with a sedimentary layer presenting granulometric decrease at depths greater than 8 m. An associated sharp decrease in permeability was also measured in cores from boreholes. The obtained results reveal that radagrams, besides providing high resolution images, allowing the detection of small structures (> 10 cm), also presented a correlation with the permeability data. In this way, GPR data may be used to build upscaling laws, bridging the gap between outcrop and seismic data sets, which may result in better models for faulted reservoirs

Faixas de proteção ambiental do Rio Pitimbu/RN: uma análise como subsídio ao planejamento e ordenamento do território

The Environmental Protection area sof Pitimbu river are important tools for planning and territorial land management. The Pitimbu river protection is aided in laws, so much of Federal stamp, as the Brazilian s Forest Code (Law No. 4771/1965), and in State s and City s Resolutions. So, this research begins in the State s Law No. 8426/2003interpretations, for being the most restrictive in the river's margin occupation and management. The objective is to analyze the applicability of the Environmental Protection areas of Pitimbu river, localized at the State of Rio Grande do Norte, considering environmental legislation and how to use this space by the man. Having specific goals for the discussion of the legislation s scope to this river; the identification of the types of soil s covering and evaluation the effectiveness of Law Nº.8426/2003, as protection instrument and land management. The river is characterized by its ecological importance and for feeding the Jiqui pond, an important reservoir that supplies 30% of drinking water to the east, west and south population sof the capital of the State. Pitimbu river is passing by a process of environmental degradation, originating from actions as deforestations of its ciliary forests by intensive agricultural practices; introduction of urban and industrial effluents leading to its contamination; increase of the pluvial drainage; erosion, sedimentation and discharge of urban waste , along with pressure for urban settlements along its banks. Under the methodological point of view is part of theoretical planning and land management research, and from a vision of social and environmental spaces. It was produced a survey map of the soil s covering, with 16 classes. Divided into coverage and disturbed natural covering. Using the 300 meters spatial limits of the Environmental Protection Strip, according to the State Law. The survey highlighted a higher percentage of classes disturbed, indicating man s interference in the balance of that system, as well as the lack of environmental actions. Leading to the degradation of riparian areas, and lack of conservation of water resources. Finally, it was considered that the strips of environmental protection are not effective as the preservation and territorial ordination