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

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

Joker: um realizador de desenhos animados para linguagens formais

Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++.

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

OZJ : uma ferramenta para geração de óraculos para teste de software a partir de especificação formal

A literatura sobre Teste de Software apresenta diversas estratégias e metodologias que definem critérios eficazes e automatizáveis para selecionar casos de teste capazes de detectar erros em softwares. Embora eficientes na descoberta de erros, as técnicas de seleção de casos de teste exigem que uma quantidade relativamente grande de testes seja realizada para satisfazer os seus critérios. Essa característica acarreta, em parte, um alto custo na atividade de teste, uma vez que, ao fim de cada teste deve-se verificar se o comportamento do software está ou não de acordo com os seus requisitos. Oráculo para teste de software é um mecanismo capaz de determinar se o resultado de um teste está ou não de acordo com os valores esperados. Freqüentemente, assume-se que o próprio projetista de teste é o responsável por esta tarefa. A automatização da atividade dos oráculos deu origem a oráculos automáticos, os quais são capazes de determinar o bom ou mau funcionamento do software a partir de uma fonte de informação confiável. Ao longo dos anos, a especificação formal vêm sendo largamente utilizada como fonte de informação para oráculos automáticos. Diversas estratégias vêm propondo geradores de oráculos baseados em especificações formais. Dentre as características marcantes dessas estratégias, cita-se aquelas que são aplicáveis a implementações derivadas a partir da estrutura da especificação e aquelas que geram oráculos a partir de técnicas específicas de seleção de casos. Essas características, entretanto, limitam a aplicação abrangente dos oráculos por restringi-los tanto a implementações derivadas diretamente de especificações como ao uso de técnicas específicas de seleção de casos de teste. Este trabalho apresenta um estudo sobre os geradores de oráculos para teste de software, identifica aspectos fundamentais que regem seu processo de construção e propõe uma estratégia que permite a geração de oráculos semi-automaticamente, mesmo para implementações não derivadas diretamente da estrutura da especificação. A estratégia proposta é, também, aplicável aos casos de teste derivados de qualquer técnica de seleção de casos de teste.

ProTool : uma ferramenta de prototipação de software para o ambiente PROSOFT

Dentre as principais áreas que constituem a Ciência da Computação, uma das que mais influenciam o mundo atual é a Engenharia de Software, envolvida nos aspectos científicos e tecnológicos do desenvolvimento de software. No desenvolvimento de software, a fase de especificação dos requisitos é uma das mais importantes, visto que erros não detectados nesta são propagados para as fases posteriores. Quanto mais avançado estiver o desenvolvimento, mais caro custa reparar um erro introduzido nas fases iniciais, pois isto envolve reconsiderar vários estágios do desenvolvimento. A prototipação permite que os requisitos do software sejam validados logo no início do desenvolvimento, evitando assim a propagação de erros. Paralelamente, a utilização de métodos formais visa revelar inconsistências, ambigüidades e falhas na especificação do software, que podem caso contrário, não serem detectadas. Usar a prototipação de software juntamente com uma notação formal enfatiza a especificação do problema e expõe o usuário a um sistema “operante” o mais rápido possível, de modo que usuários e desenvolvedores possam executar e validar as especificações dos requisitos funcionais. O objetivo principal deste trabalho é instanciar uma técnica da área de Prototipação de Software que capacite o engenheiro de software gerar automaticamente protótipos executáveis a partir de especificações formais de tipos abstratos de dados, na notação PROSOFT-algébrico, visando a validação dos requisitos funcionais logo no início do desenvolvimento do software. Para tanto foi proposto um mapeamento da linguagem PROSOFT-algébrico para OBJ. Como OBJ possui um eficiente sistema de reescrita de termos implementado, a utilização deste propicia a prototipação de tipos abstratos de dados, especificados em PROSOFT-algébrico. Os componentes envolvidos na definição deste trabalho, assim como o mapeamento entre as linguagens, foram especificados algebricamente e implementados no ambiente de desenvolvimento de software PROSOFT. A implementação serviu para validar o mapeamento proposto através de dois estudos de caso. Por fim, são apresentadas as conclusões alcançadas e as atividades adicionais vislumbradas a partir do trabalho proposto.

