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

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

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

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

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

Análisis económico de tres fincas de producción bovina de doble propósito explotadas de forma intensiva y extensiva durante el período 1992-1993

El objetivo principal del estudio fue conocer el comportamiento económico de tres fincas ganaderas de Doble Propósito; dos de ellas, ubicadas en el municipio de "Muy Muy" y explotadas de forma extensiva (fincas 1 y 2) y una tercera en el municipio de Tipitapa explotada de forma intensiva (3). La. base principal de este trabajo la constituyó la información proporcionada por loa productores, la que fue recolectada a través de un diagnóstico estático y un dinámico por el periodo de un año, la mayor parte de esta era de carácter económico, dándole prioridad a los gastos e ingresos incurridos en el periodo, además, se consideró algunas actividades de manejo practicado en ella. Se determinaron algunos índices productivos, la inversión inicial en medios fijos, los gastos por componentes, los ingresos y la rentabilidad entre otras. Los resultados indican que las fincas ubicadas en la zona de Tipitapa presentan ventajas comparativas en cuanto a la calidad de los suelos, facilidad de tecnificación, acceso al mercado, adquisición de insumos a más bajos precios Etc., dentro de las fincas evaluadas la tierra represento la mayor inversión de capital en medios fijos (53.58%), para las fincas de "Muy Muy" y 38% para la finca tres. Los mayores gastos correspondieron al componente mano de obra en las tres fincas, mientras que lo efectuado en alimentación en la finca uno y dos (10%) reflejan la baja suplementación en relación a la finca tres (40%) el que constituyó en esta un gasto constante. Respecto a los costos fijos y variables, la finca uno fue la que presentó los costos fijos más altos (76.29%); y la finca tres los costos variables (39.50%). El costo de producción de un litro de leche resultó superior al precio de venta del mismo en las tres fincas, al considerar dentro de los costos el interés de capital (Método A), el precio de venta fue C$1.25, C$1.15 y C$1,50 y el costo de producción de C$1.44, C$1.16 y C$1. 72. Al excluir dicho interés (Método B) el costo de producción fue de C$1.09, C$0.86 y C$1.42. Los mayores ingresos fueron aportados por el subsistema leche en las tres fincas, por concepto de venta de leche fluida y animales propios de esta actividad (85.40%, 98.12% y 67.24%). Al establecer relación entre los ingresos totales, costos totales y la inversión se encontró que las fincas 1 y 3 operaron con pérdidas determinándose entonces que las actividades no fueron rentables (-7.283%) y (-12.663%) durante este período, mientras que la finca 2 presentó una rentabilidad de (4.4%). Se identificaron algunas limitantes que al final repercuten en la actividad económica de las fincas sobresaliendo entre otros: Los bajos precios por la venta de los productos, los altos costos de los insumos, falta de conservación de pastos en la época seca, asistencia técnica irregular, la no utilización de registros, entre otras. Sólo con el incremento del volumen de la producción y superando la mayoría de las limitantes es que se logrará que las fincas amplíen sus beneficios, cubran sus costos y logren operar sin pérdidas.

La musica comu recursu didautico nel deprendimientu del asturianu na Educacion Primaria. 'La música como recurso didáctico en la enseñanza del asturiano en la Educación Primaria'.

Sugerir de forma orientativa dos métodos para crear canciones en asturiano, mostrando algunas posibilidades de trabajo que éstas pueden ofrecer como recurso didáctico para enseñar la lengua asturiana en un marco de interdisciplinariedad y siguiendo un modelo de escuela activa. La creación de canciones en lengua asturiana como medio para alcanzar objetivos lingüísticos. Expone su teoría de que en Educación Primaria la interdisciplinariedad es fundamental. Desde este punto de vista, explica el porqué considera que la música puede ser un elemento muy importante no sólo para utilizarla como recurso didáctico sino también como elemento motivador. Todo esto lo justifica por medio de un ejemplo de cómo a partir de una canción popular asturiana se pueden sacar elementos de enseñanza no sólo para el área de Lenguaje, sino también para la de Plástica, Matemáticas y Ciencias Naturales. Por otro lado, propone dos métodos para que los niños creen sus propias canciones. Para concluir presenta 8 fichas como modelos prácticos orientativos. Bibliografía especializada en Música, lengua asturiana y didáctica de la lengua. Utiliza la explicación teórica de los métodos, acompañada de ejemplos donde incluye letras de canciones, pentagramas, dibujos y gráficos. La enseñanza del asturiano en Educación Primaria debe contar con una estrategia didáctica que consiga en los niños un mayor conocimiento y empleo de la lengua. Desde este punto de vista, el tratamiento de textos musicales puede ser un recurso muy interesante ya que comprende una serie de aspectos que ayudan al aprendizaje de la lengua, pueden servir como argumento introductorio para cualquier tema de estudio interdisciplinar y además sirven como elemento motivador. Pero no debe limitarse al niño a aprender canciones populares de la cultura tradicional, sino que se le debe animar a que haga sus propias canciones. Para ello propone dos métodos: método a) donde primero se crearía la melodía (los niños individualmente van probando sonidos hasta que uno encuentra una serie de 4 sonidos que sea aceptado por los demás, de igual forma se proponen los 4 siguientes y así sucesivamente hasta completarla), y después se crearía el texto (al igual que antes, los niños van proponiendo fragmentos de frases hasta rellenar la melodía); y un método b) que se basa en la misma forma de trabajo que el anterior pero que consta de tres fases (creación de un esquema rítmico, creación de una melodía y creación de una letra). La estructura de las fichas que presenta como muestra de trabajo es la siguiente: esquema musical, esquema de entonación, partitura, letra de la canción, trabajo lingüístico y trabajo musical a partir de la canción.

