Especificação do tipo intervalar parametrizado em CASL

The interval datatype applications in several areas is important to construct a interval type reusable, i.e., a interval constructor can be applied to any datatype and get intervals this datatype. Since the interval is, of certain form, a set of elements limited for two bounds, left and right, with a order notions, then it s reasonable that interval constructor enclose datatypes with partial order. On the order hand, what we want is work with interval of any datatype like this we work with this datatype then. it s important to guarantee the properties of the datatype when maps to interval of this datatype. Thus, the interval constructor get a theory to parametrized interval type, i.e., a interval with generics parameters (for example rational, real, complex). Sometimes, the interval application in some algebras doesn t guarantee the mainutenance of their properties, for example, when we use interval of real, that satisfies the field properties, it doesn t guarantee the distributivity propertie. A form to surpass this problem Santiago introduced the local equality theory that weakened the notion of strong equality, and thus, allowing some properties are local keeped, what can be discard before. The interval arithmetic generalization aim to apply the interval constructor on ordered algebras weakened for local equality with the purpose of the keep their properties. How the intervals are important in applications with continuous data, it s interesting specify that theory using a specification language that supply a system development using intervals of form disciplined, trustworth and safe. Currently, the algebraic specification language, based in math models, have been use to that intention often. We choose CASL (Common Algebraic Specification Language) among others languages because CASL has several characteristics excellent to parametrized interval type, such as, provide parcialiy and parametrization

Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)

Este trabalho apresenta uma técnica de verificação formal de Sistemas de Raciocínio Procedural, PRS (Procedural Reasoning System), uma linguagem de programação que utiliza a abordagem do raciocínio procedural. Esta técnica baseia-se na utilização de regras de conversão entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, são apresentadas regras de conversão de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verificação formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verificação das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional disponível para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de conversão PRS-RPC, podemos ser levados a querer fazer esta conversão de maneira estritamente manual. No entanto, a probabilidade de introdução de erros na conversão é grande, fazendo com que o esforço necessário para garantirmos a corretude da conversão manual seja da mesma ordem de grandeza que a eliminação de eventuais erros diretamente no programa PRS original. Assim, a conversão automatizada é de suma importância para evitar que a conversão manual nos leve a erros indesejáveis, podendo invalidar todo o processo de conversão. A principal contribuição deste trabalho de pesquisa diz respeito ao desenvolvimento de uma técnica de verificação formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de conversão de PRS para RPC. A segunda fase é concernente ao desenvolvimento de um conversor para fazer a transformação de maneira automatizada dos programas PRS para as RPCs. A conversão automática é possível, porque todas as regras de conversão apresentadas seguem leis de formação genéricas, passíveis de serem incluídas em algoritmos

Simulação da destilação molecular de filme descendente para o petróleo

The heavy part of the oil can be used for numerous purposes, e.g. to obtain lubricating oils. In this context, many researchers have been studying alternatives such separation of crude oil components, among which may be mentioned molecular distillation. Molecular distillation is a forced evaporation technique different from other conventional processes in the literature. This process can be classified as a special distillation case under high vacuum with pressures that reach extremely low ranges of the order of 0.1 Pascal. The evaporation and condensation surfaces must have a distance from each other of the magnitude order of mean free path of the evaporated molecules, that is, molecules evaporated easily reach the condenser, because they find a route without obstacles, what is desirable. Thus, the main contribution of this work is the simulation of the falling-film molecular distillation for crude oil mixtures. The crude oil was characterized using UniSim® Design and R430 Aspen HYSYS® V8.5. The results of this characterization were performed in spreadsheets of Microsoft® Excel®, calculations of the physicochemical properties of the waste of an oil sample, i.e., thermodynamic and transport. Based on this estimated properties and boundary conditions suggested by the literature, equations of temperature and concentration profiles were resolved through the implicit finite difference method using the programming language Visual Basic® (VBA) for Excel®. The result of the temperature profile showed consistent with the reproduced by literature, having in their initial values a slight distortion as a result of the nature of the studied oil is lighter than the literature, since the results of the concentration profiles were effective allowing realize that the concentration of the more volatile decreases and of the less volatile increases due to the length of the evaporator. According to the transport phenomena present in the process, the velocity profile tends to increase to a peak and then decreases, and the film thickness decreases, both as a function of the evaporator length. It is concluded that the simulation code in Visual Basic® language (VBA) is a final product of the work that allows application to molecular distillation of petroleum and other similar mixtures.

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Otimização de um sistema de distribuição predial de água fria: estudo de caso

