Obtención automática del entorno en la verificación modular de sistemas reactivos

Abstract

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.