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

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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Vanzetto, Hernán P.
Otros Autores: Merz, Stephan
Formato: bachelorThesis trabajo final de grado publishedVersion
Lenguaje:Español
Publicado: Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario 2014
Materias:
verificación formal
asistente de pruebas
TLA+
axiomas
aritmética de números enteros
Acceso en línea:http://hdl.handle.net/2133/3561
http://hdl.handle.net/2133/3561
Aporte de:
Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR) de Universidad Nacional de Rosario
id I15-R121-2133-3561
record_format dspace
institution Universidad Nacional de Rosario
institution_str I-15
repository_str R-121
collection Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR)
language Español
orig_language_str_mv spa
topic verificación formal
asistente de pruebas
TLA+
axiomas
aritmética de números enteros
spellingShingle verificación formal
asistente de pruebas
TLA+
axiomas
aritmética de números enteros
Vanzetto, Hernán P.
Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle
topic_facet verificación formal
asistente de pruebas
TLA+
axiomas
aritmética de números enteros
description 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.
author2 Merz, Stephan
author_facet Merz, Stephan
Vanzetto, Hernán P.
format bachelorThesis
trabajo final de grado
publishedVersion
author Vanzetto, Hernán P.
author_sort Vanzetto, Hernán P.
title Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle
title_short Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle
title_full Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle
title_fullStr Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle
title_full_unstemmed Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle
title_sort formalización de la aritmética de tla+ en el asistente de pruebas isabelle
publisher Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario
publishDate 2014
url http://hdl.handle.net/2133/3561
http://hdl.handle.net/2133/3561
work_keys_str_mv AT vanzettohernanp formalizaciondelaaritmeticadetlaenelasistentedepruebasisabelle
bdutipo_str Repositorios
_version_ 1764820412246523907

Ejemplares similares