JFloat: uma biblioteca de ponto flutuante para a linguagem Java com suporte a arredondamento direcionado

This work presents JFLoat, a software implementation of IEEE-754 standard for binary floating point arithmetic. JFloat was built to provide some features not implemented in Java, specifically directed rounding support. That feature is important for Java-XSC, a project developed in this Department. Also, Java programs should have same portability when using floating point operations, mainly because IEEE-754 specifies that programs should have exactly same behavior on every configuration. However, it was noted that programs using Java native floating point types may be machine and operating system dependent. Also, JFloat is a possible solution to that problem

Geração automática de testes a partir de descrições de linguagens

Some programs may have their entry data specified by formalized context-free grammars. This formalization facilitates the use of tools in the systematization and the rise of the quality of their test process. This category of programs, compilers have been the first to use this kind of tool for the automation of their tests. In this work we present an approach for definition of tests from the formal description of the entries of the program. The generation of the sentences is performed by taking into account syntactic aspects defined by the specification of the entries, the grammar. For optimization, their coverage criteria are used to limit the quantity of tests without diminishing their quality. Our approach uses these criteria to drive generation to produce sentences that satisfy a specific coverage criterion. The approach presented is based on the use of Lua language, relying heavily on its resources of coroutines and dynamic construction of functions. With these resources, we propose a simple and compact implementation that can be optimized and controlled in different ways, in order to seek satisfaction the different implemented coverage criteria. To make the use of our tool simpler, the EBNF notation for the specification of the entries was adopted. Its parser was specified in the tool Meta-Environment for rapid prototyping

MyPersonal-EPG: um EPG personalizável e com suportes a recomendações para o SBTVD

In this work we present the architecture and implementation of MyPersonal-EPG, a personal EPG with support to recommendations, built on top of the Ginga middleware, that fulfill the following requirements: (i) to allow users to build their own personal programming grids, based on programming guides from several broadcasters; (ii) to offer a mechanism to tune the desired channels on the moment the selected programs are about to begin; (iii) to allow users to select the desired programs categories; (iv) to offer programs recommendations, in both synchronous and asynchronous way, based on the categories previously selected by users; (v) to allow users to modify the current configuration options; (vi) to allow the creation of several users accounts, so that each user can store its own information. The application‟s usability test is also presented and its results are discussed and analyzed

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

Java-XSC : módulo complexo e complexo intervalar

This work aims to develop modules that will increase the computational power of the Java-XSC library, and XSC an acronym for "Language Extensions for Scientific Computation . This library is actually an extension of the Java programming language that has standard functions and routines elementary mathematics useful interval. in this study two modules were added to the library, namely, the modulus of complex numbers and complex numbers of module interval which together with the modules original numerical applications that are designed to allow, for example in the engineering field, can be used in devices running Java programs

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

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

POPT: uma abordagem de ensino de programação orientada a problema e testes

There is a growing interest of the Computer Science education community for including testing concepts on introductory programming courses. Aiming at contributing to this issue, we introduce POPT, a Problem-Oriented Programming and Testing approach for Introductory Programming Courses. POPT main goal is to improve the traditional method of teaching introductory programming that concentrates mainly on implementation and neglects testing. POPT extends POP (Problem Oriented Programing) methodology proposed on the PhD Thesis of Andrea Mendonça (UFCG). In both methodologies POPT and POP, students skills in dealing with ill-defined problems must be developed since the first programming courses. In POPT however, students are stimulated to clarify ill-defined problem specifications, guided by de definition of test cases (in a table-like manner). This paper presents POPT, and TestBoot a tool developed to support the methodology. In order to evaluate the approach a case study and a controlled experiment (which adopted the Latin Square design) were performed. In an Introductory Programming course of Computer Science and Software Engineering Graduation Programs at the Federal University of Rio Grande do Norte, Brazil. The study results have shown that, when compared to a Blind Testing approach, POPT stimulates the implementation of programs of better external quality the first program version submitted by POPT students passed in twice the number of test cases (professor-defined ones) when compared to non-POPT students. Moreover, POPT students submitted fewer program versions and spent more time to submit the first version to the automatic evaluation system, which lead us to think that POPT students are stimulated to think better about the solution they are implementing. The controlled experiment confirmed the influence of the proposed methodology on the quality of the code developed by POPT students

Geração de testes a partir de gramáticas: áreas de aplicação

The work proposed by Cleverton Hentz (2010) presented an approach to define tests from the formal description of a program s input. Since some programs, such as compilers, may have their inputs formalized through grammars, it is common to use context-free grammars to specify the set of its valid entries. In the original work the author developed a tool that automatically generates tests for compilers. In the present work we identify types of problems in various areas where grammars are used to describe them , for example, to specify software configurations, which are potential situations to use LGen. In addition, we conducted case studies with grammars of different domains and from these studies it was possible to evaluate the behavior and performance of LGen during the generation of sentences, evaluating aspects such as execution time, number of generated sentences and satisfaction of coverage criteria available in LGen

