Beta: uma ferramenta para geração de testes de unidade a partir de especificações B

Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies

Lazer e urbanização: a dinâmica do setor de serviços no litoral de Parnamirim e Nísia Floresta - RN

The research here undertaken analyzes the process of urbanization on the coast of Panamirim - RN and Nísia Floresta - RN, arising from leisure, the main leisure expression was considered the second residence and coastal tourism. The leisure promoted the growth of businesses and public and private services to meet consumer demand in that area, which initially occurred with users of second home, and which also gradually begin to occupy the coastline of these municipalities in 1980 and more recently with the development of tourism in the 1990s until now. To undertake such an analysis, we did the georeferencing about the trade and also public and private services of that coast, characterizing them; evaluated the extent to which services deployed in this area meets the demands of tourists and users of second residence; it was also identified how the centrality of Natal interferes in the expansion of services in these locations. The spatial area of research includes the coastal municipalities of Parnamirim and Nísia Floresta, considering the limits of the census of the Instituto Brasileiro de Geografia e Estatística- IBGE, and about the time frame, it was considered the 1990s to the present day. The methodology consists of: 1. survey and reading of the literature related to the researched topic, serving as the theoretical analysis in the construction of the object studied; 2. collection and organization of secondary data by the IBGE and tourism sectors of the State of Rio Grande do Norte, Natal and main municipalities of the research; 3. Questionnaires and / or interviews with the traders, service providers, tourists, users of second homes, local residents, and government. The analysis of such data collected allowed the preparation of graphs, maps and tables that illustrate the results obtained in the research field, basing so the study. The relevance of the study is shown by the extensive survey data involving agents of the research, including tourists, users of second homes and, above all, the data for the service sector that did not exist in the analyzed area. The study results identified in the area analyzed the emergence of three new centers, arising from the urbanization process from leisure, one of them located in the municipality of Nísia Foresta Beach in Barra de Tabatinga, and two in Parnamirim, more specifically in locality Pium and Beach Pirangi do Norte. It was further observed that, being located in tourist areas, the main feature of these new centers is seasonality

Caminhos de sobrevivência institucional: a gestão do núcleo de oficinas e artes profissionalizantes laís aderne

The object of this study is the organizational management, particularly the relational processenvironment organization focused on the survival of the space Department of the Arts and Crafts Mestre Raimundo Cardoso linked to the structural arrangement of the Liceu do Paracuri.. Aimed to understand the ways of organizational survival, from the actors' perception of the Center for Arts Career Workshops and Lais Aderne, with investments that discuss the theoretical models of management, institutional theory, cultural organization and institutionalization of public education requirement of the municipal light LDB. (1996) used a qualitative approach with a view to RICHARDSON (1985). The data generated were analyzed based on the technique of content analysis, the thematic type [categorical] Bardin (1977). The results indicate that the institutionalization of the arrangement of the Liceu do Paracuri emerges meet the legal requirement of the autonomy of municipal educational administration under the aegis of sustainable development, quality of life and basic education from the municipal Hélio Gueiros (1993-1996 ). More specifically the Center for Arts and Crafts Laís Aderne, the unit of analysis, the subjects said that this space is designed as a link between the demands of school and community searching through interdisciplinary activities educate and train manpower mainly potter. They did mention the existence of institutional factors (history, culture, habits, values) represent a strong socio-cultural element to the actors belonging to the core that guides behavior and actions of these individuals, fueled by a sense of hope, inclusion of future artisans in culture ceramist. It made a shared management, the existence of a unique work through cultural revival. However, over the course of time, the core is faced with dilemmas of managing transitions mainly regarding governmental, technological beyond endurance by the craftsmen for the optimization of their work. The conclusion - that the paths chosen for the organizational survival of the core meaning and guiding their actions in the systematization of conduct, representations, memories and traditions through habits and choices of consensus, the viewpoint of the actors

Itinerário educacional de uma aluna cega e a busca pela imagem adaptada

