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

Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

Especificação do micronúcleo FreeRTOS utilizando o método B

This paper presents a contribution to the international Verified Software Repository effort through the formal specification of the microkernel FreeRTOS real-time system. Such specification was made in abstract level making use of the B method . For thus, properties of the microkernel were chosen and selected as specification requisites, which was constructed centered at the functionalities responsible for the utilization of these properties. This properties weres setting as specification requirements. The specification was constructed modeling the function of microkernel that implement this properties. This work intended to encourage the formal verification of FreeRTOS and also contribute to the formal creation of a microkernel real-time systems, based in FreeRTOS. Furthermore, this model brings a formal documentation point view of the microkernel, demonstrating features and how this internal states is changing. Finally, this work could be an example of specification of the actual system by the B method.

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

Um método para desenvolvimento de abordagens generativas com composição de linguagens específicas de domínio

The software systems development with domain-specific languages has become increasingly common. Domain-specific languages (DSLs) provide increased of the domain expressiveness, raising the abstraction level by facilitating the generation of models or low-level source code, thus increasing the productivity of systems development. Consequently, methods for the development of software product lines and software system families have also proposed the adoption of domain-specific languages. Recent studies have investigated the limitations of feature model expressiveness and proposing the use of DSLs as a complement or substitute for feature model. However, in complex projects, a single DSL is often insufficient to represent the different views and perspectives of development, being necessary to work with multiple DSLs. In order to address new challenges in this context, such as the management of consistency between DSLs, and the need to methods and tools that support the development with multiple DSLs, over the past years, several approaches have been proposed for the development of generative approaches. However, none of them considers matters relating to the composition of DSLs. Thus, with the aim to address this problem, the main objectives of this dissertation are: (i) to investigate the adoption of the integrated use of feature models and DSLs during the domain and application engineering of the development of generative approaches; (ii) to propose a method for the development of generative approaches with composition DSLs; and (iii) to investigate and evaluate the usage of modern technology based on models driven engineering to implement strategies of integration between feature models and composition of DSLs

Estudo mecânico da estabilidade dorsal da osteossíntese intramedular associada à fixação externa (método de Ulson)

OBJETIVO: Avaliar o método de Ulson de fixação intramedular associado à fixação externa variando a altura do travamento externo dos fios de Kirschner e sem fixação externa. MÉTODO: Foram utilizadas 18 tíbias de porcos, sendo realizada osteotomia transversal na região da tuberosidade e introduzidos dois fios de Kirschner intramedulares em cada peça, em três diferentes padrões de montagem: grupo I - travamento com minifixador externo com 3,0cm de altura; grupo II - travamento com 4,5cm de altura; grupo III: sem travamento externo. Realizaram-se ensaios mecânicos de cisalhamento, obtendo-se: carga máxima, limite de proporcionalidade e coeficiente de rigidez. RESULTADOS: Não foram encontradas diferenças significativas de carga máxima e limite de proporcionalidade entre os grupos; o grupo II apresentou maior coeficiente de rigidez. CONCLUSÃO: A altura do travamento dos fios de Kirschner no método de Ulson, dentro dos limites avaliados, não prejudicou a estabilidade do sistema de fixação da fratura.

Um método semi-automatizado para elicitação de requisitos de acessibilidade Web

In the context of Software Engineering, web accessibility is gaining more room, establishing itself as an important quality attribute. This fact is due to initiatives of institutions such as the W3C (World Wide Web Consortium) and the introduction of norms and laws such as Section 508 that underlie the importance of developing accessible Web sites and applications. Despite these improvements, the lack of web accessibility is still a persistent problem, and could be related to the moment or phase in which this requirement is solved within the development process. From the moment when Web accessibility is generally regarded as a programming problem or treated when the application is already developed entirely. Thus, consider accessibility already during activities of analysis and requirements specification shows itself a strategy to facilitate project progress, avoiding rework in advanced phases of software development because of possible errors, or omissions in the elicitation. The objective of this research is to develop a method and a tool to support requirements elicitation of web accessibility. The strategy for the requirements elicitation of this method is grounded by the Goal-Oriented approach NFR Framework and the use of catalogs NFRs, created based on the guidelines contained in WCAG 2.0 (Web Content Accessibility Guideline) proposed by W3C

Método e sociologia em Weber: alguns conceitos fundamentais

Os parâmetros de análise social fornecidos pelos fundamentos da obra weberiana apontam algumas determinações necessárias à análise de fenômenos sociais. Defendendo uma sociologia capaz de compreender os sentidos e conexões presentes nas ações sociais, Weber propõe uma concepção específica de método e de objeto na sociologia, que se assenta na explicação de ações sociais individuais, sob condições determinadas, e busca, ao mesmo tempo, explicitar as significações das instituições sociais, nas quais os indivíduos agem, como resultantes também da ação humana. A partir de tais idéias, o breve ensaio ora apresentado, propõe-se a debater alguns elementos trabalhados nos conceitos weberianos de método e sociologia

