Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

A utilização da pesquisa operacional para o gerenciamento dos leitos em um hospital particular: estudo de caso baseado em simulação computacional

The hospital is a place of complex actions, where several activities for serving the population are performed such as: medical appointments, exams, surgeries, emergency care, admission in wards and ICUs. These activities are mixed with anxiety, impatience, despair and distress of patients and their families, issues involving emotional balance both for professionals who provide services for them as for people cared by them. The healthcare crisis in Brazil is getting worse every year and today, constitutes a major problem for private hospitals. The patient that comes to emergencies progressively increase, and in contrast, there is no supply of hospital beds in the same proportion, causing overcrowding, declines in the quality of care delivered to patients, drain of professionals of the health area and difficulty in management the beds. This work presents a study that seeks to create an alternative tool that can contribute to the management of a private hospital beds. It also seeks to identify potential issues or deficiencies and therefore make changes in flow for an increase in service capacity, thus reducing costs without compromising the quality of services provided. The tool used was the Computational Simulation –based in discrete event, which aims to identify the main parameters to be considered for a proper modeling of this system. This study took as reference the admission of a private hospital, based on the current scenario, where your apartments are in saturation level as its occupancy rate. The relocation of project beds aims to meet the growing demand for surgeries and hospital admissions observed by the current administration.

CES: Um Mecanismo Genérico de Composição de Eventos para Sistemas Sensíveis ao Contexto

Pervasive applications use context provision middleware support as infrastructures to provide context information. Typically, those applications use communication publish/subscribe to eliminate the direct coupling between components and to allow the selective information dissemination based in the interests of the communicating elements. The use of composite events mechanisms together with such middlewares to aggregate individual low level events, originating from of heterogeneous sources, in high level context information relevant for the application. CES (Composite Event System) is a composite events mechanism that works simultaneously in cooperation with several context provision middlewares. With that integration, applications use CES to subscribe to composite events and CES, in turn, subscribes to the primitive events in the appropriate underlying middlewares and notifies the applications when the composed events happen. Furthermore, CES offers a language with a group of operators for the definition of composite events that also allows context information sharing

Estudo estatístico sobre eventos de precipitação intensa no nordeste do Brasil

The Northeast of Brazil (NEB) shows high climate variability, ranging from semiarid regions to a rainy regions. According to the latest report of the Intergovernmental Panel on Climate Change, the NEB is highly susceptible to climate change, and also heavy rainfall events (HRE). However, few climatology studies about these episodes were performed, thus the objective main research is to compute the climatology and trend of the episodes number and the daily rainfall rate associated with HRE in the NEB and its climatologically homogeneous sub regions; relate them to the weak rainfall events and normal rainfall events. The daily rainfall data of the hydrometeorological network managed by the Agência Nacional de Águas, from 1972 to 2002. For selection of rainfall events used the technique of quantiles and the trend was identified using the Mann-Kendall test. The sub regions were obtained by cluster analysis, using as similarity measure the Euclidean distance and Ward agglomerative hierarchical method. The results show that the seasonality of the NEB is being intensified, i.e., the dry season is becoming drier and wet season getting wet. The El Niño and La Niña influence more on the amount of events regarding the intensity, but the sub-regions this influence is less noticeable. Using daily data reanalysis ERAInterim fields of anomalies of the composites of meteorological variables were calculated for the coast of the NEB, to characterize the synoptic environment. The Upper-level cyclonic vortex and the South atlantic convergene zone were identified as the main weather systems responsible for training of EPI on the coastland

Uma fundamentação para sinais e sistemas intervalares

In this work we use Interval Mathematics to establish interval counterparts for the main tools used in digital signal processing. More specifically, the approach developed here is oriented to signals, systems, sampling, quantization, coding and Fourier transforms. A detailed study for some interval arithmetics which handle with complex numbers is provided; they are: complex interval arithmetic (or rectangular), circular complex arithmetic, and interval arithmetic for polar sectors. This lead us to investigate some properties that are relevant for the development of a theory of interval digital signal processing. It is shown that the sets IR and R(C) endowed with any correct arithmetic is not an algebraic field, meaning that those sets do not behave like real and complex numbers. An alternative to the notion of interval complex width is also provided and the Kulisch- Miranker order is used in order to write complex numbers in the interval form enabling operations on endpoints. The use of interval signals and systems is possible thanks to the representation of complex values into floating point systems. That is, if a number x 2 R is not representable in a floating point system F then it is mapped to an interval [x;x], such that x is the largest number in F which is smaller than x and x is the smallest one in F which is greater than x. This interval representation is the starting point for definitions like interval signals and systems which take real or complex values. It provides the extension for notions like: causality, stability, time invariance, homogeneity, additivity and linearity to interval systems. The process of quantization is extended to its interval counterpart. Thereafter the interval versions for: quantization levels, quantization error and encoded signal are provided. It is shown that the interval levels of quantization represent complex quantization levels and the classical quantization error ranges over the interval quantization error. An estimation for the interval quantization error and an interval version for Z-transform (and hence Fourier transform) is provided. Finally, the results of an Matlab implementation is given

Modelagem estatística e atribuições dos eventos de precipitação extrema na Amazônia brasileira

Intense precipitation events (IPE) have been causing great social and economic losses in the affected regions. In the Amazon, these events can have serious impacts, primarily for populations living on the margins of its countless rivers, because when water levels are elevated, floods and/or inundations are generally observed. Thus, the main objective of this research is to study IPE, through Extreme Value Theory (EVT), to estimate return periods of these events and identify regions of the Brazilian Amazon where IPE have the largest values. The study was performed using daily rainfall data of the hydrometeorological network managed by the National Water Agency (Agência Nacional de Água) and the Meteorological Data Bank for Education and Research (Banco de Dados Meteorológicos para Ensino e Pesquisa) of the National Institute of Meteorology (Instituto Nacional de Meteorologia), covering the period 1983-2012. First, homogeneous rainfall regions were determined through cluster analysis, using the hierarchical agglomerative Ward method. Then synthetic series to represent the homogeneous regions were created. Next EVT, was applied in these series, through Generalized Extreme Value (GEV) and the Generalized Pareto Distribution (GPD). The goodness of fit of these distributions were evaluated by the application of the Kolmogorov-Smirnov test, which compares the cumulated empirical distributions with the theoretical ones. Finally, the composition technique was used to characterize the prevailing atmospheric patterns for the occurrence of IPE. The results suggest that the Brazilian Amazon has six pluvial homogeneous regions. It is expected more severe IPE to occur in the south and in the Amazon coast. More intense rainfall events are expected during the rainy or transitions seasons of each sub-region, with total daily precipitation of 146.1, 143.1 and 109.4 mm (GEV) and 201.6, 209.5 and 152.4 mm (GPD), at least once year, in the south, in the coast and in the northwest of the Brazilian Amazon, respectively. For the south Amazonia, the composition analysis revealed that IPE are associated with the configuration and formation of the South Atlantic Convergence Zone. Along the coast, intense precipitation events are associated with mesoscale systems, such Squall Lines. In Northwest Amazonia IPE are apparently associated with the Intertropical Convergence Zone and/or local convection.