Verificación de sistemas distribuidos mediante el análisis de datos de comunicación

Ideas preliminares

Resumen

Este trabajo presenta ideas preliminares para el análisis formal de sistemas distribuidos, aprovechando datos observacionales derivados de la comunicación para verificar el comportamiento del sistema. Nuestra metodología sintetiza la especificación formal y la verificación en tiempo de ejecución, con especificaciones expresadas en un lenguaje específico de dominio basado en lógica de primer orden y programas regulares, similar a lo que se encuentra en la lógica dinámica de primer orden. Basándonos en este formalismo, diseñamos e implementamos una herramienta prototipo que emplea la verificación en tiempo de ejecución para analizar los datos registrados durante la ejecución del sistema, lo que permite tanto el análisis fuera de línea (post-mortem) como la verificación del comportamiento en tiempo de ejecución. Para validar nuestro enfoque, realizamos una evaluación experimental inicial utilizando datos de telemetría de un bus CAN satelital (desarrollado por INVAP S.E.), un sistema aeroespacial de misión crítica. Los resultados iniciales demuestran la capacidad del marco para detectar desviaciones del comportamiento especificado.