Inferencia y verificación de propiedades en sistemas ciber-físicos estocásticos

Abstract

Este Trabajo de Fin de Grado tiene principalmente como objetivo la ampliación de las capacidades de análisis de las herramientas para la vericación de los sistemas ciberfísicos en tiempo de ejecución. Los requisitos de la vericación están expresados en Signal Temporal Logic (STL), un tipo de lógica temporal enfocada al análisis de señales analógicas o reales. La lógica temporal es un tipo de lógica modal que nos permite expresar propiedades sobre un estado o una secuencia de estados del sistema. La primera mejora consiste en añadir dos nuevos operadores lógicos para denir tendencias (derivadas) y acumulaciones (integrales) sobre esas señales. La segunda parte del proyecto consiste en incorporar los nuevos operadores lógicos en una una biblioteca de minería de datos ya existente para evaluar expresiones de STL paramétrica. Hemos comprobado el buen funcionamiento de los nuevos operadores y hemos diseñado una nueva interfaz gráca para ofrecer una interacción más fácil tanto con STL como con la biblioteca de minería.

The purpose of this Final Degree Project is mainly to expand the analysis capabilities of the tools for the verication of cyber-physical systems at runtime. The verication requirements are expressed in Signal Temporal Logic (STL), a type of temporal logic focused on the analysis of analog or real signals. Temporal logic is a type of modal logic that allows us to express properties about a state or a sequence of states of the system. The rst improvement consists of adding two new logical operators for dening trends (derivatives) and accumulations (integrals) in those signals. The second part of the project consists of including the new logical operators to an existing data mining library for evaluating parametric STL expressions. We have tested the functionality of the new operators and designed a new graphical interface that oers an easier interaction with both STL and the data mining library.