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