Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

Uma abordagem dirigida por modelos para desenvolvimento de middlewares auto-adaptativos para transmissão de fluxo de dados baseado em restrições de QoS

The use of middleware technology in various types of systems, in order to abstract low-level details related to the distribution of application logic, is increasingly common. Among several systems that can be benefited from using these components, we highlight the distributed systems, where it is necessary to allow communications between software components located on different physical machines. An important issue related to the communication between distributed components is the provision of mechanisms for managing the quality of service. This work presents a metamodel for modeling middlewares based on components in order to provide to an application the abstraction of a communication between components involved in a data stream, regardless their location. Another feature of the metamodel is the possibility of self-adaptation related to the communication mechanism, either by updating the values of its configuration parameters, or by its replacement by another mechanism, in case of the restrictions of quality of service specified are not being guaranteed. In this respect, it is planned the monitoring of the communication state (application of techniques like feedback control loop), analyzing performance metrics related. The paradigm of Model Driven Development was used to generate the implementation of a middleware that will serve as proof of concept of the metamodel, and the configuration and reconfiguration policies related to the dynamic adaptation processes. In this sense was defined the metamodel associated to the process of a communication configuration. The MDD application also corresponds to the definition of the following transformations: the architectural model of the middleware in Java code, and the configuration model to XML

MoSAC: um módulo para seleção de configurações arquiteturais baseado em critérios de QoS no contexto de sistema distribuídos autoadaptativos

The process for choosing the best components to build systems has become increasingly complex. It becomes more critical if it was need to consider many combinations of components in the context of an architectural configuration. These circumstances occur, mainly, when we have to deal with systems involving critical requirements, such as the timing constraints in distributed multimedia systems, the network bandwidth in mobile applications or even the reliability in real-time systems. This work proposes a process of dynamic selection of architectural configurations based on non-functional requirements criteria of the system, which can be used during a dynamic adaptation. This proposal uses the MAUT theory (Multi-Attribute Utility Theory) for decision making from a finite set of possibilities, which involve multiple criteria to be analyzed. Additionally, it was proposed a metamodel which can be used to describe the application s requirements in terms of the non-functional requirements criteria and their expected values, to express them in order to make the selection of the desired configuration. As a proof of concept, it was implemented a module that performs the dynamic choice of configurations, the MoSAC. This module was implemented using a component-based development approach (CBD), performing a selection of architectural configurations based on the proposed selection process involving multiple criteria. This work also presents a case study where an application was developed in the context of Digital TV to evaluate the time spent on the module to return a valid configuration to be used in a middleware with autoadaptative features, the middleware AdaptTV

Contribuição da teoria do caos para a gestão do turismo: uma análise a partir da percepção dos gestores da hotelaria de Natal/RN

O presente estudo tem como objetivo analisar como os gestores da hotelaria percebem a relação da teoria do caos e turismo, descrever como é pensada e concebida a gestão do turismo; mostrar as características caopléxicas do turismo e sua gestão e identificar os elementos do padrão estratégico de gestão e planejamento na visão dos gestores dos Meios de Hospedagem. Os dados foram obtidos através da observação direta intensiva e aplicação de entrevistas aplicadas junto aos hoteleiros da cidade de Natal/RN. Constata que as teorias da mudança e do caos proporcionam visão do conjunto de relações, aspectos e implicações do turismo, com base nas incertezas e instabilidades ambientais e de mercado. Mostra que a maioria dos modelos de análise, planejamento e gestão do turismo ainda é limitada, em razão do seu caráter linear e unidimensional. Destaca que o objetivo da teoria do caos é fornecer explicações dos fenômenos, não é fazer previsões, pois é impossível prever o futuro a longo prazo. Trata das estratégias de gestão como geradoras de novas fontes de incerteza, pois a realidade não pode ser completamente representada por modelos. Ter consciência desses fatos significa, entretanto, considerar o campo de múltiplas possibilidades e oportunidades da mudança e do caos na gestão do desenvolvimento do turismo. Essas idéias foram aplicadas à análise da gestão do turismo na localidade investigada. Os questionamentos levantados no estudo pautaram-se em pesquisa bibliográfica, fundamentada, principalmente, em autores como Beni, Prahalad, Mintzberg, Ritto, Senge e Hamel. Conclui-se que na era do conhecimento, as organizações que continuam presas ao paradigma mecanicista têm dificuldade de acompanhar as mudanças do mercado e sendo a hotelaria uma indústria de serviços que tem características organizacionais complexas e adaptativas, é imprescindível que os empreendimentos hoteleiros funcionem como sistemas interativos, que acompanhem as mudanças de um mercado tão turbulento e instável tendo na teoria do caos e da complexidade uma das possibilidades de compreender a realidade fora do modelo mecanicista.

