Verificación de Sistemas en Tiempo Real utilizando Comprobadores de Modelos
Javier Tuya, José R. De Diego, José A. Corrales
NOVATICA, Vol.
118, pp. 74-81, Noviembre 95
(ps.zip)
Resumen
En este artículo se muestra cómo se pueden utilizar comprobadores de modelos
para realizar la verificación formal de propiedades de vivacidad y seguridad en
especificaciones gráficas obtenidas con métodos SA/RT. El comportamiento
reactivo del sistema se modela de forma operacional mediante diagramas de
transición de estados. Esta especificación es acompañada de las propiedades que
ha de cumplir, escritas de forma declarativa en lógica temporal CTL. Se utiliza
entonces un comprobador de modelos (SMV) para verificar el cumplimiento de las
propiedades deseadas en el modelo operacional.
Index - Testing
- Personal Page