PolyVer: Un Enfoque Compositivo para el Modelado y Verificación de Sistemas Políglotas

Información Básica

• ID del Artículo: 2503.03207
• Título: PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
• Autores: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
• Clasificación: cs.PL (Lenguajes de Programación)
• Fecha de Publicación/Conferencia: Formal Methods in Computer-Aided Design 2025
• Enlace del Artículo: https://arxiv.org/abs/2503.03207

Resumen

Los sistemas de software políglotas (polyglot systems) están compuestos por programas implementados en múltiples lenguajes de programación, pero los verificadores de programas existentes generalmente están diseñados solo para un único lenguaje. Para verificar sistemas políglotas, típicamente se requiere traducirlos a un lenguaje de verificación común o representación formal. Este artículo propone PolyVer, un método alternativo que realiza verificación poliglota directamente mediante técnicas de abstracción, razonamiento compositivo y síntesis. PolyVer construye sistemas políglotas como modelos formales de sistemas de transiciones, donde las funciones de actualización relacionadas con transiciones se implementan en lenguajes objetivo (como C o Rust). Para ejecutar la verificación, PolyVer conecta verificadores de modelos de sistemas de transiciones con verificadores específicos del lenguaje a través de contratos de precondición/postcondición de funciones de actualización. Estos contratos se generan automáticamente mediante oráculos de síntesis basados en síntesis guiada por sintaxis o modelos de lenguaje grande, y se verifican mediante verificadores específicos del lenguaje.

Contexto de Investigación y Motivación

Definición del Problema

Los sistemas de software modernos adoptan cada vez más arquitecturas políglotas, como marcos ROS2 y Lingua Franca que permiten a los desarrolladores elegir el lenguaje de programación más apropiado para cada componente. Sin embargo, esta flexibilidad introduce desafíos de verificación:

1. Diferencias de Semántica de Lenguajes: Diferentes lenguajes de programación poseen sintaxis y semántica distintas. Por ejemplo, la función saturating_add de Rust se satura al valor máximo en caso de desbordamiento, mientras que la suma en C puede envolver.
2. Limitaciones de Verificadores Existentes: La mayoría de verificadores de programas (como CBMC para C, Kani para Rust) están diseñados específicamente para un único lenguaje y no pueden manejar directamente sistemas políglotas.
3. Complejidad de Traducción: Traducir un sistema poliglota completo a un único lenguaje de verificación requiere soportar la sintaxis y semántica completa de todos los lenguajes, lo cual es prohibitivo para lenguajes modernos.

Importancia de la Investigación

La complejidad creciente de los sistemas políglotas aumenta el riesgo de defectos de software. En dominios críticos para la seguridad (como conducción autónoma y aeroespacial), se requieren las garantías fuertes proporcionadas por verificación formal, en lugar de depender únicamente de métodos incompletos como pruebas.

Limitaciones de Métodos Existentes

• Métodos de Traducción Monolítica: Requieren desarrollar infraestructura de compilador completa para cada lenguaje
• Dificultad en Preservación de Semántica: Es difícil capturar fielmente todas las construcciones específicas del lenguaje fuente en el lenguaje de verificación objetivo
• Problemas de Escalabilidad: Los problemas de verificación generados pueden volverse excesivamente grandes

Contribuciones Principales

1. Formalización del Problema de Verificación Poliglota: Primera formalización sistemática del problema de verificación poliglota y propuesta de una solución compositiva que integra múltiples verificadores específicos del lenguaje.
2. Síntesis Automática de Contratos: Propuesta de un método automático para síntesis y refinamiento de contratos de precondición/postcondición utilizando lenguaje intermedio y ciclos CEGIS-CEGAR, soportando síntesis guiada por sintaxis y modelos de lenguaje grande como oráculos de síntesis.
3. Implementación de Herramienta: Implementación de la herramienta PolyVer basada en UCLID5, soportando C y Rust a través de verificadores CBMC y Kani, demostrando que los oráculos de síntesis basados en LLM superan a los métodos de síntesis puramente simbólicos.
4. Estudios de Caso y Evaluación: Desarrollo de un verificador para el lenguaje de coordinación Lingua Franca, verificación de sistemas políglotas que contienen procesos en C y Rust, así como fragmentos de C que trabajos anteriores no podían soportar.

Explicación Detallada del Método

Definición de la Tarea

Entrada: Modelo poliglota M = (Q,V,I₀,T,F) y propiedad del sistema φ Salida: Resultado de verificación (aprobado/fallido) y posible traza de contraejemplo Objetivo: Determinar si M ⊨ φ se cumple

Donde:

• Q: Conjunto de modos
• V: Conjunto de variables tipificadas
• I₀: Conjunto de estados iniciales
• T: Conjunto de transiciones de modos
• F: Conjunto de procedimientos