Síntese e caracterização de pós Ba(x)Sr(1-x)Co0,8Fe0,2O3- através do método de coprecipitação via oxalato

Ceramic powders based on oxides of perovskite-type structure is of fundamental interest nowadays, since they have important ionic-electronic conductivity in the use of materials with technological applications such as gas sensors, oxygen permeation membranes, catalysts and electrolytes for solid oxide fuel cells (SOFC). The main objective of the project is to develop nanostructured ceramic compounds quaternary-based oxide Barium (Br), Strontium (Sr), Cobalt (Co) and Iron (Fe). In this project were synthesized compounds BaxSr(1-x)Co0, 8Fe0,2O3- (x = 0.2, 0.5 and 0.8) through the oxalate co-precipitation method. The synthesized powders were characterized by thermogravimetric analysis and differential thermal analysis (TGADTA), X-ray diffraction (XRD) with the Rietveld refinement using the software MAUD and scanning electron microscopy (SEM). The results showed that the synthesis technique used was suitable for production of nanostructured ceramic solid solutions. The powders obtained had a crystalline phase with perovskite-type structure. The TGA-DTA results showed that the homogeneous phase of interest was obtained temperature above 1034°C. It was also observed that the heating rate of the calcination process did not affect the elimination of impurities present in the ceramic powder. The variation in the addition of barium dopant promoted changes in the average crystallite size in the nanometer range, the composition being BSCF(5582) obtained the lowest value (179.0nm). The results obtained by oxalate co-precipitation method were compared with those synthesis methods in solid state and EDTA-citrate method

Método de Projeções Ortogonais

The problem treated in this dissertation is to establish boundedness for the iterates of an iterative algorithm in 2, under some technical conditions. However, this paper uses non-trivial intuitive arguments and its proofs lack suficient rigor. In this dissertation we discuss and strengthen the results of this paper, in order to complete and simplify its proofs

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

Estudo de caso de dois acidentes do trabalho investigados com o método de árvore de causas

São apresentados dois acidentes do trabalho típicos, ocorridos em empresa de grande porte, investigados com o Método de Árvore de Causas ­ ADC, método que permite identificar o papel desempenhado por fatores gerenciais e de organização do trabalho no desencadeamento desses fenômenos. Os casos apresentados revelam a participação, na gênese dos acidentes, de fatores como designação temporária e improvisada de trabalhadores para funções e postos de trabalho, execução de tarefas deixadas à iniciativa e ao arbítrio dos trabalhadores, falta de ferramentas e de materiais apropriados à execução de tarefas e falhas na circulação de informações, entre outros. São também analisadas as indicações para o uso do método, suas potencialidades em termos de prevenção, bem como as implicações decorrentes de dificuldades de aplicação, de necessidades de treinamento e reciclagens e do dispêndio elevado de tempo para investigação de cada acidente.

Comparação entre método bioquímico e reação em cadeia de polimerase para identificação de Lactobacillus spp., isolados de aves

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

A refrigeração no diagnóstico de Salmonella spp. utilizando o método microbiológico tradicional e reação em cadeia da polimerase em carcaças de frango

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Influência do método de fenação e tempo de armazenamento sobre a composição bromatológica e ocorrência de fungos no feno de alfafa (Medicago sativa, L. cv. Flórida 77)

O experimento objetivou estudar a influência de 24 tratamentos resultantes do arranjo fatorial 6 x 4, referente a seis métodos de fenação e quatro tempos de armazenamento em delineamento inteiramente casualizado, com cinco repetições para análise bromatológica e quatro para determinação de fungos. Os métodos de fenação consistiram em: T1 - (sombra, E) secagem à sombra, a forrageira foi levada para o galpão imediatamente após o corte e mantida espalhada (E); T2 e T3 - o material permaneceu ao sol até perder 50% do peso e posteriormente foi seco à sombra, sendo o T2 espalhado (sol 50%, E) e o T3 amontoado - A (sol 50%, A); T4 e T5, consistiram do recolhimento da forragem para completar sua secagem à sombra, após viragem e perda de 60% de peso sob exposição ao sol, T4 espalhada (sol 60%, E), T5 amontoada (sol 60%, A) e o T6 perda de 80% do peso sob exposição ao sol e posteriormente amontoado à sombra (sol 80%, A). Os quatro tempos de armazenamento foram: 0, 15, 30 e 60 dias. Verificou-se que os fenos nos quais o material ficou mais tempo exposto ao sol apresentaram pior qualidade em termos de PB, FDN e FDA. A ocorrência de fungos foi maior no feno seco à sombra (T1) e naqueles em que a forragem foi amontoada, devido à ausência de aeração para retirada de umidade. O método mais adequado para a conservação da alfafa consistiu na exposição da forragem ao sol até a perda de 50% do peso da forragem original, com posterior secagem do material espalhado à sombra.