Función facilitadora de la imagen en los procesos de aprendizaje.

Comprobar empíricamente la función de los medios audiovisuales en los procesos de aprendizaje, tanto en los aspectos informativos como en los vinculados a la adquisición de actitudes. Formada por alumnos de FP de primer grado, pertenecientes al Centro Profesional Madre Sacramento de Torrent, Valencia, divididos en cuatro grupos: grupo A, 30 alumnos, medio aplicado el vídeo; grupo B, 28 alumnos, medio las diapositivas, explicación del profesor; grupo C, 25 alumnos, medio la explicación magistral; grupo D, 29 alumnos, medio la información verbo-icónica. Elaboración de distintos soportes informativos sobre un tema concreto de aprendizaje relacionado con el entorno del alumno: el territorio de la comarca de L'Horta sud. Se toman como variables dependientes los propios soportes: vídeo, diapositivas-explicación profesor, clase magistral e información verbo-icónica, y como variables independientes las situaciones del pretest y posttest. Soportes: diaporama transformado en vídeo-programa, un material verboicónico, un guión oral con diapositivas y un guión estríctamente oral. Prueba de control de 24 ítems. Test de Sheffe. Análisis de varianza y covarianza para determinar la significatividad de diferencias entre grupos. Comparación entre grupos. Representaciones gráficas. Con el análisis de varianza se comprueba que los cuatro grupos no son homogéneos de partida. Mediante el método A, vídeo, se pasa de una media aceptable en el pretest a una media baja de aprendizaje; con el método B, diapositivas clase, surge la media de rendimiento más alta de los cuatro grupos, partiendo todos ellos de una media baja en el pretest. Con el método C, explicación oral, aunque se partió de unos conocimientos previos muy altos, el rendimiento no es el esperado, siendo su media de diferencias muy baja. Con el método D, texto verboicónico, se parte de la media inicial más baja y se obtiene el rendimiento menor de todos aunque no significativo con relación al resto de grupos. Los medios audiovisuales y verboicónicos facilitan el aprendizaje tanto en los procesos informativos como en los actitudinales. La experiencia metodológica que mejores efectos produce es la explicación del profesor con apoyo de imágenes. Las mayores diferencias se producen entre la explicación con diapositivas y la explicación clásica oral. Se advierte la importancia del profesor en la aplicación de los medios. El vídeo, aunque no es el método idóneo en el rendimiento general, ayuda a despertar actitudes y conductas formales.

El Dibujo en primero de BUP : hacia un lenguaje de la imagen.

