Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle

DSpace/Manakin Repository

Show simple item record

dc.contributor.advisor Merz, Stephan
dc.contributor.author Vanzetto, Hernán P.
dc.date.accessioned 2014-10-08T13:28:56Z
dc.date.available 2014-10-08T13:28:56Z
dc.date.issued 2010-06-18
dc.identifier.uri http://hdl.handle.net/2133/3561
dc.description.abstract TLA+ es un lenguaje para especificar sistemas distribuidos y concurrentes. Está basado en una lógica clásica de primer orden no-tipada y en una variante de la teoría de conjuntos estándar ZF, más una pequeña parte de lógica temporal. Una versión extendida del lenguaje, llamada TLA+2, permite además escribir pruebas estructuradas jerárquicamente para verificar propiedades de las especificaciones. El Administrador de Pruebas TLAPM transforma las pruebas escritas en TLA+2 en una colección de obligaciones de prueba que son enviadas a uno o más demostradores secundarios para que sean verificadas. Estos producen trazas o scripts de las pruebas verificadas que luego deben certificarse en un entorno lógico como el asistente de pruebas genérico Isabelle. De esta forma, el núcleo del entorno lógico es el único componente confiable del sistema de pruebas de TLA+. El lenguaje TLA+ está siendo formalizado en Isabelle como una nueva lógica-objeto llamada Isabelle/TLA+. Hasta el momento incluye un subconjunto de la lógica de primer orden, teoría de conjuntos, funciones, puntos fijos y la construcción de números naturales, y se instanciaron los principales métodos de prueba semi-automáticos ya existentes en Isabelle.  El objetivo de este trabajo es extender Isabelle/TLA+ para dar soporte a la aritmética estándar de TLA+ sobre los números naturales y enteros. Esto implica definir axiomáticamente los operadores aritméticos y probar sus propiedades para aumentar el poder de razonamiento de los métodos de prueba automáticos, lo que permitirá al TLAPM certificar las pruebas de especificaciones que utilizan aritmética. es
dc.language.iso spa
dc.publisher Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario es
dc.rights openAccess es
dc.subject verificación formal es
dc.subject asistente de pruebas es
dc.subject TLA+ es
dc.subject axiomas es
dc.subject aritmética de números enteros es
dc.title Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle es
dc.type bachelorThesis
dc.type trabajo final de grado
dc.type publishedVersion
dc.description.peerreviewed Peer reviewed es


Files in this item

This item appears in the following Collection(s)

Show simple item record

My Account


Search DSpace


Browse