Investigación
Mis intereses de investigación y áreas de enfoque.
Sistemas de Ciberseguridad
Investigación sobre métodos formales aplicados a la ciberseguridad, análisis de protocolos de seguridad y desarrollo de técnicas de verificación para sistemas seguros.
Sistemas Ciberfísicos
Modelado y verificación de sistemas que integran procesos computacionales y físicos, garantizando seguridad y confiabilidad en aplicaciones críticas.
Sistemas Distribuidos
Modelado y verificación de sistemas distribuidos, enfocándose en protocolos, algoritmos y técnicas de verificación formal para sistemas concurrentes.
Sistemas en Tiempo Real
Investigación sobre modelado, verificación y análisis de sistemas en tiempo real utilizando autómatas temporizados y especificaciones de lógica temporal.
Sistemas Embebidos Críticos
Desarrollo de técnicas de verificación formal para sistemas embebidos en dominios críticos de seguridad, garantizando corrección y confiabilidad.
Autómatas Temporizados
Investigación fundamental sobre autómatas temporizados con relojes parcialmente independientes, desarrollando nuevos modelos y algoritmos de verificación para sistemas en tiempo real.
Lógicas Temporales
Investigación sobre lógicas temporales para especificar y verificar propiedades de sistemas en tiempo real y distribuidos, incluyendo TCTL y otros formalismos temporales.
Simulación y Bisimulación
Desarrollo de relaciones de equivalencia y técnicas de refinamiento para sistemas temporizados y distribuidos utilizando teoría de simulación y bisimulación.
Model Checking
Aplicación de técnicas de model checking utilizando herramientas como UPPAAL y SCADE para verificar la corrección de sistemas en tiempo real y distribuidos.
Métodos Formales
Aplicación de técnicas matemáticas y especificaciones formales para diseñar, desarrollar y verificar sistemas de software y hardware con garantías rigurosas de corrección.
Demostración de Teoremas
Investigación sobre demostración interactiva de teoremas y asistentes de prueba para verificar propiedades complejas de sistemas en tiempo real y modelos de autómatas.
Pruebas Basadas en Modelos
Desarrollo de metodologías de prueba derivadas de modelos formales para generar automáticamente casos de prueba para sistemas complejos y líneas de productos de software.
Pruebas de Mutación
Investigación sobre técnicas de pruebas de mutación para evaluar la calidad de conjuntos de pruebas y mejorar la efectividad de las pruebas en sistemas altamente configurables.
Líneas de Productos de Software
Investigación sobre modelado de variabilidad, prueba de sistemas altamente configurables y escalado de análisis de variabilidad en líneas de productos de software.
Análisis y Representación Simbólica
Desarrollo de técnicas simbólicas y estructuras de datos para análisis y verificación eficiente de grandes espacios de estados en sistemas temporizados y distribuidos.