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

Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs

Análise da evolução costeira do litoral setentrional do estado do rio grande do norte, região sob influência da indústria petrolífera

The northern coast of Rio Grande do Norte State is characterized by strong changes in coastal morphology, caused by various geological and climatic factors. In this region are installed the main socio-economic activities of the State, highlighting the oil industry, which exerts much of its activities in the coastal area studied. Erosion is a constant problem in this region because it affects the entire local populace to the destruction of houses and trade, rendering tourism, affecting the livelihood activities and industrial activities. The greatest risk is related to environmental damage that can be caused by the oil spill in this region. To understand what determines the changes in coastal morphology this Doctoral Thesis is proposed to identify the factors at local, regional and even global corroborate coastal dynamics to this coast in question. For this study, used several different products and tools for interpreting the conditions of the erosive effect that dominates the whole northern coast of the State, in an attempt to quantify and describe the causes and effects that affect the entire coastal zone monitored. The development of activities is built into the projects Rede 05 PETROMAR (CTPETRO-FINEP/PETROBRAS/CNPq), PETRORISCO, HIDROSEMA, PETROMAR e Rede 05/04 POTMAR (FNDCT/CTPETROFINEP/ CNPq), in the activities of multidisciplinary and inter-features in issues involving environmental monitoring and oil activity

Avaliação de impacto ambiental e gestão dos recursos natuarias no estuário Apodi Mossoró, nordeste do Brasil

The aim of this study is to investigate the eco-environmental vulnerability, its changes, and its causes to develop a management system for application of eco-environmental vulnerability and risk assessment in the Apodi-Mossory estuary, Northeast Brazil. This analysis is focused on the interference of the landscape conditions, and its changes, due to the following factors: the oil and natural gas industry, tropical fruits industry, shrimp farms, marine salt industry, occupation of the sensitive areas; demand for land, vegetation degradation, siltation in rivers, severe flooding, sea level rise (SLR), coastal dynamics, low and flat topography, high ecological value and tourism in the region and the rapid growth of urbanization. Conventional and remote sensing data were analyzed using modeling techniques based on ArcGIS, ER-Mapper, ERDAS Imagine and ENVI software. Digital images were initially processed by Principal Component Analysis and transformation of the maximum fraction of noise, and then all bands were normalized to reduce errors caused by bands of different sizes. They were integrated in a Geographic Information System analysis to detect changes, to generate digital elevation models, geomorphic indices and other variables of the study area. A three band color combination of multispectral bands was used to monitor changes of land and vegetation cover from 1986 to 2009. This task also included the analysis of various secondary data, such as field data, socioeconomic data, environmental data and prospects growth. The main objective of this study was to improve our understanding of eco-environmental vulnerability and risk assessment; it´s causes basically show the intensity, its distribution and human-environment effect on the ecosystem, and identify the high and low sensitive areas and area of inundation due to future SLR, and the loss of land due to coastal erosion in the Apodi-Mossoró estuary in order to establish a strategy for sustainable land use. The developed model includes some basic factors such as geology, geomorphology, soils, land use / land cover, vegetation cover, slope, topography and hydrology. The numerical results indicate that 9.86% of total study area was under very high vulnerability, 29.12% high vulnerability, 52.90% moderate vulnerability and 2.23% were in the category of very low vulnerability. The analysis indicates that 216.1 km² and 362.8 km² area flooded on 1m and 10m in sea levels respectively. The sectors most affected were residential, industrial and recreational areas, agricultural land, and ecosystems of high environmental sensitivity. The results showed that changes in eco-environmental vulnerability have a significant impact on the sustainable development of the RN state, since the indicator is a function of sensitivity, exposure and status in relation to a level of damage. The model were presented as a tool to assist in indexing vulnerability in order to optimize actions and assess the implications of decisions makers and policies regarding the management of coastal and estuarine areas. In this context aspects such as population growth, degradation of vegetation, land use / land cover, amount and type of industrialization, SLR and government policies for environmental protection were considered the main factors that affect the eco-environmental changes over the last three decades in the Apodi-Mossoró estuary.

Monitoramento ambiental da costa do Rio Grande do Norte com base em sensoriamento remoto e geodésia de precisão

This paper presents models of parameters of Sea Surface Layer (SSL), such as chlorophyll-a, sea surface temperature (SST), Primary Productivity (PP) and Total Suspended Matter (TSM) for the region adjacent to the continental shelf of Rio Grande do Norte (RN), Brazil. Concentrations of these parameters measured in situ were compared in time quasi-synchronous with images AQUA-MODIS between the years 2003 to 2011. Determination coefficients between samples in situ and bands reflectance sensor AQUA-MODIS were representative. From that, concentrations of SSL parameters were acquired for the continental shelf of the RN (eastern and northern) analyzing the geographic distribution of variation of these parameters between the years 2009-2012. Geographical and seasonal variations mainly influenced by global climate phenomena such as El Niño and La Niña, were found through the analysis of AQUA-MODIS images by Principal Components Analysis (PCA). Images show qualitatively the variance and availability of TSM in the regions, as well as their relationship with coastal erosion hotspots, monitored along the coast of the RN. In one of the areas identified as being of limited availability of TSM, we developed a methodology for assessment and evaluation of Digital Elevation Models (DEM) of beach surfaces (emerged and submerged sections) from the integration of topographic and bathymetric data measured in situ and accurately georeferenced compatible to studies of geomorphology and coastal dynamics of short duration. The methodology consisted of surveys with GNSS positioning operated in cinematic relative mode involved in topographic and bathymetric executed in relation to the stations of the geodetic network of the study area, which provided geodetic link to the Brazilian Geodetic System (GBS), univocal , fixed, and relatively stable over time. In this study Ponta Negra Beach, Natal / RN, was identified as a region with low variance and availability of MPS in the region off, as characterized by intense human occupation and intense coastal erosion in recent decades, which presents potential of the proposed methodology for accuracy and productivity, and the progress achieved in relation to the classical methods of surveying beach profiles