Resumen de Model checking for the concurrent constraint paradigm
Alicia Villanueva García 
En muchas aplicaciones reales la verificación formal de propiedades temporales es imprescindible. En la bibliografía podemos encontrar muchos casos de estudio en los que se muestra cómo las técnicas de verificación formal han permitido detectar errores en sistemas que parecían correctos. El model checking es una técnica de verificación automática que, dado un modelo del sistema y una fórmula temporal, comprueba si el modelo satisface la fórmula. El problema principal del model checking es la explosión de estados. En esta tesis se usa el paradigma Concurren! Constraint (ce) para especificar sistemas reactivos y sistemas híbridos. Se consideran tres lenguajes temporales que han sido definidos a partir del paradigma ce: el lenguaje tcc, el lenguaje tccp y el lenguaje hcc. Los dos primeros pueden modelar sistemas reactivos gracias a que han sido definidos sobre una noción de tiempo discreto, mientras que el tercer lenguaje es capaz de modelar sistemas híbridos ya que usa una noción de tiempo continuo. Sabemos que una adecuada semántica denotacional permite realizar análisis muy interesantes de lenguajes. Cuando fue introducido el lenguaje tcc se definió su semántica operacional y su semántica denotacional, sin embargo estas dos semánticas a veces no coinciden. En esta tesis se ha definido una semántica denotacional fully abstract (con respecto a la semántica operacional) para el modelo de programación tcc. Además mostramos un ejemplo de cómo se puede usar esta nueva semántica denotacional para analizar la expresividad del operador de tcc que modela los conceptos de timeout y preemption. Se ha demostrado que la introducción de dicho constructor hace al lenguaje tcc más potente que el paradigma ce. El resultado más importante de esta tesis es la definición de un algoritmo de model checking para el lenguaje tccp. La idea es la de explotar las características del paradigma ce para resolver (en parte) el problema de la explosión de estados.
