Geração automática de hardware apartir de especificações formais: estendendo uma abordagem de tradução

A remoção de inconsistências em um projeto é menos custosa quando realizadas nas etapas iniciais da sua concepção. A utilização de Métodos Formais melhora a compreensão dos sistemas além de possuir diversas técnicas, como a especificação e verificação formal, para identificar essas inconsistências nas etapas iniciais de um projeto. Porém, a transformação de uma especificação formal para uma linguagem de programação é uma tarefa não trivial. Quando feita manualmente, é uma tarefa passível da inserção de erros. O uso de ferramentas que auxiliem esta etapa pode proporcionar grandes benefícios ao produto final a ser desenvolvido. Este trabalho propõe a extensão de uma ferramenta cujo foco é a tradução automática de especificações em CSPm para Handel-C. CSP é uma linguagem de descrição formal adequada para trabalhar com sistemas concorrentes. Handel-C é uma linguagem de programação cujo resultado pode ser compilado diretamente para FPGA's. A extensão consiste no aumento no número de operadores CSPm aceitos pela ferramenta, permitindo ao usuário definir processos locais, renomear canais e utilizar guarda booleana em escolhas externas. Além disto, propomos também a implementação de um protocolo de comunicação que elimina algumas restrições da composição paralela de processos na tradução para Handel-C, permitindo que a comunicação entre múltiplos processos possa ser mapeada de maneira consistente e que a mesma somente ocorra quando for autorizada.

Geração automática de hardware a partir de especificações formais: estendendo uma abordagem de tradução

Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification

MaRISA-AOCode: uma abordagem genérica para geração de código orientado a aspectos

Currently there are several aspect-oriented approaches that are related to different stages of software development process. These approaches often lack integration with each other and their models and artifacts are not aligned in a coherent process. The integration of Aspect-Oriented Software development (AOSD) and Model-Driven Development (MDD) enables automatic propagation of models from one phase to another, avoiding loss of important information and decisions established in each. This paper presents a model driven approach, called Marisa-AOCode, which supports the processing of detailed design artifacts to code in different Aspect-Oriented Programming languages. The approach proposed by Maris- AOCode defines transformation rules between aSideML, a modeling language for aspectoriented detailed design, and Metaspin, a generic metamodel for aspect-oriented programming languages. The instantiation of the generic metamodel (Metaspin) provided by the approach of Maris-AOCode is illustrated by the transformation of Metaspin for two languages: AspectLua and CaesarJ. We illustrate the approach with a case study based on the Health Watcher System

Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

Uma estratégia dirigida a modelos e baseada em linguagem de descrição arquitetural para linhas de produtos de software

Model-oriented strategies have been used to facilitate products customization in the software products lines (SPL) context and to generate the source code of these derived products through variability management. Most of these strategies use an UML (Unified Modeling Language)-based model specification. Despite its wide application, the UML-based model specification has some limitations such as the fact that it is essentially graphic, presents deficiencies regarding the precise description of the system architecture semantic representation, and generates a large model, thus hampering the visualization and comprehension of the system elements. In contrast, architecture description languages (ADLs) provide graphic and textual support for the structural representation of architectural elements, their constraints and interactions. This thesis introduces ArchSPL-MDD, a model-driven strategy in which models are specified and configured by using the LightPL-ACME ADL. Such strategy is associated to a generic process with systematic activities that enable to automatically generate customized source code from the product model. ArchSPLMDD strategy integrates aspect-oriented software development (AOSD), modeldriven development (MDD) and SPL, thus enabling the explicit modeling as well as the modularization of variabilities and crosscutting concerns. The process is instantiated by the ArchSPL-MDD tool, which supports the specification of domain models (the focus of the development) in LightPL-ACME. The ArchSPL-MDD uses the Ginga Digital TV middleware as case study. In order to evaluate the efficiency, applicability, expressiveness, and complexity of the ArchSPL-MDD strategy, a controlled experiment was carried out in order to evaluate and compare the ArchSPL-MDD tool with the GingaForAll tool, which instantiates the process that is part of the GingaForAll UML-based strategy. Both tools were used for configuring the products of Ginga SPL and generating the product source code

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

Geração de casos de teste a partir de especificações B

With the increasing complexity of software systems, there is also an increased concern about its faults. These faults can cause financial losses and even loss of life. Therefore, we propose in this paper the minimization of faults in software by using formally specified tests. The combination of testing and formal specifications is gaining strength in searches mainly through the MBT (Model-Based Testing). The development of software from formal specifications, when the whole process of refinement is done rigorously, ensures that what is specified in the application will be implemented. Thus, the implementation generated from these specifications would accurately depict what was specified. But not always the specification is refined to the level of implementation and code generation, and in these cases the tests generated from the specification tend to find fault. Additionally, the generation of so-called "invalid tests", ie tests that exercise the application scenarios that were not addressed in the specification, complements more significantly the formal development process. Therefore, this paper proposes a method for generating tests from B formal specifications. This method was structured in pseudo-code. The method is based on the systematization of the techniques of black box testing of boundary value analysis, equivalence partitioning, as well as the technique of orthogonal pairs. The method was applied to a B specification and B test machines that generate test cases independent of implementation language were generated. Aiming to validate the method, test cases were transformed manually in JUnit test cases and the application, created from the B specification and developed in Java, was tested. Faults were found with the execution of the JUnit test cases