O planejamento turístico e o comércio ambulante : uma análise à luz da teoria das representações sociais

The Social Representation Theory provides subsidies to scientifically analyze what is called common sense, suggesting that thought be given credibility to the individual, from the assignment of logic to it. The Representations allow us to interpret, understand, explain and thus classify information, events and people. In this sense, this study aimed to analyze how social representations of the actors of the intinerant traders who operate in Ponta Negra/RN can be used as an element for tourism planning. To achieve the desired goals, we conducted a qualitative study, from a descriptive study, using methods of data collection the research literature, the technique of free association of words and the questionnaire, applied with 90 intinerant traders who work in Ponta Negra/RN beach. As tools of data analysis were used to analyze literature, and software EVOC and SPHINX. This research has revealed the predominance of people in itinerant male, between 18 and 28 years, with incomplete primary education, no contributors of Previdência Social and working seven days a week. The core elements of representations brings that explain that their knowledge is guided by collectively shared knowledge in the culture of tourism, which is seen as something that brings economics benefits (money) to the society, from the travel and entertainment. The plan represents the forward thinking, based on development plans that seek improvements and organization. The structure and operation of tourism planning in Natal/RN, there were no representation of intinerant traders. It is concluded that understanding the needs of itinerant traders provides grants to developing strategies for the development of tourism. This is achieved from its inclusion in tourism planning, since it enables tourism managers to understand how they are capturing, interpreting and acting on their next reality, since these representations are fundamental in forming opinions and the establishment of individual attitudes and collective. Thus, it is an important theory to be used to subsidize social research with individuals living reality and local needs, but which is the margin of decision-making processes of economic in the Brazil

A teoria da ruína aplicada em um modelo de empresa financeira com risco de crédito

In this work we study a new risk model for a firm which is sensitive to its credit quality, proposed by Yang(2003): Are obtained recursive equations for finite time ruin probability and distribution of ruin time and Volterra type integral equation systems for ultimate ruin probability, severity of ruin and distribution of surplus before and after ruin

Teoria da Ruína em um Modelo de Markov com dois Estados

In this work, we present a risk theory application in the following scenario: In each period of time we have a change in the capital of the ensurance company and the outcome of a two-state Markov chain stabilishs if the company pays a benece it heat to one of its policyholders or it receives a Hightimes c > 0 paid by someone buying a new policy. At the end we will determine once again by the recursive equation for expectation the time ruin for this company

Função Afifim: Teoria e aplicações

In this work we present a proposal to contribute to the teaching and learning of affine function in the first year of high school having as prerequisite mathematical knowledge of basic education. The proposal focuses on some properties, special cases and applications of affine functions in order to show the importance of the demonstrations while awaken student interest by showing how this function is important to solve everyday problems

What is a Fuzzy Bi-implication?

In order to make this document self-contained, we first present all the necessary theory as a background. Then we study several definitions that extended the classic bi-implication in to the domain of well stablished fuzzy logics, namely, into the [0; 1] interval. Those approaches of the fuzzy bi-implication can be summarized as follows: two axiomatized definitions, which we proved that represent the same class of functions, four defining standard (two of them proposed by us), which varied by the number of different compound operators and what restrictions they had to satisfy. We proved that those defining standard represent only two classes of functions, having one as a proper subclass of the other, yet being both a subclass of the class represented by the axiomatized definitions. Since those three clases satisfy some contraints that we judge unnecessary, we proposed a new defining standard free of those restrictions and that represents a class of functions that intersects with the class represented by the axiomatized definitions. By this dissertation we are aiming to settle the groundwork for future research on this operator.

Comportamento locomotor de crianças e adultos jovens em ambiente doméstico simulado

