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.

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

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

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

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.

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