Metodologia para modelagem, validação e programação de controladores lógicos industriais usando statecharts básicos

Due of industrial informatics several attempts have been done to develop notations and semantics, which are used for classifying and describing different kind of system behavior, particularly in the modeling phase. Such attempts provide the infrastructure to resolve some real problems of engineering and construct practical systems that aim at, mainly, to increase the productivity, quality, and security of the process. Despite the many studies that have attempted to develop friendly methods for industrial controller programming, they are still programmed by conventional trial-and-error methods and, in practice, there is little written documentation on these systems. The ideal solution would be to use a computational environment that allows industrial engineers to implement the system using high-level language and that follows international standards. Accordingly, this work proposes a methodology for plant and control modelling of the discrete event systems that include sequential, parallel and timed operations, using a formalism based on Statecharts, denominated Basic Statechart (BSC). The methodology also permits automatic procedures to validate and implement these systems. To validate our methodology, we presented two case studies with typical examples of the manufacturing sector. The first example shows a sequential control for a tagged machine, which is used to illustrated dependences between the devices of the plant. In the second example, we discuss more than one strategy for controlling a manufacturing cell. The model with no control has 72 states (distinct configurations) and, the model with sequential control generated 20 different states, but they only act in 8 distinct configurations. The model with parallel control generated 210 different states, but these 210 configurations act only in 26 distinct configurations, therefore, one strategy control less restrictive than previous. Lastly, we presented one example for highlight the modular characteristic of our methodology, which it is very important to maintenance of applications. In this example, the sensors for identifying pieces in the plant were removed. So, changes in the control model are needed to transmit the information of the input buffer sensor to the others positions of the cell

Dos requisitos à arquitetura em linhas de produtos de software: uma estratégia de transformações entre modelos

The tracking between models of the requirements and architecture activities is a strategy that aims to prevent loss of information, reducing the gap between these two initial activities of the software life cycle. In the context of Software Product Lines (SPL), it is important to have this support, which allows the correspondence between this two activities, with management of variability. In order to address this issue, this paper presents a process of bidirectional mapping, defining transformation rules between elements of a goaloriented requirements model (described in PL-AOVgraph) and elements of an architectural description (defined in PL-AspectualACME). These mapping rules are evaluated using a case study: the GingaForAll LPS. To automate this transformation, we developed the MaRiPLA tool (Mapping Requirements to Product Line Architecture), through MDD techniques (Modeldriven Development), including Atlas Transformation Language (ATL) with specification of Ecore metamodels jointly with Xtext , a DSL definition framework, and Acceleo, a code generation tool, in Eclipse environment. Finally, the generated models are evaluated based on quality attributes such as variability, derivability, reusability, correctness, traceability, completeness, evolvability and maintainability, extracted from the CAFÉ Quality Model

ISE-SPL: Uma abordagem baseada em linha de produtos de software aplicada à geração automática de sistemas para educação médica na plataforma E-learning

E-learning, which refers to the use of Internet-related technologies to improve knowledge and learning, has emerged as a complementary form of education, bringing advantages such as increased accessibility to information, personalized learning, democratization of education and ease of update, distribution and standardization of the content. In this sense, this paper aims to develop a tool, named ISE-SPL, whose purpose is the automatic generation of E-learning systems for medical education, making use of concepts of Software Product Lines. It consists of an innovative methodology for medical education that aims to assist professors of healthcare in their teaching through the use of educational technologies, all based on computing applied to healthcare (Informatics in Health). The tests performed to validate the ISE-SPL were divided into two stages: the first was made by using a software analysis tool similar to ISE-SPL, called SPLOT and the second was performed through usability questionnaires to healthcare professors who used ISESPL. Both tests showed positive results, proving it to be an efficient tool for generation of E-learning software and useful for professors in healthcare

Estudos de algumas ferramentas de coleta e visualização de dados e desempenho de aplicações paralelas no ambiente MPI

The last years have presented an increase in the acceptance and adoption of the parallel processing, as much for scientific computation of high performance as for applications of general intention. This acceptance has been favored mainly for the development of environments with massive parallel processing (MPP - Massively Parallel Processing) and of the distributed computation. A common point between distributed systems and MPPs architectures is the notion of message exchange, that allows the communication between processes. An environment of message exchange consists basically of a communication library that, acting as an extension of the programming languages that allow to the elaboration of applications parallel, such as C, C++ and Fortran. In the development of applications parallel, a basic aspect is on to the analysis of performance of the same ones. Several can be the metric ones used in this analysis: time of execution, efficiency in the use of the processing elements, scalability of the application with respect to the increase in the number of processors or to the increase of the instance of the treat problem. The establishment of models or mechanisms that allow this analysis can be a task sufficiently complicated considering parameters and involved degrees of freedom in the implementation of the parallel application. An joined alternative has been the use of collection tools and visualization of performance data, that allow the user to identify to points of strangulation and sources of inefficiency in an application. For an efficient visualization one becomes necessary to identify and to collect given relative to the execution of the application, stage this called instrumentation. In this work it is presented, initially, a study of the main techniques used in the collection of the performance data, and after that a detailed analysis of the main available tools is made that can be used in architectures parallel of the type to cluster Beowulf with Linux on X86 platform being used libraries of communication based in applications MPI - Message Passing Interface, such as LAM and MPICH. This analysis is validated on applications parallel bars that deal with the problems of the training of neural nets of the type perceptrons using retro-propagation. The gotten conclusions show to the potentiality and easinesses of the analyzed tools.

