Sistema de traducción automática para lenguajes de verificación formal: TPTP a PVS (FirsT2PVS)

Abstract

[Resumen]: La verificación formal es una técnica empleada para demostrar matemáticamente la corrección de sistemas, especialmente en contextos donde la fiabilidad y la seguridad son críticas, como el software aeroespacial, médico o de control industrial. A diferencia de las pruebas tradicionales, que validan únicamente casos concretos, la verificación formal garantiza que ciertas propiedades lógicas se cumplen en todos los escenarios posibles de ejecución definidos por el modelo. TPTP (Thousands of Problems for Theorem Provers) es un lenguaje estándar en verificación formal, ampliamente utilizado en herramientas automáticas como VAMPIRE. Sin embargo, cuando estas herramientas no logran encontrar una prueba, el proceso se detiene sin ofrecer retroalimentación útil al usuario. Esto limita su aplicabilidad en dominios donde se requiere trazabilidad, entendimiento del proceso y validación manual. En contraste, PVS (Prototype Verification System) es un sistema de verificación asistida basado en lógica de orden superior (HOL), que permite al usuario participar activamente en la construcción de la prueba. Esta interacción ofrece mayor control, fiabilidad y transparencia, siendo especialmente útil cuando los métodos automáticos fallan o no son concluyentes. No obstante, las diferencias sintácticas y semánticas entre TPTP y PVS dificultan una traducción directa entre ambos lenguajes. Este trabajo propone el desarrollo de un sistema de traducción automática entre TPTP y PVS, centrado en la gramática THF por su expresividad y compatibilidad con el entorno PVS. El sistema combina técnicas clásicas de análisis léxico y sintáctico (mediante FLEX y BISON) con una fase intermedia de transformación semántica programada en Python. El resultado son especificaciones PVS válidas, trazables y anotadas, que permiten a un experto continuar el proceso de verificación sin requerir conocimientos previos del formato TPTP. Esta herramienta contribuye a la interoperabilidad entre entornos de demostración automática y asistida, ampliando el alcance práctico de la verificación formal.

[Abstract]: Formal verification is a technique used to mathematically prove the correctness of systems, particularly in domains where reliability and safety are critical, such as aerospace, medical, or control software. Unlike traditional testing, which only validates specific cases, formal verification ensures that certain properties hold in all possible execution scenarios defined by the model. TPTP (Thousands of Problems for Theorem Provers) is a standard language in formal verification, widely used by automated tools such as VAMPIRE. However, when these tools fail to find a proof, the process halts without offering useful feedback to the user. This limitation reduces their applicability in contexts that demand traceability, human interpretability, and manual verification. In contrast, PVS (Prototype Verification System) is an interactive verification environment based on higher-order logic (HOL), allowing the user to guide the proof process manually. This interaction enables greater control, transparency, and reliability, especially in situations where automatic provers fail or are inconclusive. Nevertheless, the syntactic and semantic differences between TPTP and PVS make a direct translation between them non-trivial. This project proposes the development of an automatic translation system from TPTP to PVS, focusing on the THF grammar due to its expressiveness and compatibility with the PVS environment. The system integrates classical structured language processing tools (FLEX, BISON) with an intermediate semantic transformation phase implemented in Python. The output consists of valid, traceable and annotated PVS specifications, enabling domain experts to continue the verification process without prior knowledge of TPTP. This tool enhances interoperability between automated and interactive verification environments, expanding the practical reach of formal verification.