JCircus 2.0: Uma extensão da ferramenta de tradução de Circus para Java

This dissertation aims at extending the JCircus tool, a translator of formal specifications into code that receives a Circus specification as input, and translates the specification into Java code. Circus is a formal language whose syntax is based on Z s and CSP s syntax. JCircus generated code uses JCSP, which is a Java API that implements CSP primitives. As JCSP does not implement all CSP s primitives, the translation strategy from Circus to Java is not trivial. Some CSP primitives, like parallelism, external choice, communication and multi-synchronization are partially implemented. As an aditional scope, this dissertation will also develop a tool for testing JCSP programs, called JCSPUnit, which will also be included in JCircus new version. The extended version of JCircus will be called JCircus 2.0.

Os Pontos de Cultura como espaços não-formais de ensino: Práticas educativas na Baixada Fluminense.

A presente pesquisa consiste em um panorama das práticas educativas desenvolvidas pelas ONGs atuantes como Pontos de Cultura situadas na região da Baixada Fluminense. Este trabalho tem como objetivo geral analisar as ações desenvolvidas pelas ONGs contempladas como pontos de cultura na região da Baixada Fluminense de acordo com os seguintes objetivos específicos: identificar aquelas ações que podem ser consideradas de caráter educativo não-formal e as relações entre estas ações ao conceito de cultura política. A partir da discussão dos conceitos de Cultura apresentados por Marilena Chauí, do histórico das políticas culturais no Brasil, por Antonio Albino Canelas Rubim e das definições que originaram o programa fruto de uma política pública recente no Brasil, estas ações são entendidas dentro da categoria não-formal. Assim sendo, há a discussão do papel da educação não-formal nestes processos através do desenvolvimento dos conceitos por autores como Maria da Glória Gohn, José Carlos Libâneo e Jaume Trilla, uma descrição da região e a análise de dados oriunda das respostas obtidas através de duas entrevistas e dez formulários respondidos pelos gestores responsáveis pelas organizações em 2014. Os resultados encontrados indicaram que o Programa Cultura Viva atua como uma espécie de preenchimento das lacunas apresentadas por Gohn no que se refere à educação não-formal e de que embora as organizações possuam campos de atuação bem heterogêneos, as práticas educativas realizadas possuem em comum a abordagem da cultura como direito humano e que estas podem ser uma mola propulsora para a construção de uma nova cultura política.

Serviços de georreferenciamento e levantamento do uso da terra dos imóveis rurais da Embrapa: especificações técnicas dos produtos esperados.

Especificações técnicas para a elaboração do banco de dados espacializados das unidades da Embrapa; Layers do BD espacial; Recomendações na vetorização/edição de feições; Uso e cobertura da terra; Restrições legais de uso; Regras para APPs; Regras para Reserva Legal (RL); Definição de APP e Reserva Legal no SIG.

CARTOGRAFIA DAS APRENDIZAGENS FORMAIS PARA ADULTOSNA CIDADE DE ESTREMOZ: O PERÍODO 2000-2005

No âmbito do projeto de investigação As Novas Núpcias da Qualificação noAlentejo promovido pelo Centro de Investigação em Educação e Psicologia daUniversidade de Évora, e, considerando a questão da educação e formação de adultosem Portugal, foi efetuado um trabalho de investigação centrado na localidade deEstremoz, decorrente do trabalho final do segundo ciclo de estudos em Ciências daEducação na vertente de Educação Comunitária.

As aprendizagens não formais e informais no ingresso à Escola Secundária Padre António Macedo: possíveis parcerias com outras instituições de Vila Nova de Santo André

