Aplicación de la verificación del modelo CTL/LTL en algún sistema

Question

Me disculpo si mi título es vago, estoy tratando de aplicar la verificación del modelo CTL/LTL en algún sistema escrito en Java, sin embargo, todavía no entiendo cómo alcanzar un resultado utilizando ninguno de los enfoques mencionados. ¿Modelo mi especificación LTS/Escribir y uso una herramienta como Spin para validar eso o? Principalmente estoy buscando un punto en una dirección que me ayude a comenzar.

Nuevamente, lo siento, pero hice este hilo después de tanta frustración buscando una explicación de mi problema.

Gracias

Answer 1

Estoy bastante seguro de que necesitas diseñar tu sistema en Promela, en lugar de Java. Luego ingresa el sistema en Promela y la especificación en LTL (o CTL) para girar, lo que genera un código C para un verificador de modelos para la instancia específica.