Avaliando a robustez e manutenibilidade do comportamento excepcional de aplicações C#

Mainstream programming languages provide built-in exception handling mechanisms to support robust and maintainable implementation of exception handling in software systems. Most of these modern languages, such as C#, Ruby, Python and many others, are often claimed to have more appropriated exception handling mechanisms. They reduce programming constraints on exception handling to favor agile changes in the source code. These languages provide what we call maintenance-driven exception handling mechanisms. It is expected that the adoption of these mechanisms improve software maintainability without hindering software robustness. However, there is still little empirical knowledge about the impact that adopting these mechanisms have on software robustness. This work addresses this gap by conducting an empirical study aimed at understanding the relationship between changes in C# programs and their robustness. In particular, we evaluated how changes in the normal and exceptional code were related to exception handling faults. We applied a change impact analysis and a control flow analysis in 100 versions of 16 C# programs. The results showed that: (i) most of the problems hindering software robustness in those programs are caused by changes in the normal code, (ii) many potential faults were introduced even when improving exception handling in C# code, and (iii) faults are often facilitated by the maintenance-driven flexibility of the exception handling mechanism. Moreover, we present a series of change scenarios that decrease the program robustness

Análise da rede política do turismo brasileiro.

The dissertation examines the influence of relationships among actors from Brazilian Tourism Political Network who compose the National Council of Tourism in the drafting of the National Tourism Plans (PNT) - PNTs 2003/2007 and 2007/2010, focusing on two main types of interaction: cooperation and information exchange. Therefore, the study departed from the understanding that the concept of tourism as a human phenomenon is configured as an essential conceptual basis for the development, implementation and analysis of public policies. The application of Network Theory and Social Network Analysis serves as an analytical tool, in addition, the use of concepts of Policy Networks enabled to interpret, in distinct aspects, the social reality of tourism in a more precise and detailed way. The study had a cross-sectional with a longitudinal perspective and case study was adopted, thus enabling to apply the model of social network analysis and qualitative approach. Through the survey conducted, it was found that the drafting process of National Tourism Plans was the result of the interaction of a complex network of actors from public and private initiatives, who compose the National Council of Tourism, and that their power of influence came out simultaneously, but not symmetrically, for both their performance/intervention in the meetings, and the possession of economic and organizational resources. Hence, the establishment of partnerships and information exchanges among the actors were underlying to the PNT drafting process, both in problems perception and insertion in the government agenda, as in making proposals to solve them, thus guiding the construction of large programs and programs contained in both investigated plans.

GESTÃO AMBIENTAL E COMPETITIVIDADE EM DESTINOS TURÍSTICOS: percepção dos gestores de pequenos meios de hospedagem de Natal/RN sobre o uso de práticas ambientais como fator de competitividade

The present work aimed at investigating the small hotel managers perceptions from Natal/RN concerning the environmental practice uses as a competitive factor. This study is characterized as a descriptive exploratory research that used an aleatory probabilistic sample followed by the application of collect data instrument (questionnaire). The small hotels located in Natal/RN were the study participants and the specific location where 35 questionnaires were answered. Based on the data and on the mangers point of view, it is possible to comprehend that, among the presented indicators, the development of environmental programs in the hotel enterprise is showed as the least important for the client s choice. As the main conclusion it is relevant to argue that, according to the small hotel managers, the guests do not still search for hotels that implement environmental practices. On the other side, the interviewed managers believe that the use of these practices can generate a great competitive advantage in relation to their competitors. The information obtained by this present research will be able to contribute to establish a contemporary panorama in relation to the importance attributed by the managers concerning the use of environmental practices in small hotel enterprises in Natal/RN. In addition the correct use of this information can generate possibilities of major competitiveness in this segment

Determinantes de competitividade de destinos turísticos aplicados aos roteiros regionais: uma avaliação do roteiro Seridó/RN

The tourism industry is gaining representation by move and stimulate the economy, especially by allowing the generation of employment and income, thus allowing growth opportunities for localities where tourism develops. Therefore, the present study entitled determinants of competitiveness of tourist destinations applied to regional routes: an evaluation of the Route of Seridó/RN, discusses the issue of competitiveness in tourism and tries to understand the scenery of this Route. The main objective of the study is to assess the conditions of competitiveness in the Route of Seridó/RN according to benchmarks and global determinants of competitiveness for tourist destinations. The study has also as specifics objectives: define dimensions of the reference model for use in evaluating the competitiveness of the Route of Seridó/RN; identify levels of governance and competitiveness in the municipalities that make up the sample set above the Route, and analyze to what extent the competitiveness of the Route correspond to the global reference of competitiveness of tourism destinations. Regarding the methodology, it is a search for an exploratory- descriptive and used a combination of quantitative and qualitative research method as expected and required in the implementation of the evaluation tool called Compet&enible Model. For data collection, it has been taken technical visits and also analysis of documents and materials. Data analysis was based on the records and documents and the use of simple descriptive statistics for the scores of the elements offered by Compet&enible Model. The results allowed us to know the real conditions of competitiveness of the Seridó/RN Route forward to the attributes of tourist destinations for global competitiveness: the dimension I, Governance, reached 17 points, classified as "in structuring" and dimension II, Competitiveness, reached 10 points, ranking "weak". These results highlight the need for greater involvement of the actors in the supply chain of tourism in Polo Seridó/RN for the actions, programs and projects are put into practice. It is expected that tourism is considered an important activity for the local and global development, serving as a reference for the future management of Seridó/RN Route, guiding new policy guidelines, planning and organization to better competitiveness

