Enunciado

Se desea implementa el control de un cruce de carrreteras regulado con semáforos, con una carretera principal y otra secundaria, y botones para indicar la intención de cruzar de los peatones

• Ambas carreteras tienen un semáforo con un paso de peatones

• La carretera principal está en verde para los vehículos todo el tiempo que sea posible

• La carretera secundaria tiene una espira que permite identificar cuándo hay coches esperrando en el semáforo

• Si un peatón quierre cruzar, tiene que presionar el botón correspondiente

• Un peatón no puede esperar indefinidamente para cruzar

• Un coche de la carretera secundaria no puede esperar indefinidamente para pasar

Objetivo

Objetivo:  El objetivo de este reto es practicar la metodología propuesta para el desarrollo de soluciones creativas a un problema real.

Será necesario realizar todos los pasos del diseño orientado a modelos que hemos visto en clase hasta la fecha:

1. Especificación en LTL
2. Modelado de los comportamientos con máquinas de estados
3. Verificación formal del modelo
4. Implementación semi-automática

El reto planteado se realizará en grupos de hasta 3 personas, cualquier cuestión que surja se discutirá en el foro de esta sección (se premiará la participación ayudando a los compañeros), y se entregará en la tarea habilitada para tal fin en esta sección.

Debe entregarse un archivo comprimido (zip o rar) con los siguientes archivos:

documentacion.pdf

• Documentación de la práctica, incluyendo los nombres de los integrantes del equipo
• Debe justificar brevemente todas las decisiones

spin/model.pml

• Fichero Promela con la especificación en LTL del sistema (lo más completa posible)
• Incluye también el modelo de verificación de las máquinas de estados del sistema
• Incluye también el modelo del entorno

src/fsm.cysrc/fsm.h

• Implementación de máquinas de Mealy utilizada en la asignatura

src/model.c

• Implementación de las máquinas de estados del sistema utilizando la interfaz de fsm.h

src/main.c

• Programa principal con la activación periódica de las máquinas de estados del sistema
• main.c, model.c y fsm.c deben compilar limpiamente (sin errores ni warnings) para generar un ejecutable

—

PV : Principal verde

Estado de las carreteras:

• PV, SR
• PR, SV
• PR, SR -> Cuando se pulsen los dos botones de peatones, luego comprueba el sensor de coches, pasan todos los de secundaria, y luego da paso al principal.