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.
//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)) }
Verificación:
//El arrancado del vehículo siempre y cuando ha sido abierto.
ltl pruebaDos {[] (cierreCentralizado == activado -> <>(arranqueCoche == activado)) }
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.
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).
-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).