Esta investigação teve como principal objectivo avaliar da presença dos contextos institucionais não formais e informais no conjunto das aprendizagens reveladas pelos estudantes que ingressaram, na Escola Secundária Padre António Macedo, no ano lectivo 2009-2010, e averiguar qual o contributo das instituições locais no seu percurso de aprendizagem. A abordagem metodológica assentou num dispositivo de matriz quantitativa, com o recurso ao inquérito por questionário a uma amostra de alunos. Observámos um potencial educativo na cidade proporcionado por instituições, onde se destacaram amigos, familiares e clubes desportivos, procurados pelos jovens para satisfazer a sua necessidade de conhecimento e ocupar tempos livres. Sendo as áreas com mais episódios de aprendizagens, extra escolares: saúde, cidadania, desporto e artes, os jovens reconheceramse detentores de conhecimentos propiciados pela comunidade e instituições locais; ABSTRACT: This research had, as main aim, to assess the presence of formal and informal institutional contexts in all the learnings revealed by the students who enrolled Escola Secundária Padre António Macedo in the year 2009-2010, and also to determine what contribution local institutions had in their learning. The methodological approach was based on a quantitative matrix device, by applying a questionnaire survey to a sample of students. We saw an educational potential offered by institutions in the city, where the highlights were friends, family and sports clubs, popular among young people to satisfy their need for knowledge and to occupy their free time. The areas with more episodes of extra school learning were: health, citizenship, sport and arts. Young people recognized themselves in possession of knowledge provided by the community and local institutions.

Cartografia das aprendizagens formais para adultos na cidade de Estremoz: o período 2000-2005

O presente trabalho centra-se no levantamento das entidades promotoras de certificação formal, académica ou profissional, na cidade de Estremoz, direcionadas a adultos, no respeitante ao ensino não superior. Assumindo como ponto de partida a identificação desta oferta, pretende-se delinear um desenho cartográfico que permita conhecer e caracterizar a oferta de qualificação existente entre 2000/2005. Pretende-se compreender como esta contribuiu para a qualificação do público adulto, e, perceber, se foi ao encontro das necessidades socioeconómicas desta cidade, tentando compreender qual o seu impacto no que concerne ao desenvolvimento social e humano. Identificadas as entidades existentes, sustentada numa abordagem quantitativa, foram aplicados dois questionários visando caracterizar a educação formal, e, qual o seu contributo para o desenvolvimento deste público específico tendo-se verificado alguma preocupação em responder às necessidades sociais identificadas. Considera-se ainda a existência de um aumento na oferta formativa ao longo do tempo, associado à melhoria do desempenho profissional em que se estabelece uma relação entre empregabilidade e qualificação juntamente com a preocupação de promover a formação holística do cidadão; ABSTRACT:This paper focuses on the survey of promoters of formal certification, academic or professional, in Estremoz, aimed at adults, with respect to non-higher education. Taking as its starting point the identification of this offering, it is intend to outline a cartographic design to ascertain and characterize the range of qualifications between 2000/2005. The objective is to understand how this contributed to the qualification of the adult public, and notice if it was according the socioeconomic needs of the city, trying to understand its impact regarding social and human development. Identified existing entities, sustained in a quantitative methodology, two questionnaires were applied to characterize the formal education, what their contribution to the development of this specific audience and there has been some concern in responding to social needs identified. It is further considered that there is an increase in training provision over time associated with the improvement of professional performance which establishes a relationship between employability and qualification concerning the promotion of holistic formation of the citizen.

Inclusão escolar de crianças e jovens de comunidades ciganas : práticas pedagógicas formais e não-formais no âmbito do programa Escolhas

Relatório de estágio de mestrado, Ciências da Educação (Educação Intercultural), Universidade de Lisboa, Instituto de Educação, 2011

Práticas organizacionais formais utilizadas para a aprendizagem com acidentes de trabalho

O SHO 2010, Colóquio Internacional de Segurança e Higiene Ocupaciona