Observamos o comportamento locomotor de 40 crianças (de 5 a 8 anos) e de 40 adultos jovens (de 19 a 28 anos) frente a restrições ambientais, que percorreram dois circuitos em condições de luminosidade total e reduzida e transporte de carga (sem carga, 3% e 7% da massa corporal), andando o mais rápido possível e evitando contato com objetos. O tempo gasto na tarefa foi obtido por meio de um cronômetro digital, em três tentativas por condição. ANOVA para três fatores (circuito x iluminação x carga) revelou que: as crianças demoraram mais tempo para realizar a tarefa quando carga foi adicionada; crianças mais jovens percorreram o circuito em tempo maior que crianças mais velhas; as condições não alteraram a locomoção dos adultos. Concluímos que crianças necessitam integrar as informações sensoriais e acoplá-las ao sistema efetor. Programas de intervenção são necessários para facilitar essa integração sem restrição da mobilidade das crianças.

Teoria da Formação e Avaliação no currículo de Educação Física

Having as reference the curricular proposals that composed the new directives for Formation of Professors for the Basic Education, Full Licence in Brazil, it was aimed to analyze in the pedagogic project of a Physical Education Licence course, the professional profile proposed, the conceptual orientation adopted (curriculum model) as well the evaluation proposed in the curriculum. These results obtained from the descriptive study have contemplated documental source and content analysis approach, utilizing as basis for discussion of the results the formation theory. Among the most significant data it was established that, the presented professor profile must consider an Academic, Technological, Practical and Socio-Reconstructionist orientation, detaching during the evaluation process a high skill level in Academic Orientation, as well remarking that the evaluation is presented as a great gap in the pedagogic project.

Contexto esportivo e as restrições comportamentais: reflexões a luz da psicologia bioecológica

To deal with restrictions takes in them to a boarding that has been studied as perspective theoretician to understand as the practitioners acquire standards of coordination in the chosen sports (ARAUJO, 2005). It is basic for the training that if has a knowledge concerning the restrictions more significant than they act on the human performance of the athletes, because this will make possible one adequate recital in the work proposal of the team staff. The question of the theory application, in the world of the sport, is a tool has very desired and pursued, however, nor always if they apply the theoretical knowledge in experimental research that promotes enough and important alterations, that can favor the real additions to Sport Sciences. This study it is an attempt to collaborate in this intention, in way to locate and to modify beginning usual routines between experts and of the sports, in special to the considered situation sports, as the Volleyball (IVOILOV, 2001). This objective is not fixed only in the relative questions to the teach-learning processes, nor so little to the sportive training, but it advances, also, for the instructions given for the coaches to commanded its, at moments any of the sportive trajectory of these; it innovates when searching to exemplify, directly, in a modality of international domain but with few systematic analyses on the human performances in question.

Desempenho motor no esporte: das restrições do iniciante ao experiente

A set of constraints on the performance of motor skills is a determinant factor of success in many sport modalities that require from the athlete continuous adaptation to changes in the game context. Taking into account Newell's model of organism (or performer), task and environmental constraints in the acquisition of motor skills (NEWELL, 1986), the focus of this study is the set of changes that take place in motor behavior from the beginner to the high level athlete. In specific, the focus is toward changes in sports settings in which the ball is the center of the game, responsible for the relationship among athletes of the same team as well as between opponents, as in volleyball. The ball, in its trajectory, carries on a set of constraints to the player's behavior. To be able of imposing constraints on the opponent's behavior is so important as to know how to deal with a ball sent to you by the opponent in an unpredictable trajectory.

Teoria algébrica de processos da medida em sistemas quânticos

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

A sistemática incompreensão da teoria quântica e as dificuldades dos professores na introdução da Física Moderna e Contemporânea no Ensino Médio

O objetivo desta pesquisa é avaliar a proposta de introdução da Física Moderna e Contemporânea no Nível Médio da Educação Básica. Parte-se do pressuposto de que os professores assumem, às vezes até subconscientemente, que a teoria base da FMC é incompreensível. Investigamos, em 2007, os discursos de cinco professores de Física de um município da região Nordeste, visando compreender as possibilidades desses professores introduzirem a FMC em suas aulas de Física e em que medida estas possibilidades estão associadas às suas formações profissionais. Para a construção e análises dos discursos pautamo-nos na Análise de Discurso Francesa e em referenciais da Teoria Crítica da Educação. Constatamos que apesar de atribuírem papel relevante à introdução da FMC no Nível Médio, os professores não estão encarando este desafio.