The scope of this study directs an investigation in search of how the blind person learns knowledge at school mediated by the image in context of an inclusive education and how it can be (or is) triggered by the adaptation of images to the tactile seizure of the blind person and his correlative process of reading. To achieve this intent we choose a qualitative approach of research and opted for the modality of case study, based on the empirical field of a public school in the city of Cruzeta, RN and as a the main subject a congenitally blind female student enrolled in high school there, focusing, often, on the discipline of geography in its words mapping. Our procedures for construction of data are directly involved to the documentary analysis of open reflective interview and observation. The base guiding theory of our assessments is located in the current understanding about the human psychological development of its educational process inside an inclusive perspective, of contemporary conceptions about the visual disability as well of image as a cultural product. Accordingly, the human person is a concrete subject, whose development is deeply marked by the culture, historically built by human society. This subject regardless of his specific features, grasping the world in an interactive and immediate way, internalising and producing culture. In this thinking, we believe that the blind person perceives in multiple senses the stimuli of his environment and acts in the world toward his integration into the social environment. The image as a product of culture, historically and socially determined, appears as a sign conventionally used as an icon that in itself concentrates knowledge of which the student who does not realize visually himself and his surroundings cannot be excluded. In this direction, the inclusive educational process must build conditions of access to knowledge for all students without distinction, including access to the interpretation of the images originally intended for the seizure strictly visual to other perceptive models. Based in this theory and adopting principles of content analysis, we circulated inside the interpretation of the data constructed from the analysis of documents, from the subject speeches, from records of the observation made in the classroom and other notes of the field daily. In the search for pictures on the school contents, adapted to the tactile seizure of blind student, was seen little and not systematic in practice and teaching at the school. It showed us the itinerary of the student life marked by a succession of supports, most of the time inappropriate and pioneers in cooling the construction of her autonomy. It also showed us the tensions and contradictions of a school environment, supposedly inclusive, that stumbles in search of its intent, in the attitudinal and cumulative barriers brought, because of its aggravating maintenance. These findings arose of crossing data around of a categorization that gives importance to 1) Concepts regarding the school inclusion, 2) Elements of the school organization, educational proposal and teaching practice, 3) Meaning of the visual image as the object of knowledge, 4) Perception in multiple senses and 5) Development and learning of the blind person before impositions of the social environment. In light of these findings we infer that it must be guaranteed to the disabled person removal of the attitudinal barriers that are against his full development and the construction of his autonomy. In that sense, should be given opportunity to the student with visual disability, similarly to all students, not only access to school, but also the dynamics of a school life efficient, that means the seizure of knowledge in all its modalities, including the imagery. To that end, there is a need of the continued training of teachers, construction of a support network in response to all needs of students, and the opportunity to development of reading skills beyond a perspective eminently focused in the sight

Estilos de aprendizagem sob a ótica da Psicologia Evolucionista

Among a variety of learning conceptions, David Kolb´s Experiential Learning Theory proposes four different learning styles: diverging, characterized by orientation towards people and multi-perspective vision; assimilating, concerned with ideas and abstract concepts as well as theory formulation; converging, expert in dealing with technical tasks and problem solving; and accommodating, risk taker and good at getting things done. Interesting correlations have been pointed out between Kolb s learning styles, professional careers and genders. With respect to behaviors, specific cognitive skills and interests, sex differences are widely known, and explained by Evolutionary Psychology as the result of distinct selective pressures acting on each gender. The aim of this research was to assess adolescents learning styles and their relation with interests on school and career choices, analyzing possible gender differences. We distributed questionnaires to 221 senior high school students to research their preferences for school disciplines, professional activities and career choices. The Learning Style Inventory specified the learning style of each individual. Our results showed a high frequency of reflective styles, with predominance of females as diverging and males as assimilating. Concerning school and professional interests, there were correlations between styles oriented towards the abstract and technical interests. Moreover, females preferred disciplines related to languages and interpersonal activities while males preferred disciplines related to science and technical activities. There were more males in exact science and engineering careers, and more females in social science and applied social science. Correlations found between learning styles, school and professional interests corroborate Kolb´s propositions, and the findings about gender differences are supported by Evolutionary Psychology theories

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.

Caminhos de sobrevivência institucional: a gestão do Núcleo de Oficinas e Artes Profissionalizantes Laís Aderne