This dissertation presents a methodology to the optimization of a predial system of cold water distribution. It s about a study of a case applied to the Tropical Buzios Residential Condominium, located in the Búzio s Beach, Nísia Floresta city, the east coast of the Rio Grande do Norte state, twenty kilometers far from Natal. The design of cold water distribution networks according to Norm NBR 5626 of the ABNT - Brazilian Association of Techniques Norms, does not guarantee that the joined solution is the optimal solution of less cost. It s necessary the use of an optimization methodology, that supplies us, between all the possible solutions, the minimum cost solution. In the optimization process of the predial system of water distribution of the Tropical Búzios Condominium, is used Method Granados, that is an iterative algorithm of optimization, based on the Dynamic Programming, that supplies the minimum cost s network, in function of the piezometric quota of the reservoir. For the application of this Method in ramifies networks, is used a program of computer in C language. This process is divided in two stages: attainment of the previous solution and reduction of the piezometric quota of headboard. In the attainment of the previous solution, the minors possible diameters are used that guarantee the limit of maximum speed and the requirements of minimum pressures. The piezometric quota of headboard is raised to guarantee these requirements. In the second stage of the Granados Method, an iterative process is used and it objective is to reduce the quota of headboard gradually, considering the substitution of stretches of the network pipes for the subsequent diameters, considering a minimum addition of the network cost. The diameter change is made in the optimal stretch that presents the lesser Exchange Gradient. The process is locked up when the headboard quota of desired is reached. The optimized network s material costs are calculated, and is made the analysis of the same ones, through the comparison with the conventional network s costs

Controle vetorial de velocidade de uma máquina de indução sem mancais trifásica com bobinado dividido utilizando estimação neural de fluxo

This work describes the study and the implementation of the vector speed control for a three-phase Bearingless induction machine with divided winding of 4 poles and 1,1 kW using the neural rotor flux estimation. The vector speed control operates together with the radial positioning controllers and with the winding currents controllers of the stator phases. For the radial positioning, the forces controlled by the internal machine magnetic fields are used. For the radial forces optimization , a special rotor winding with independent circuits which allows a low rotational torque influence was used. The neural flux estimation applied to the vector speed controls has the objective of compensating the parameter dependences of the conventional estimators in relation to the parameter machine s variations due to the temperature increases or due to the rotor magnetic saturation. The implemented control system allows a direct comparison between the respective responses of the speed and radial positioning controllers to the machine oriented by the neural rotor flux estimator in relation to the conventional flux estimator. All the system control is executed by a program developed in the ANSI C language. The DSP resources used by the system are: the Analog/Digital channels converters, the PWM outputs and the parallel and RS-232 serial interfaces, which are responsible, respectively, by the DSP programming and the data capture through the supervisory system

Controle vetorial de velocidade de um motor de indução trifásico com estimação neural de fluxo

This work describes the study and the implementation of the speed control for a three-phase induction motor of 1,1 kW and 4 poles using the neural rotor flux estimation. The vector speed control operates together with the winding currents controller of the stator phasis. The neural flux estimation applied to the vector speed controls has the objective of compensating the parameter dependences of the conventional estimators in relation to the parameter machine s variations due to the temperature increases or due to the rotor magnetic saturation. The implemented control system allows a direct comparison between the respective responses of the speed controls to the machine oriented by the neural rotor flux estimator in relation to the conventional flux estimator. All the system control is executed by a program developed in the ANSI C language. The main DSP recources used by the system are, respectively, the Analog/Digital channels converters, the PWM outputs and the parallel and RS-232 serial interfaces, which are responsible, respectively, by the DSP programming and the data capture through the supervisory system

Uma proposta de regulador nebuloso para geradores eólicos de indução

This work presents a proposal for a voltage and frequency control system for a wind power induction generator. It has been developed na experimental structure composes basically by a three phase induction machine, a three phase capacitor and a reactive static Power compensator controlled by histeresys. lt has been developed control algorithms using conventional methods (Pl control) and linguistic methods (using concepts of logic and fuzzy control), to compare their performances in the variable speed generator system. The control loop was projected using the ADJDA PCL 818 model board into a Pentium 200 MHz compu ter. The induction generator mathematical model was studied throught Park transformation. It has been realized simulations in the Pspice@ software, to verify the system characteristics in transient and steady-state situations. The real time control program was developed in C language, possibilish verify the algorithm performance in the 2,2kW didatic experimental system

Estudo e implementação em plantas físicas de um controlador preditivo generalizado com restrições

This work shows a study about the Generalized Predictive Controllers with Restrictions and their implementation in physical plants. Three types of restrictions will be discussed: restrictions in the variation rate of the signal control, restrictions in the amplitude of the signal control and restrictions in the amplitude of the Out signal (plant response). At the predictive control, the control law is obtained by the minimization of an objective function. To consider the restrictions, this minimization of the objective function is done by the use of a method to solve optimizing problems with restrictions. The chosen method was the Rosen Algorithm (based on the Gradient-projection). The physical plants in this study are two didactical systems of water level control. The first order one (a simple tank) and another of second order, which is formed by two tanks connected in cascade. The codes are implemented in C++ language and the communication with the system to be done through using a data acquisition panel offered by the system producer