Fresamento com ar quente: uma proposta para minimizar a formação de trincas térmicas em ferramentas de metal duro

This work presents the results, analyses and conclusions about a study carried out with objective of minimizing the thermal cracks formation on cemented carbide inserts during face milling. The main focus of investigation was based on the observation that milling process is an interrupted machining process, which imposes cyclic thermal loads to the cutting tool, causing frequent stresses changes in its superficial and sub-superficial layers. These characteristics cause the formation of perpendicular cracks from cutting edge which aid the cutting tool wear, reducing its life. Several works on this subject emphasizing the thermal cyclic behavior imposed by the milling process as the main responsible for thermal cracks formation have been published. In these cases, the phenomenon appears as a consequence of the difference in temperature experienced by the cutting tool with each rotation of the cutter, usually defined as the difference between the temperatures in the cutting tool wedge at the end of the cutting and idle periods (T factor). Thus, a technique to minimize this cyclic behavior with objective of transforming the milling in an almost-continuous process in terms of temperature was proposed. In this case, a hot air stream was applied into the idle period, during the machining process. This procedure aimed to minimize the T factor. This technique was applied using three values of temperature from the hot air stream (100, 350 e 580 oC) with no cutting fluid (dry condition) and with cutting fluid mist (wet condition) using the hot air stream at 580oC. Besides, trials at room temperature were carried out. Afterwards the inserts were analyzed using a scanning electron microscope, where the quantity of thermal cracks generated in each condition, the wear and others damages was analyzed. In a general way, it was found that the heating of the idle period was positive for reducing the number of thermal cracks during face milling with cemented carbide inserts. Further, the cutting fluid mist application was effective in reducing the wear of the cutting tools.

Secagem do resíduo de acerola (Malphigia emarginata D.C.): estudo do processo e avaliação do impacto sobre o produto final

Brazil, one of the largest agricultural producers in the world, has managed in recent years to significantly improve its production. However, in response to this advance in the agro-industrial sector, the generation of agro-industrial residues has also increased. New technological alternatives have to be implemented in order to bring economic and rational use of this material and drying is one of the possible choices. Considering the great importance that bioactive compounds present for food science and technology, this research aims to evaluate the air-drying process of acerola residue in a tray convective drier under controlled temperature (60, 70 e 80ºC), air velocity (4.0, 5.0 e 6.0 m/s) and material width (0.5, 0.62 e 0.75 cm) by applying an experimental planning 23 + 3. Based on that, the impact on physical-chemical characteristics, color, bioactive compounds concentration and antioxidant activity of dried acerola waste was evaluated, having the in natura and freeze dried waste as control groups. Dried acerola residue presented natural pigments, mainly carotenoids (143.68 - 68.29 mg/g) and anthocyanins (290.92 - 90.11 mg/100 g), which explain the red and yellow instrumental color parameters observed. The acerola residue powder is also rich in phenolic compounds (3261.11 -2692.60 mgGAEeq/100g), proanthocyanidins (61.33-58.46 eq/100g), ascorbic acid (389.44 739.29 mg/100 g) and DPPH antioxidant activity (20.91 24.72 μg Trolox eq/g). Results show decreased concentration of phenolic compounds, anthocyanins, carotenoids, proanthocyanidins and ascorbic acid caused by the air-drying process. However, even after the observed drying losses, the acerola residue powder can be considered a high value food ingredient, considering the high bioactive compounds concentration found in the final product, as well as the colorimetric characterization and microbiological stability of the dried powder

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"

Floração precoce em cana-de-açúcar - um estudo utilizando ferramentas de análise in silico e proteômica

Sugarcane is one of the most important products of the world and Brazil is responsible for 25 % of the world production. One problem of this culture at northeast of Brazil is the early flowering. In our laboratory, it has been made before four subtractive libraries using early and late flowering genotypes in order to identify messages related to the flowering process. In this work, two cDNAs were chosen to make in silico analysis and overexpression constructs. Another approach to understand the flowering process in sugarcane was to use proteomic tools. First, the protocol for protein extraction using apical meristem was set up. After that, these proteins were separated on two bidimensional gels. It was possible to observe some difference for some regions of these gels as well as some proteins that can be found in all conditions. The next step, spots will be isolated and sequence on MS spectrometry in order to understand this physiological process in sugarcane