The object of this study is the organizational management, particularly the relational processenvironment organization focused on the survival of the space Department of the Arts and Crafts Mestre Raimundo Cardoso linked to the structural arrangement of the Liceu do Paracuri.. Aimed to understand the ways of organizational survival, from the actors' perception of the Center for Arts Career Workshops and Lais Aderne, with investments that discuss the theoretical models of management, institutional theory, cultural organization and institutionalization of public education requirement of the municipal light LDB. (1996) used a qualitative approach with a view to RICHARDSON (1985). The data generated were analyzed based on the technique of content analysis, the thematic type [categorical] Bardin (1977). The results indicate that the institutionalization of the arrangement of the Liceu do Paracuri emerges meet the legal requirement of the autonomy of municipal educational administration under the aegis of sustainable development, quality of life and basic education from the municipal Hélio Gueiros (1993-1996 ). More specifically the Center for Arts and Crafts Laís Aderne, the unit of analysis, the subjects said that this space is designed as a link between the demands of school and community searching through interdisciplinary activities educate and train manpower mainly potter. They did mention the existence of institutional factors (history, culture, habits, values) represent a strong socio-cultural element to the actors belonging to the core that guides behavior and actions of these individuals, fueled by a sense of hope, inclusion of future artisans in culture ceramist. It made a shared management, the existence of a unique work through cultural revival. However, over the course of time, the core is faced with dilemmas of managing transitions mainly regarding governmental, technological beyond endurance by the craftsmen for the optimization of their work. The conclusion - that the paths chosen for the organizational survival of the core meaning and guiding their actions in the systematization of conduct, representations, memories and traditions through habits and choices of consensus, the viewpoint of the actors

Análise fractal da vasculatura arteriolar e venular da retina em pessoas sem doença ocular

Although it has been suggested that retinal vasculature is a diffusion-limited aggregation (DLA) fractal, no study has been dedicated to standardizing its fractal analysis . The aims of this project was to standardize a method to estimate the fractal dimensions of retinal vasculature and to characterize their normal values; to determine if this estimation is dependent on skeletization and on segmentation and calculation methods; to assess the suitability of the DLA model and to determine the usefulness of log-log graphs in characterizing vasculature fractality . To achieve these aims, the information, mass-radius and box counting dimensions of 20 eyes vasculatures were compared when the vessels were manually or computationally segmented; the fractal dimensions of the vasculatures of 60 eyes of healthy volunteers were compared with those of 40 DLA models and the log-log graphs obtained were compared with those of known fractals and those of non-fractals. The main results were: the fractal dimensions of vascular trees were dependent on segmentation methods and dimension calculation methods, but there was no difference between manual segmentation and scale-space, multithreshold and wavelet computational methods; the means of the information and box dimensions for arteriolar trees were 1.29. against 1.34 and 1.35 for the venular trees; the dimension for the DLA models were higher than that for vessels; the log-log graphs were straight, but with varying local slopes, both for vascular trees and for fractals and non-fractals. This results leads to the following conclusions: the estimation of the fractal dimensions for retinal vasculature is dependent on its skeletization and on the segmentation and calculation methods; log-log graphs are not suitable as a fractality test; the means of the information and box counting dimensions for the normal eyes were 1.47 and 1.43, respectively, and the DLA model with optic disc seeding is not sufficient for retinal vascularization modeling

Balanced Scorecard como ferramenta de avaliação da consistência estratégica: um estudo em instituição de ensino superior privada

This Master of Science Thesis investigates in an exploratory modeling the idea of strategy consistency applying as an assessment tool a model of performance indicators of a higher education institution based on the balanced scorecard (BSC). It is carried on a review of conceptual BSC perspective hierarchy models and of studies on higher education institution in Brazil and worldwide. From a BSC model with three indicators at each perspective is carried on a case study with directors and coordinators of a private higher education institution with a descriptive and multivariate analysis using cluster analysis. The main findings point to a different perception of respondents on the importance level of the perspectives with a higher importance level given to Learning and Growth and Process that to Customer and Financial. Particularly, the financial perspective got a importance level significantly lower that the others, what suggests an inconsistency on the strategy deployment on the institution considered in terms of the perception of the managerial levels of the importance level of the perspectives