O ritual simbólico do Ctrl+C (copiar ) e Ctrl+V (colar) no ensino médio

Nowadays, technology has a direct influence on the relationship student and teacher have with language. The internet is a powerful tool in helping work with the language and, through it, the knowledge comes to the student easily and intensely. Furthermore, this facility has enhanced and made visible what has been called, within the University community, "plagiarism generation." This work assumes that this generation has, in their written texts, symbolic movements similar to those of "copy and paste" applied to research work carried out by high school students. Taking this as starting point, this dissertation aims to analyze how high school students of the 1st year from a school in Natal (RN) construct texts, under the movements known as "Ctrl + c" and "Ctrl + v", with reference to the text of the "other". More specific issues are behind the general objective, namely: 1. how the student appropriates the source-text when he copies and pastes? 2. What are the categories of analysis that allow us to look analytically and theoretically for the "ctrl + c / ctrl + v" practice made by the student? 2. how the studies developed in the fields of "Genetic Criticism" (Grésillon, 1987), the "school manuscripts" (Calil, 2004) and "paraphrase" (Fuchs, 1982) may help in working with writing in the classroom standing as a possible way to minimize the copy and paste effects in the students texts? Thus, we observe the categories of analysis that allow us to look, theoretically and analytically, for the symbolic ritual of the "ctrl + c" (copy) and "ctrl + v" (paste) in high school. Our study shows that the student text is a "hybrid body" whose writing is a drawing entanglement because of the presence of the foreign text, verbatim, and the presence of linguistic elements to paraphrase the original text.This textual embodiment has, behind it, certain operations, namely: replacing, moving, adding and deleting statements. Given the specificity of the data and the research objectives, this study aligns with qualitative research methods (SILVERMAN, 2009) and falls within the knowledge field of Applied Linguistics, which is characterized especially by investigating problems, phenomena in which language in a real situation is taken as central (BRUMFIT, 1995).Theoretically, our work follows the approach of studies on the paraphrase (Fuchs, 1982, 1994a, 1994b; DAUNAY, 1997, 1999, 2002a, 2002b), the studies developed in the field of Genetic Criticism (Grésillon, 1987, 1994, 1992, 2008 ) and those developed by Eduardo Calil (2004) on "school manuscripts"

Projeto e implementação de uma plataforma MP-SoC usando SystemC

This work presents the concept, design and implementation of a MP-SoC platform, named STORM (MP-SoC DirecTory-Based PlatfORM). Currently the platform is composed of the following modules: SPARC V8 processor, GPOP processor, Cache module, Memory module, Directory module and two different modles of Network-on-Chip, NoCX4 and Obese Tree. All modules were implemented using SystemC, simulated and validated, individually or in group. The modules description is presented in details. For programming the platform in C it was implemented a SPARC assembler, fully compatible with gcc s generated assembly code. For the parallel programming it was implemented a library for mutex managing, using the due assembler s support. A total of 10 simulations of increasing complexity are presented for the validation of the presented concepts. The simulations include real parallel applications, such as matrix multiplication, Mergesort, KMP, Motion Estimation and DCT 2D

LWiSSy: uma linguagem específica de domínio para modelagem de sistemas de redes de sensores e atuadores sem fio

The field of Wireless Sensor and Actuator Networks (WSAN) is fast increasing and has attracted the interest of both the research community and the industry because of several factors, such as the applicability of such networks in different application domains (aviation, civil engineering, medicine, and others). Moreover, advances in wireless communication and the reduction of hardware components size also contributed for a fast spread of these networks. However, there are still several challenges and open issues that need to be tackled in order to achieve the full potential of WSAN usage. The development of WSAN systems is one of the most relevant of these challenges considering the number of variables involved in this process. Currently, a broad range of WSAN platforms and low level programming languages are available to build WSAN systems. Thus, developers need to deal with details of different sensor platforms and low-level programming abstractions of sensor operational systems on one hand, and they also need to have specific (high level) knowledge about the distinct application domains, on the other hand. Therefore, in order to decouple the handling of these two different levels of knowledge, making easier the development process of WSAN systems, we propose LWiSSy (Domain Language for Wireless Sensor and Actuator Networks Systems), a domain specific language (DSL) for WSAN. The use of DSLs raises the abstraction level during the programming of systems and modularizes the system building in several steps. Thus, LWiSSy allows the domain experts to directly contribute in the development of WSANs without having knowledge on low level sensor platforms, and network experts to program sensor nodes to meet application requirements without having specific knowledge on the application domain. Additionally, LWiSSy enables the system decomposition in different levels of abstraction according to structural and behavioral features and granularities (network, node group and single node level programming)

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

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

Interfaces cérebro-computador: estudo, design e desenvolvimento do jogo AdmiralMind Battleship

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior