Objetivos:
Primeramente has de obtener la información acerca del método, en este caso del comprobador de modelos ('model checker') SPIN. También tendrás que bajarte el software y configurarlo adecuadamente en tu ordenador. Como herramienta de verificación, SPIN puede ser más potente y versátil que otras herramientas similares estudiadas en el curso; además la especificación de las propiedades te será más fácil, ya que se realiza sólo utilizando LTLP. Por otra parte, SPIN utiliza un lenguaje de especificación que no conoces: Promela; tendrás que instalar el software y, posiblemente, buscar información de cómo hacerlo en 'Todo sobre SPIN' .
Puedes empezar leyendo una descripción general sobre el diseño y la estructura del 'verificador' SPIN, así como una revisión de sus fundamentos teóricos y de sus aplicaciones prácticas más importantes, en:
Para aprender a manejarlo bien, puedes programar algunos ejemplos, procurando tomar notas sobre los programas que realices y los resultados que has observes durante la ejecución. Después has de escribir el artículo, de acuerdo con los siguientes puntos:
-número mínimo de páginas =10
-escrito con el formato llncs2e (formalo LateX) o word
-describir el lenguaje de especificación SPIN, utilizando como ejemplos los programas cortos que has realizado.
-diseña detalladamente y verifica un sistema que conozcas bien
-elabora una especificación de las propiedades del sistema en LTL
-determina hasta qué punto el diseño que has realizado satisface la especificación y escríbelo
-llega a conclusiones, formalmente justificadas, acerca de las ventajas e inconvenientes que presenta el lenguaje de especificación Promela, el comprobador de modelos SPIN, respecto de otros que conozcas.
Calificación: sobre 10
puntos, dependerá del grado de consecución de los objetivos
anteriores:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|