Arquitectura del Modelo

1. Máquina de Estados Extendida (ESM)

PolyVer modela sistemas políglotas como máquinas de estados extendidas, donde:

• Los estados se componen de modos y asignaciones de variables
• Las transiciones se asocian con condiciones de guardia y relaciones de actualización
• Las relaciones de actualización se especializan en secuencias de llamadas a procedimientos

2. Lenguaje de Contrato Intermedio L*

La innovación clave es la introducción del lenguaje intermedio L* como "pegamento" entre diferentes lenguajes:

• Los contratos se escriben en L*
• Se transforman a lenguajes concretos mediante compilación semántica-preservante compL
• Evita la complejidad de traducción de lenguaje completo

3. Método Híbrido CEGIS-CEGAR

El núcleo del algoritmo es un ciclo iterativo de dos capas:

Ciclo CEGAR Externo:

1. Construir modelo abstracto M' usando contrato actual
2. Verificador de modelos verifica M' ⊨ φ
3. Si falla, verificar si el contraejemplo es espurio
4. Si es espurio, refinar contrato; de lo contrario, reportar contraejemplo verdadero

Ciclo CEGIS Interno:

1. Oráculo de síntesis genera contrato candidato
2. Verificador de predicado verifica validez del contrato
3. Si es inválido, agregar ejemplo positivo y resintentizar

Puntos de Innovación Técnica

1. Estrategia de Verificación Compositiva

A diferencia de traducción monolítica, PolyVer adopta estrategia "divide y conquista":

• Usar abstracción de contrato para procedimientos individuales
• Verificadores específicos del lenguaje verifican validez de contratos
• Verificador de modelos verifica propiedades a nivel de sistema

2. Generación Automática de Contratos

Soporta múltiples oráculos de síntesis:

• Sintetizador Basado en LLM: Utiliza prompts de cadena de pensamiento y DSL de Python
• Sintetizador SyGuS/SyMO: Codifica problemas como problemas de programación por ejemplos

3. Verificación de Espuriosidad

Verificar la alcanzabilidad de trazas de contraejemplo mediante {V = d} C {V' ≠ d'}, distinguiendo entre contraejemplos verdaderos y espurios.

Configuración Experimental

Conjunto de Datos

1. Pruebas de Referencia LFVerifier: 22 programas Lingua Franca, incluyendo sintaxis C restringida
2. Ejemplos LF Completos: Controlador LED, robot escalador, controlador de actitud de satélite y otros sistemas embebidos
3. Sistemas Políglotas: Programas LF mixtos C/Rust, aplicaciones ROS2, programas de llamadas FFI

Métricas de Evaluación

• Número de iteraciones de síntesis (IS: iteraciones CEGIS, AR: iteraciones CEGAR)
• Tiempo de ejecución (SOT: tiempo de oráculo de síntesis, VOT: tiempo de verificador de predicado, UT: tiempo UCLID5)
• Tasa de éxito de verificación

Métodos de Comparación

Comparación con LFVerifier15, la única herramienta conocida de verificación automática end-to-end para programas LF.

Detalles de Implementación

• Uso de OpenAI o1-mini como sintetizador LLM, 3 consultas paralelas por procedimiento
• CBMC-6.3.1, Kani-0.56.0, z3-4.8.7 como backends de verificación
• Máquina Intel Core i9 de 3.7GHz, 62GB RAM

Resultados Experimentales

Resultados Principales

RQ1: Comparación con Trabajo de Verificación LF Existente

En 22 pruebas de referencia:

• PolyVer verifica exitosamente todas las pruebas, LFVerifier no puede verificar el ejemplo TrafficLight
• 18 pruebas sintetizan correctamente contratos en un único ciclo CEGIS, promedio 37 segundos
• Aunque el tiempo de ejecución total es más lento (principalmente dominado por tiempo de síntesis de contrato), proporciona mejoras cualitativas significativas

RQ2: Manejo de Ejemplos LF Completos

Verificación exitosa de sistemas embebidos que contienen código C completo:

• Controlador LED: 1 procedimiento, 123 líneas de código C, 31.0 segundos de tiempo de síntesis
• Robot Escalador: 12 procedimientos, 75 líneas de código C/Rust, 685.4 segundos de tiempo de síntesis
• Controlador de Satélite: 6 procedimientos, 424 líneas de código C, 729.0 segundos de tiempo de síntesis

RQ3: Verificación de Sistemas Políglotas

Verificación de verdaderos sistemas políglotas:

• Programas LF mixtos C/Rust
• Aplicaciones de servicio ROS2
• Programas de llamadas FFI entre lenguajes

