Obtención automática del entorno en la verificación modular de sistemas reactivos
- Riva Alvarez, Claudio de la
- Pablo Javier Tuya González Directeur/trice
Université de défendre: Universidad de Oviedo
Fecha de defensa: 23 janvier 2004
- José Antonio López Brugos President
- José Antonio Corrales González Secrétaire
- José Javier Dolado Cosín Rapporteur
- José Miguel Toro Bonilla Rapporteur
- Juan Garbajosa Sopeña Rapporteur
Type: Thèses
Résumé
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.