Proyecto de Laboratorio de Verificación de Sistemas Concurrentes

Descripción del Sistema

La iteración de un usuario con el sistema de un automóvil que controla aspecto de velocidad crucero, confort, o seguridad etc...

Usuario:

-Apertura/Cierre centralizado del vehículo.
-Arrancar/Parrar el vehículo.
-Poner en movimiento el vehículo.
-Desactivar/Activar auto-frenado del vehículo.
-Establecer velocidad crucera.
-Activar/Desactivar sistema en pendientes.
-Abrir/Cerrar puerta del vehículo.

Sistema:

-Abrir/Cerrar coche.

-Freno de emergencia.

-Notificar del de auto-frenado.

-Notificar en caso de algún error.

-Informar velocidad crucera.

Verificación:

//El arrancado del vehículo siempre y cuando ha sido abierto.

ltl pruebaDos {[] (cierreCentralizado == activado -> <>(arranqueCoche == activado)) }

//Establecer velocidad crucero siempre que el vehículo este arrancado y en movimiento.
//Si si el vehículo no esta en movimiento o no esta arrancado llegara a poder poner velocidad crucero ?
//Esta prueba tiene que fallar para el correcto funcionamiento segun los criterios establecidos.

ltl pruebaDos {[] (movimiento == desactivado || arranqueCoche == desactivado -> <>(velCrucero == activado)) }

//Cuando se activa el cierre centralizado el vehículo tiene que estar sin movimiento ademas de estar cerrado y parado.

ltl pruebaTres {[] (cierreCentralizado == activado -> [](movimiento == desactivado && aperturaPuerta == activado && arranqueCoche == desactivado)) } 

 

Teórica del funcionamiento del sistema:

Un usuario mediante una llave abre el vehículo el cierreCentralizado, luego abre la puerta, lo arranca, puede o bien activar auto-frenado (sensores delante del vehículo que frena en caso de encontrar un obstáculo) o bien ponerlo en marcha, el sistema le notificara por la pantalla de lo seleccionado.

Una vez puesto en marcha el vehículo el usuario puede establecer velocidad crucera (100km/h pudiendo soltar el pie del acelerador).

Cuando el usuario llega a su destino parara el vehículo, sale de el y cierra con el cierre centralizado. El sistema hará que el vehículo se enciendan luces para confirmar que todo ha ido bien.

---

Nivel de abstracción:

Se plantea que: Tendremos un Usuario, Sistema ( vehículo) y Sensores.

-El usuario tiene comunicación bidireccional con el Sistema.

-Donde sensores son unidireccionales, al sistema.
-El sistema de frenado automático envía información al sistema, es decir el sistema no comprueba el estado del frenado automático.
-Cuando los sensores se activan, aparece un aviso al usuario.
-En un principio en el nivel de abstracción las puertas se pueden abrir y cerrar sin restricciones del sistema (en marcha o en movimiento).