Hallazgos Importantes

1. LLM Supera Métodos Simbólicos: Los solucionadores SyGuS/SyMO requieren numerosas iteraciones CEGAR y frecuentemente no terminan
2. Desafíos en Síntesis de Contratos: Procedimientos con flujo de control complejo y dependencias de datos requieren más iteraciones
3. Verificación de Practicidad: Capaz de manejar código de implementación real en lugar de ejemplos de juguete

Trabajo Relacionado

Verificación de Sistemas Políglotas

• Métodos de Traducción Manual: Cook et al. traducen código de ensamblador a C para verificar el hipervisor Xen
• Traducción Automática de Fragmentos: LFVerifier traduce automáticamente fragmentos C a lenguaje de verificación
• Métodos de Caja Negra: Inferir resúmenes del comportamiento de entrada-salida

Verificación Compositiva

• Verificación compositiva basada en lógica de Hoare ampliamente aplicada a programas de gran escala en un único lenguaje
• Uso de interpretación abstracta y CEGAR para automatizar aprendizaje de precondiciones/postcondiciones

Inferencia de Contratos

• Métodos de inferencia de contratos guiados por propiedades
• Solucionadores de cláusulas Horn de restricción
• Aplicaciones recientes de LLM en aprendizaje de especificaciones

Conclusiones y Discusión

Conclusiones Principales

1. PolyVer resuelve exitosamente desafíos clave en verificación de sistemas políglotas
2. El método compositivo evita la complejidad de traducción de lenguaje completo
3. La síntesis automática de contratos hace el método práctico
4. Los sintetizadores basados en LLM funcionan mejor que métodos simbólicos tradicionales

Limitaciones

1. Terminación: El algoritmo no garantiza terminación, depende de la calidad del oráculo de síntesis
2. Soporte de Lenguajes: Actualmente solo soporta C y Rust, requiere desarrollo de oráculos de verificación para otros lenguajes
3. Expresividad de Contratos: La capacidad expresiva del lenguaje intermedio L* limita la complejidad de propiedades verificables
4. Escalabilidad: El tiempo de síntesis de contratos para sistemas grandes puede convertirse en cuello de botella

Direcciones Futuras

1. Extensión a otros sistemas de software distribuido poliglota y sistemas robóticos
2. Aplicación a verificación formal de traducción de código (como traducción de C a Rust)
3. Mejora de eficiencia y precisión de síntesis de contratos
4. Soporte para propiedades de lógica temporal más complejas

Evaluación Profunda

Fortalezas

1. Importancia del Problema: La verificación de sistemas políglotas es un problema práctico e importante
2. Innovación del Método: La combinación de verificación compositiva + síntesis automática de contratos es novedosa
3. Fundamento Teórico: Definiciones formales claras, garantías de corrección explícitas
4. Valor Práctico: Capaz de manejar sistemas reales en lugar de ejemplos de juguete
5. Implementación de Herramienta: Proporciona implementación de herramienta utilizable

Insuficiencias

1. Sobrecarga de Rendimiento: El tiempo de síntesis de contratos es relativamente largo, puede limitar aplicación práctica
2. Cobertura de Lenguajes: Actualmente solo soporta C y Rust, extensibilidad requiere verificación
3. Pruebas Limitadas: Aunque incluye ejemplos reales, la escala es relativamente pequeña
4. Dependencia de LLM: Depende de servicios LLM comerciales, puede afectar reproducibilidad

Impacto

1. Contribución Académica: Abre nueva dirección de investigación para verificación de sistemas políglotas
2. Valor Práctico: Proporciona herramienta de verificación para sistemas políglotas críticos para la seguridad
3. Inspiración Técnica: La idea de contratos como interfaz entre lenguajes tiene valor universal

Escenarios Aplicables

1. Sistemas Embebidos: Sistemas en tiempo real mixtos C/Rust
2. Sistemas Distribuidos: Marcos ROS2, gRPC y otros políglotas
3. Aplicaciones Críticas para la Seguridad: Sistemas que requieren garantías de verificación formal
4. Integración de Sistemas Heredados: Sistemas con código nuevo y antiguo mezclado

Referencias

El artículo cita 50 referencias relacionadas, cubriendo múltiples campos incluyendo sistemas políglotas, verificación formal, inferencia de contratos, síntesis guiada por sintaxis y otros trabajos importantes, proporcionando una base teórica sólida para la investigación.

Evaluación General: Este es un artículo de investigación de alta calidad que resuelve un problema importante y práctico. El método es innovador, la experimentación es completa y la implementación de herramienta es integral. Aunque hay espacio para mejora en rendimiento y escalabilidad, hace contribuciones importantes al campo de verificación de sistemas políglotas.