Tesis doctoral de Claudio De La Riva Alvarez
El enfoque modular es una de las técnicas más adecuadas para aliviar el problema de la explosión combinatoria de estados en la verificación de sistemas reactivos. El análisis del sistema completo se traslada al análisis de los componentes que forman el sistema. En embargo, previamente a la verificación de cada componente, es encesario especificar los entornos con los que interacciona cada uno. en esta tesis se desarrollan dos métodos para la generación automática de los entornos (restricciones) que se puede utilizar en la verificación de cada componente. En el primero de ellos, la extracción de restricciones se realiza de forma independiente para cada componente del sistema usando la información de su entorno. Las restricciones generadas especifican relaciones entre los eventos del entorno del componente. La segunda, es una ampliación de la anterior, y permite la generación de restricciones para varios componentes del sistema. En este caso, las restricciones obtenidas en un componente dado están basadas en las generadas previamente en otro u otros componentes del sistema, y permiten especificar comportamientos más exactos del entorno. ambas técnicas se evalúan con un caso práctico de tamaño real y se comparan con al especificación manual de restricciones.
Datos académicos de la tesis doctoral «Obtención automática del entorno en la verificación modular de sistemas reactivos«
- Título de la tesis: Obtención automática del entorno en la verificación modular de sistemas reactivos
- Autor: Claudio De La Riva Alvarez
- Universidad: Oviedo
- Fecha de lectura de la tesis: 23/01/2004
Dirección y tribunal
- Director de la tesis
- Tuya González Pablo Javier
- Tribunal
- Presidente del tribunal: José Antonio Lopez brugos
- José Javier Dolado cosín (vocal)
- Miguel Toro bonilla (vocal)
- Juan Garbajosa sopeña (vocal)