Análisis empírico de SMV en la verificación de Sistemas Reactivos
José R. De Diego, Claudio de la Riva, Javier Tuya
En: Jornadas de Ingeniería de Requisitos y ambientes Software (IDEAS'98),
Torres, Brasil, pp. 145-156, 1998
(ps.zip)
Resumen
Los comprobadores de modelos cuando se utilizan para verificar propiedades
sobre sistemas de tamaño no trivial, presentan el problema de la explosión de
estados. Aun cuando sean capaces de realizar la verificación en un tiempo
finito, este puede llegar a ser muy elevado. En este trabajo se muestran los
resultados de la reducción de tiempos de verificación en sistemas reactivos,
mediante el empleo de la verificación modular y a través de un uso adecuado del
verificador. Se analiza sobre un caso de estudio, cuáles pueden ser las
reducciones de tiempos obtenidas y se plantea una línea de trabajo con SMV a
partir de los datos obtenidos.
Index - Testing
- Personal Page