Verificación difusa en línea de sistemas de tiempo real y análisis de su incertidumbre

Resumen

Esta tesis presenta el leguaje de especificación FTL-CFree, que extiende la lógica temporal con semántica difusa y con la capacidad para cuantificar variables, a fin de ser aplicado en el ámbito de la verificación en línea. La semántica del lenguaje es difuso-evolutiva, pues, dada una traza de entrada, la interpretación no sólo establece el grado de certeza de la aserción, sino que además determina cómo esta magnitud puede evolucionar si nuevos sufijos son incorporados a la traza de entrada. Como es habitual en la verificación en línea, el lenguaje provee la generación del oracle correspondiente y, por lo tanto, es posible obtener una especificación observable a partir de los requisitos de alto nivel de un sistema. La verificación en línea proporciona información, en cada instante, del estado de un sistema. Sin embargo, la capacidad para analizar su estado desde un punto de vista estacionario, cuando el sistema opera en condiciones nominales, resulta de gran utilidad entre la comunidad de ingenieros. El resultado de evaluar un requisito de la especificación, formulado con el lenguaje FTL-CFree, está afectado por la variación intrínseca del propio sistema y, con esto, caracterizar estadísticamente su respuesta es de especial interés. La semántica de FTL-CFree transforma un escenario de entrada en una medida difusa, que puede ser analizada de acuerdo con el principio de variable aleatoria. Así, se demuestra que una fórmula FTL-CFree sigue una distribución de probabilidad específica y se confirma que la teoría de la probabilidad es capaz de caracterizar la incertidumbre aleatoria en mediciones difusas. A partir del principio de variable aleatoria FTL-CFree, y tomando una serie de restricciones probabilísticas en condiciones nominales, se desarrolla un método para la identificación (parametrización) de fórmulas.