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

Aplicação do método B ao projeto formal de software embarcado

This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry

A integração do tutorial interativo TryLogic via IMS Learning Tools Interoperability: construindo uma infraestrutura para o ensino de Lógica através de estratégias de demonstração e refutação

Logic courses represent a pedagogical challenge and the recorded number of cases of failures and of discontinuity in them is often high. Amont other difficulties, students face a cognitive overload to understand logical concepts in a relevant way. On that track, computational tools for learning are resources that help both in alleviating the cognitive overload scenarios and in allowing for the practical experimenting with theoretical concepts. The present study proposes an interactive tutorial, namely the TryLogic, aimed at teaching to solve logical conjectures either by proofs or refutations. The tool was developed from the architecture of the tool TryOcaml, through support of the communication of the web interface ProofWeb in accessing the proof assistant Coq. The goals of TryLogic are: (1) presenting a set of lessons for applying heuristic strategies in solving problems set in Propositional Logic; (2) stepwise organizing the exposition of concepts related to Natural Deduction and to Propositional Semantics in sequential steps; (3) providing interactive tasks to the students. The present study also aims at: presenting our implementation of a formal system for refutation; describing the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification; presenting the Conjecture Generator that works for the tasks involving proving and refuting; and, finally to evaluate the learning experience of Logic students through the application of the conjecture solving task associated to the use of the TryLogic

Gênero, sexualidade e educação formal no Brasil: uma análise preliminar da produção acadêmica entre 1990 e 2006

Cet article présente les résultats de la recherche Démocratisation de la connaissance: recherche de pointe sur le genre et l'éducation formelle comme soutien pour formuler des agendas et des actions de politiques gouvernementales et non gouvernementales. Développée entre 2006 et 2007, elle visait à met re à jour, systématiser et diffuser la connaissance accumulée dans la production universitaire brésilienne sur les liens entre l'éducation formelle et les thématiques du genre, des femmes et/ou de la sexualité. Une banque de données contenant le titre et le résumé de 1 213 dissertations, thèses et articles a été constituée. Nous soulignons autant les défis théoriques, concernant une meilleure compréhension des concepts étudiés par cete enquête, que les défis méthodologique, comme la définition des descripteurs et des sources devant être examinées. Sa conclusion présente des tableaux et graphiques qui tracent un portrait initial des documents disponibles dans la base de données et indiquent que ces thématiques ont été l'objet d'un intérêt croissant sur la période étudiée.

Medidas de desempenho escolar: avaliação formal e opinião de professores

O objetivo deste estudo foi comparar o desempenho de escolares em relação à avaliação formal e a opinião de professores. Participaram 164 escolares de ensino fundamental de cidade do interior paulista, sendo 81 do sexo masculino e 83 do sexo feminino. Foi utilizado o Teste de Desempenho Escolar e foram definidos 2 grupos, segundo a opinião da professora quanto ao desempenho normal e abaixo da média. Os resultados revelaram diferença significativa indicando que o menor desempenho foi verificado para o sexo masculino e para a quarta série. As médias do grupo definido pela professora com desempenho inferior foram abaixo do esperado e diferiram significativamente. A opinião da professora neste estudo foi fundamental para a identificação dos problemas relacionados à escolaridade.

Conteúdos lúdicos, expressivos e artísticos na educação formal

A prática de atividades lúdicas ou o incentivo ao fluir expressivo e artístico são propostas que permeiam a Educação, desde a Antiguidade Clássica. Atualmente, a necessidade premente de atentar para a inclusão contextualizada dessas práticas, vem sendo convalidada pelas diretrizes propostas pelos Parâmetros Curriculares tanto das disciplinas de Educação Física, como da Educação Artística. Entretanto esse espaço, ainda sutil, merece enfoque mais incisivo, por meio de estudos mais aprofundados acompanhados de práticas direcionadas que convalidem sua relevância. Assim, este estudo, de natureza qualitativa, objetivou investigar se essas variáveis estão disponíveis dentro dos conteúdos disseminados pelos professores e se possuem um espaço destinado ou não dentro da Educação formal. Para tanto, foi realizado um estudo exploratório com trinta professores voluntários, de ambos os sexos, pesquisados in loco, com consentimento livre e esclarecido, das disciplinas de Educação Física e Artística, utilizando como instrumento, para a coleta de dados, um questionário com perguntas mistas. Os dados foram analisados descritivamente, indicando que é possível notar a presença do lúdico e da arte, em ambas as disciplinas; mediando os processos de aprendizagem. Além disso, que os professores utilizam amplamente desses recursos, no entanto, nem sempre, de forma consciente e contextualizada, e que, apesar da implantação dos parâmetros curriculares desde 1998, esse espaço ainda não está consolidado.

Relación de dependencia del trabajo formal y brechas de protección social en América Latina y el Caribe

Incluye Bibliografía

Relación de dependencia del trabajo formal y brechas de protección social en América Latina y el Caribe

Incluye Bibliografía

Programa de prevención de violencia a través de proyectos de resolución de conflictos y mediación de pares en escuelas con niños y jóvenes en riesgo y en grupos de educación no formal, San Carlos de Bariloche, Argentina

Incluye Bibliografía

Difusão do trabalho agrícola formal no Brasil e sua dinâmica multiescalar

This paper aims to analyze the geographical dynamics of work from the spread of formal employment in the agricultural sector in Northeast Brazil. In recent years the region has had highlighted a growing movement to produce fruit for export, resulting in the promotion of important sociospatial transformations arising from the formation of a capitalist labor market. Data about the increase in the number of formal jobs show the impact of fruit growing agribusiness in the establishment of a new social and territorial division of labor. However, our study draws attention to the existence of a framework dominated for the vulnerability of the labor market by the persistence of seasonality and precarious working conditions.

Programa de demografia formal

El proposito central del programa de demografia formal, es conocer las variables demograficas determinantes de la estructura y dinamica de la poblacion de cada pais. Su cumplimiento implica la elaboracion de proyecciones de poblacion a nivel regional y nacional, el desarrollo de metodos de encuestas demograficas y asesoria a los paises en su realizacion asi como prestar asistencia tecnica a paises y a otros programas y proyectos de CELADE. El documento incluye una lista del personal y un detalle de las actividades descritas.

Computational support for the process of software requirement specification

The software industry has become more and more concerned with the appropriate application of activities that composes requirement engineering as a way to improve the quality of its products. In order to support these activities, several computational tools have been available in the market, although it is still possible to find a lack of resources related to some activities. In this context, this paper proposes the inclusion of a module to aid in the requirements specification to a tool called Requirements Elicitation Support Tool. This module allows to specify requirements in accordance with IEEE 830 standard, thus contributing to the documentation of the requirements established for a software system, besides supporting the learning of concepts related to the requirements specification, which improves the skills of users of the tool. © 2012 IEEE.

Women's formal education: achievements and obstacles

Includes bibliography

La movilidad laboral en Argentina desde mediados del decenio de 1990: el difícil camino de regreso al empleo formal

Incluye Bibliografía

Labour mobility in Argentina since the mid-1990s: the hard road back to formal employment

Includes bibliography