Plantear una serie de puntos claves a la hora de hacer una planificación pedagógica de esta disciplina, el Dibujo, tan amplia que transciende a los límites de la pura disciplina. Didáctica del Dibujo. Investigación teórica fundada sobre la base del análisis bibliométrico y de los planes de educación vigentes. Utiliza un método descriptivo para desarrollar los elementos necesarios para una planificación pedagógica de la Educación Artística, que tenga en cuenta que ésta es fundamental en el desarrollo de la personalidad del niño en sus aspectos de creatividad y sensibilidad. El análisis es comparativo cuando se contrastan los planes del Sistema Educativo con la realidad pedagógica actual centrada en la creatividad y en el arte como vehículo de ésta. Partes del estudio: a) análisis de los elementos del hecho educativo: el maestro, el alumno, el método; b) desarrollo y metodología; c) objetivos del Dibujo en primero de BUP; d) lenguaje y lenguaje plástico, características generales del lenguaje humano, características específicas del lenguaje plástico; e) introducir al alumno en el conocimiento del lenguaje de la imagen. Bibliografía. Análisis teórico. El acto de dibujar existe potencialmente en todo ser humano. Si por formación-educación entendemos el óptimo desarrollo de las facultades en potencia del ser humano, hay que admitir que nuestros Sistemas Educativos no cumplen este cometido puesto que no desarrollaron la facultad de dibujar: una desacertada orientación en la planificación de los programas margina las Enseñanzas Artísticas. Los actuales conceptos sobre la enseñanza y la formación integral del individuo tienden a situar en un plano relevante la educación a través del arte, ya que consideran las Enseñanzas Artísticas fundamentalmente formativas para el desarrollo de la personalidad del niño y, en ellas, el dibujo es el principal potenciador de la creatividad y sensibilidad. El Dibujo como educación o actividad artística debe atender en primer lugar la libre expresión del niño y proporcionarle dentro de lo posible, las destrezas constructivas y técnicas adecuadas para estimular su creatividad. Pero además, como acto de cultura, la enseñanza del Dibujo debe proporcionar al alumno la suficiente información que le permita relacionar con claridad su educación del lenguaje plástico con las demás áreas. Y de modo especial, que la expresión plástica le introduzca en la comprensión de las obras artísticas de todos los tiempos.

Comparação de dois métodos de quantificação de Salmonella sp. em embutidos suínos.

A segurança dos alimentos é uma preocupação mundial e um fator importante na comercialização de produtos de origem animal. A presença de Salmonella sp. em suínos ao abate e em produtos do tipo frescal podem representar um risco para a saúde do consumidor. A análise de risco prevê a avaliação de diferentes fatores, entre eles a quantificação do microrganismo presente no alimento. A partir disso, a contribuição do presente estudo foi buscar estabelecer um método confiável de quantificação de Salmonella sp. em produtos suínos, uma vez que uma das etapas da análise de risco prevê a quantificação do perigo. No caso de Salmonella sp., a técnica da estimativa do Número Mais Provável (NMP) tem sido adotada. Em uma primeira fase desse trabalho, amostras foram quantificadas, individualmente, com três amostras de Salmonella Typhimurium (ATTCC15290 e 2 amostras de suínos) em três diferentes contagens, 101, 102 e 103 UFC. Para o método A, as amostras quantificadas foram adicionadas a 225 mL de água peptonada tamponada, sendo, posteriormente, fracionadas em 3 alíquotas de 50mL, 5mL e 0,5mL. Para o método B, a amostra fortificada foi diluída em água peptonada tamponada até 10-3, sempre em triplicata. Na segunda fase, foram testadas amostras naturalmente contaminadas, utilizando as mesmas metodologias usadas na primeira fase. Todas as alíquotas de ambos métodos foram incubadas a 370C por 18 horas. Após, cada alíquota foi semeada em caldo Rappaport-Vassiliadis (RV) e incubadas à 420C por 24 h e após, em àgar Xylose-Lysine-Tergitol 4 (XLT4) à 370C por 48 h. Colônias suspeitas foram confirmadas por testes bioquímicos. O número de placas positivas para Salmonella sp. foi utilizado para o cálculo do Número Mais Provável, utilizando tabela apropriada. Na segunda fase, os dois métodos foram avaliados em 20 amostras naturalmente contaminadas, mantidas congeladas por até 115 dias. Em 45 ensaios conduzidos, para cada método, em amostras de lingüiça de carne suína contaminadas artificialmente, 38 do método A e 41 do método B resultaram em NMP (95% de intervalo de confiança) concordante com número de UFC de Salmonella inoculado. A maioria das amostras naturalmente contaminada de massa de embutido apresentaram contagens <10NMP/g. A variabilidade encontrada entre os valores de NMP médio foi bastante elevada, tanto entre os métodos como entre repetições de um mesmo método. Isto reflete uma das limitações do método de NMP para estimar a contagem de microrganismos e deverá ser considerada quando o método for aplicado em alimentos naturalmente contaminados e quando aplicado em um estudo de análise de risco. Uma vez que o método B foi o que demonstrou valores médios de NMP mais próximos das quantidades inoculadas, sugere-se que este seja adotado em estudos futuros de quantificação de Salmonella sp. em produtos de origem suína.

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.

Estudos por imagem e físico dos membros pélvicos de pacas (Cuniculus paca) criadas em cativeiro

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Mediação do processo ensino-aprendizagem com o jogo de empresas mercado virtual: uma pesquisa de opinião

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)