Tesis doctoral de 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 parecían cómo las técnicas de verificación formal han permitido detectar errores en sistemas que parecían correctos. el model cheching es una técnica de verificación autonómica 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 concurrent constraint (cc) para especificar sistemas reactivos y sistemas híbridos. Se consideran tres lenguajes temporales que han sido definidos a partir del paradigma cc: el lenguaje tcc, el lenguaje tccp y el lenguaje hcc. Los dos primeros pueden modelar sistemas reactivos gracias a que han 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ántcias a veces no coinciden. En esta tesis se ha definido una semátncia 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 el lenguaje tcc más potente que el paradigma cc. 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 explortar las características del paradigma cc para resolver (en parte) el problema
Datos académicos de la tesis doctoral «Model checking of the concurrent constraint paradigm«
- Título de la tesis: Model checking of the concurrent constraint paradigm
- Autor: Alicia Villanueva García
- Universidad: Politécnica de Valencia
- Fecha de lectura de la tesis: 24/05/2003
Dirección y tribunal
- Director de la tesis
- María Alpuente Frasnedo
- Tribunal
- Presidente del tribunal: furio Honsell
- marco Cadoli (vocal)
- claude Kirchner (vocal)
- jacques Jaray (vocal)