Dinâmica da paisagem na Microbacia do Riacho Cajazeiras no semiárido potiguar

The semi-arid Northeast region are coming through changes since its formation causing changes in the landscape and increased degradation. The economic dynamics which was established at the Potiguar semiarid had for a long time settled in livestock, subsistence agriculture and cotton, however, these economies decline from the year 1970. Thus, the Potiguar spaces are undergoing by a process of space reordering marked by the growth of agricultural activities and the process of urbanization. In the Potiguar western region these changes weaken significantly transform the landscape. In these areas, the process of urbanization and agricultural activities have caused changes in the hinterland landscape changing the natural dynamics of the caatinga biome that has been subject to negative interference with the indiscriminate removal of vegetation. In this case, the specific study area of the watershed of Cajazeiras Creek located in the cities of Pau dos Ferros, Água Nova, Encanto and Rafael Fernandes, changes in the landscape has led to degradation and environmental fragility. From this perspective, the research objective is to assess the dynamics of the landscape of the watershed of Cajazeiras Creek, semiarid region of the state of Rio Grande do Norte, identifying the degrading factors, the most degraded areas and/or susceptible to degradation and environmental fragility. The research investigated the phenomena of light geosystems theory that emphasizes the integration of elements in shaping the landscape. During this reporting period, it was carried out exploratory and bibliographical research, and geoprocessing techniques to assess the social and environmental conditions of the researched area and its environmental fragility. To do so, first, it was made an multitemporal analisis on the basis of the years 1984, 1996 and 2009 demonstrating that the dynamics of use and land cover in the watershed of Cajazeiras Creek showed a significant change in the landscape, especially in the caatinga vegetation. This has been recovering in various areas of the watershed, especially in its upper course in the mountains of Bom Sera, in Encanto city. The analysis showed the need to develop policies and programs for the maintenance, restoration and preservation of the caatinga vegetation of the river network and of water bodies. In addition, it was identified the most degraded areas of the watershed, environmental fragility and potential emerging that take into account the landscape components such as climate, topography, geology, pedology, geomorphology and the use and occupation of the soil in an integrated manner. The results show that the landscape of the watershed has medium and high environmental fragility throughout its area, especially on the banks of the river network provided by the use and occupation of the soil in an inadequate way with the environmental conditions of the watershed

Redesenho das configurações estruturais na gestão universitária: ações derivadas da inovação e flexibilidade na legislação pós-LDB 1996

This paper is set in a scenario in which higher education institutions suffer from external pressure to increase efficiency. The legislation after the Law of Directives and Bases for Education (LDBE), from 1996, is characterized by the fragmentation in its implementation, raising a concern with flexibility and innovation in several normative devices as well as aspects that must be incorporated to its organizational structure. The policies examined in this thesis are: Distance Education (DE); Law of Innovation and the Program of Support to Restructuring and Expansion of Federal Universities (PSREFU). This thesis aims to observe to what extent the characteristics of innovation and flexibility, which mark the new post- LDBE educational legislation, influence the organizational redesign of the Federal University of Ceará (UFC). For being about implementation policies, using contingency approach in order to collect the internal dynamics permeating the redesign of higher education institutions, the thesis focuses on the impacts caused by flexibility and innovation. This is a qualitative research, with case study methods, archive research and semi-structured interviews with members of the university administration. The results don t allow us to confirm the adoption of a more flexible and innovative configuration in the university but it is possible to identify the presence of those elements in the implementation changes, characterizing the hybrid structure. The changes mainly expose the extension of the management of projects to the administrative and academic components related to the institution. In terms of projection, the study found changes in the elements which characterize the current setting and the tendency of the university for adopting a diverse organizational structure. However, if the decentralization of management persists, the academic units may adopt their own structural solutions, but with no evidence of changes in the professional organization in most units. In this perspective, this thesis states that there are difficulties when incorporating innovation and flexibility to their organizational structure, which lead to improvised solutions, superposing skills through the redundancy of structures created with the same purpose or copying exogenous solutions