Transcription
Modelamiento y Validación con VDM de un Sistemade Control Automatizado de Velocidad en Vehículosusando Bluetooth Low Energy BeaconsAlvin Chunga Mamani, Estudiante1Universidad Nacional de San Agustín, Perú, alvin@episunsa.edu.pe.1Abstract– Con el crecimiento del parque automotor en la ciudadde Arequipa, aumenta el número de accidentes de tránsito por elexceso de velocidad en los vehículos, al analizar esta situación deplantea el desarrollo de un sistema de control de velocidadautomatizado en vehículos usando dispositivos Bluetooth LowEnergy Beacons para controlar la velocidad limite en zonas críticasde manera segura sin dañar los vehículos usando rompemuelles.Dado que es un sistema de control crítico se utiliza especificaciónformal para su desarrollo y verificación utilizando VDM.Keywords—Bluetooth low energy, Bluetooth beacons, VDM,beacons, car velocity control.I. INTRODUCCIÓNEn tiempos recientes en la creación de Sistemas de softwarecomplejos se tiende a cometer errores en la especificación derequerimientos antes de haber comenzado a desarrollarlo, endichos sistemas de se requiere de una precisión alta y loserrores hacen que se produzca una demora en la producción dedicho sistema además de generar inmensos gastos al tenerrequerimientos ambiguos. Esto se produce a causa de usarlenguaje natural el cual es ambiguo y se presta a diferentesinterpretaciones [1].El uso de Especificaciones Formales para la realización de unsistema provee una serie de ventajas al usar un lenguajeestructurado no ambiguo usando notación matemática para laespecificación de requerimientos en la etapa inicial delsoftware, para poder detectar y corregir errores en losrequerimientos antes de empezar a desarrollar el software.Sistemas Complejos que requieren un nivel de precisión criticoen donde errores en el software producen un inminente fallodel sistema, se requiere un análisis detallado para producir unsoftware que cumpla con los requisitos establecidos y lograr lacorrecta funcionalidad del Sistema sin fallos. Estos sistemasson críticos en el que un error en la elaboración del softwareconlleva a una inminente catástrofe.Se planea implementar un Sistema Automatizado paracontrolar la Velocidad de los Vehículos mediante el uso dedispositivos Bluetooth-Beacons, para ello se utilizará laherramienta VDM para modelar el sistema usando métodosformales propios de la herramienta y validarlos usando lamisma herramienta, creando test propios que sirvan paradetectar errores en los modelos y corregirlos.II. TRABAJOS RELACIONADOSSune Wolf [2] presenta un modelo ejecutable del protocolo decomunicación entre un sistema de auto-defensa utilizado abordo de aviones de combate usando Vienna DevelopmentMethod (VDM) y validado usando distintos escenarios paracubrir diferentes casos que puedan ocurrir en el sistema. Unaalternativa de análisis de los diferentes escenarios en vez dehacerlos manualmente, que consume mucho más tiempo yconlleva muchos errores.Shota, Michitoshi, Erjing y Masaru [12,14] presentan unsistema para gestionar la asistencia de estudiantes utilizandodispositivos BLE (Bluetooth Low Energy) el cual resuelve elproblema de las SmartCard que los estudiantes usaban pararegistrar asistencia y salirse de clases, además del tiempo queempleaban los estudiantes en escanear su tarjeta por un solodispositivo terminal. Se realizó una aplicación para dispositivosAndroid que recibe la señal del Beacon en el aulaperiódicamente, el cual garantiza la asistencia a clases de losestudiantes.Kumaresan y Gokulnath [13] plantean un sistema de monitoreoy seguimiento de vehículos utilizando IBeacon para guardar lainformación del vehículo y notificar a dispositivos Smartphonela ubicación del vehículo que pasa por determinada calle. Conla autorización del usuario se accederá a la informaciónguardada en el IBeacon y se calculará la posición y velocidaden base a las señales emitidas por el IBeacon y los dispositivosSmartphone.Gaurav y Varun [15] desarrollaron una herramienta para lavigilancia en tiempo real de una institución, registrar15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
asistencias y, enviar enlaces a páginas web y notificacionespara comunicarse con los estudiantes.En los trabajos vistos se ha realizado sistemas de monitoreo ycontrol usando la tecnología de dispositivos BLE.III. ESPECIFICACION FORMAL Y VDM A. DefiniciónUna especificación formal usa notación matemática paradescribir de manera precisa las propiedades que un sistema deinformación debe tener, sin preocuparse por la forma deobtener dichas propiedades. Describe lo que el sistema debehacer sin decir cómo se va a hacer. Esta abstracción hace quelas especificaciones formales sean útiles en el proceso dedesarrollar un sistema, porque permiten responder preguntasacerca de lo que el sistema hace con confianza, sin la necesidadde tratar con una gran cantidad de información no relevanteque se encuentra en el código de programa del sistema en unlenguaje de programación cualquiera, o especular sobre elsignificado de frases en un impreciso Pseudocódigo [3].B. VDM Vienna Development Method(VDM) es una colección detécnicas para especificación formal y desarrollo de software.VDM se origina en los laboratorios del IBM en Viena en 1970.El primer lenguaje soportado por el método de VDM se llamóVDL por sus siglas en inglés (Vienna Definition Language), elcual evolucionó en el lenguaje especificado VDM-SL el cualfue ISO estandarizado. A través de los años, las extensionesfueron definidas al modelo orientado a objetos [4].C. Class DefinitionEn VDM un modelo consiste en un conjunto de clasesespecificadas. Existen clases pasivas y activas, las activas sonaquellas que tienen su propio hilo de control y no necesitan deeventos externos para trabajar, mientras que las pasivassiempre son manipuladas desde el hilo de control de una claseactiva. El termino objeto es usado para denotar una instanciade una clase. Se pueden crear múltiples instancias de una claseusando el operador new que retorna una referencia al objeto.Una especificación de clase tiene los siguientes componentescomo se observa en la Fig. 1 [9]:Fig. 1 Esquema de la Clase.a) Encabezado de Clase: El encabezado de clase es el nombrede la clase e información de herencia. Una y múltiplesherencias son soportadasb) Variables de Instancia: Las variables de instancia son elestado del objeto que consiste en un conjunto de variablesde tipo que pueden ser simples como bool o nat, o tiposcomplejos como sets, sequences, maps, tuples, records yobjetos.c) Operaciones: Las operaciones son los métodos de clase quepueden modificar el estado, pueden ser definidosimplícitamente, usando pre y post condiciones, oexplícitamente, usando declaraciones imperativas yopcionalmente pre-post condiciones.d) Funciones: Las funciones son similares a las operaciones,pero el cuerpo de estas es una expresión en lugar de unadeclaración imperativa.e) Sincronización: La sincronización en VDM es asíncrona.f) Hilos: Un hilo es una secuencia de sentencias que seejecutan hasta la terminación en cuyo punto el hilo muere.Es posible especificar subprocesos que nunca terminan.D. ExpresionesLas expresiones se usan para describir cálculos que noproducen efectos secundarios; Esto significa que nuncapueden afectar el valor de una variable de instancia (a menosque contenga una llamada a la operación). VDM tiene 25categorías diferentes de expresiones.Una de las principales categorías utilizadas para definirprecondiciones, condiciones post e invariantes sonexpresiones cuantificadoras. La cuantificación de expresioneses un tipo de expresión lógica. Se utilizan con frecuencia15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
cuando es necesario una afirmación sobre una colección devalores. Hay dos tipos de cuantificadores de expresión:cuantificador universal (forall) y cuantificador existencial(exist) [10].E. Herramienta: VDM ToolBoxVDMTools es un conjunto de herramientas que le permitendesarrollar y analizar modelos precisos de sistemasinformáticos. Cuando se usan en las primeras etapas deldesarrollo del sistema, estos modelos pueden servir comoespecificaciones del sistema, o como una ayuda para comprobarla consistencia y completitud de los requerimientos de losusuarios [7].VDM ToolBox provee soporte para validación de laespecificación a través de la ejecución de pruebas utilizandoun intérprete. El intérprete permite ejecutar partes de laespecificación utilizando valores seleccionados por eldesarrollador (casos de prueba) [4].IV. BLUETOOTH LOW ENERGYA. Definición.Bluetooth Low Energy es similar al clásico Bluetooth, ya quecomparten el mismo espectro digital y la técnica de modulación,así como la tasa de bits, la única diferencia es el espaciamientode la capa física que es de 2 megaHertz en Bluetooth clásicomientras que en Bluetooth Low Energy es de un megaHertz.Como su nombre indica, la energía baja de Bluetooth usadapara el consumo bajo de la energía y los dispositivos BluetoothLow Energy son mucho más baratas que los dispositivosclásicos de Bluetooth [11].Un Beacon en tecnología inalámbrica es el concepto de ladifusión de pequeñas piezas de información como se muestraen Fig. 2. La información puede ser cualquier cosa, desde datosambientales (temperatura, presión de aire, humedad, etc.) hastadatos de micro-localización (seguimiento de activos,minoristas, etc.) o datos de orientación (aceleración, rotación,etc.).Fig.2 Dispositivo BeaconLos datos transmitidos son típicamente estáticos, pero tambiénpueden ser dinámicos y cambiar con el tiempo. Con el uso dela energía baja de Bluetooth, los beacons se pueden diseñarpara funcionar por años con una sola batería de tamaño de lamoneda [8].B. Características.En más detalles, Ibeacon son transmisores de baja complejidadque promueven una carga útil BLE particular con informaciónde identificación:A. UUID de proximidad (identificador universalmente único):valor de 128 bits que identifica de manera única a uno omás Ibeacon. Este identificador es obligatorio.B. Major data: un número sin signo de 16 bits utilizado parasegregar Ibeacon que tiene el mismo UUID de inmediatez.Este valor es voluntario.C. Minor data: un número sin signo de 16 bits utilizado paraseparar Ibeacon que tiene el mismo UUID de inmediatez yel valor principal. Este valor también es voluntario.Ibeacon que presentan el mismo UUID forman una región defaro. Entonces, cuando un dispositivo móvil con la aplicaciónactivada BLE entre en la región ibeacon, recibirá unanotificación apropiada. Estas aplicaciones también puedencontrolar la distancia relativa al ibeacon, usando el valor deRSSI [13].V. CASO DE APLICACIÓNA. Planteamiento del problemaLa ciudad de Arequipa es la segunda con un parque automotormás grande en Perú, lo que también implica un aumento en losaccidentes de tránsito, según el INEI en el año 2014 Arequipafue el departamento que registro la tasa de accidentes detránsito más elevada con 6,518 accidentes por cada 100milhabitantes, Según el estudio del INEI, el 42.9% de accidentesde tránsito fue ocasionado por el exceso de velocidad [16].15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
Actualmente no se cuenta con un sistema de control develocidad que restrinja rígidamente la velocidad de losvehículos en determinadas zonas como colegios, se ha tratadode solucionar esta problemática construyendo rompemuellesen para obligar a los vehículos a reducir la velocidad endeterminadas zonas transitadas en las que podría ocurriraccidentes por el exceso de velocidad, como es el caso de loscolegios.Tal como se muestra en Fig. 3 la creación de rompemuelles esrealizada en zonas cercanas a los colegios para obligar a losvehículos que transiten por la zona se vean obligados a reducirla velocidad al entrar a una zona muy transitada por escolares,para que no puedan ocurrir accidentes por un exceso develocidad.Fig. 4 Ubicación de Dispositivos Beacon.Los requerimientos identificados son:R1 Un sistema para el control de velocidad en Carrosusando BeaconsR2 El Beacon debe guardar un código que lo identifiquepara ser validad y la velocidad máxima que se leasigne.R3 Un carro puede estar en el rango de varios Beacons ala vez.Fig. 3 Rompemuelle tradicional.Construir rompemuelles es una solución que se haimplementado en la mayoría de lugares en los que se necesitaobligar a los conductores a reducir la velocidad de su vehículo,se cumple con el objetivo, pero al costo de que los vehículossufren daños por causas de este por lo que también podríadecirse que son un “rompeautos”.R4 La velocidad del carro debe reducirse periódicamentesi excede a la velocidad que marque algún Beacon enel rango de alcance.C. Diagrama de ClasesEn Fig. 5 se muestra el diagrama de clases generado con laespecificación realizada en las clases Beacon y Car, y lavalidación de los modelos usando la clase Test.B. PropuestaSe ha considerado utilizar dispositivos Bluetooth Low EnergyBeacons para el Sistema Propuesto, colocándolos en zonasestratégicas como se observa en Fig. 4, a fin de hacer que unautomóvil que entre en el rango del dispositivo baje suvelocidad periódicamente hasta la máxima indicada en eldispositivo Beacon.Fig. 5 Diagrama de clases15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
Las operaciones (línea 15 en adelante) son de acceso(get) ymodificación(set) de cada componente del Beacon para poderser manipulado.D. Especificación en VDM Se utilizó la herramienta VDM Toolbox.En las Fig. 6 y 7 se presenta la especificación formal enVDM .Fig. 6 Especificación de la clase Beacon.En la Fig. 6 se modela el Beacon, especificando loscomponentes propios del dispositivo de manera formal.En las líneas 10 a la 12 se especifica las propiedades que tieneun Beacon como son el UUID (Identificador propio de cadaBeacon), majorData (majorData del Beacon) y minorData(minorData del beacon), de los cuales se utilizara el majorDatapara registrar el máximo de velocidad marcada por el Beacon.Fig. 7 Especificación de la clase Car15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
En la Fig. 7 se muestra el vehículo modelado en el lenguajeformal VDM simulando el comportamiento real de un vehículo.En las líneas 9 y 10 se crean variables para representar lavelocidad y dirección del vehículo, en la línea 11 una secuenciade Beacons los cuales representan una lista, en la cual se añadeun Beacon si el vehículo entro en su rango, y al salir del rangose elimina de la lista, en base a esta lista se escoge el Beaconque tenga la menor velocidad máxima en su majorData y serála velocidad que se le ponga como limite al vehículo mientrasesté en su rango.En la línea 13 a la 19 se definen las invariantes, que son lascondiciones sobre las que trabaja el sistema, la primerainvariante (línea 14) representa la velocidad del vehículo quesiempre es mayor igual que 0, en la línea 16 la velocidadmáxima a la que puede llegar un vehículo sin restricciones develocidad, en la línea 18 y 20 se representa la dirección delvehículo que pueden ser 3 valores: -1 en sentido contrario, 0sin velocidad y 1 si se encuentra en movimiento hacia adelante.R1R2R3R4Está definido en la clase Car Fig.7.Está definido en la clase Beacon Fig. 6 que considera3 atributos, “UUID” representa el código deidentificación propio del Beacon que consta de16bytes línea 10, “majorData” representa el límitede velocidad que se le asigna al Beacon línea 11.Está definido en la clase Car Fig 7., el atributobeacons que es una secuencia de Beacons línea 11,la adición de Beacons se da en la función“addBeacon” en las líneas 56 a la 59, la eliminaciónde Beacons se da en la función “DeleteBeacon” enlas líneas 48 a la 55.Está definido en la clase Car Fig 7. en la función“ReduceSpeed” que se encarga de la comprobaciónde velocidad del vehículo y los Beacons que estén ensu rango reduciendo la velocidad periódicamentecomo se ve en las líneas 36 a la 46Fig. 8 Validación del modelo.En la Fig. 8 se muestra la validación del sistema realizado enVDM comprobando la funcionalidad y cobertura de todoslos métodos implementados en las clases Car y Beacon en unambiente simple de prueba en el que se simula la actividad quetendrá el sistema, modelado en la clase Test1 Fig. 9.E. Validación15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
vehículo ha salido del rango de un Beacon con lo que se invocaal método “DeleteBeacon” el cual remueve el Beacon de lalista del vehículo porque este ya no lo afecta.VI. RESULTADOSLa ciudad de Arequipa presenta un crecimiento del parqueautomotor cada año y con este también los accidentes que seproducen por el exceso de velocidad, el sistema planteado eneste trabajo muestra el uso de tecnología de bajo costo comoson los Beacons en un sistema de control de velocidad devehículos, siendo el reemplazo a los rompemuelles que dañanlos vehículos y no garantizan el control de velocidad en puntoscríticos como son los centros educativos.Se ha modelado y realizado la verificación del sistemapropuesto en este trabajo utilizando la herramienta VDM Tools, evaluando el correcto comportamiento y funcionamientorealizado en un ambiente simuladoREFERENCES[1][2][3][4][5][6]Fig. 9 Clase Test1.En la Fig. 9, en la línea 16 se inicializan 2 beacons invocandoa una función “createBeacons”, en esta función, se crean 2beacons (línea 31 y 32), se les asigna sus UUID (línea 33 y 34)que es su identificador único, y en las líneas 35 y 36 se lesasigna la velocidad máxima que tendrán almacenadas, uno con70 y otro con 50. En la línea 17 se crea un nuevo vehículo, sele asigna una velocidad en la línea 18. En la línea 20 se añadeun Beacon al vehículo, simulando que este entro en el radio deese Beacon, entonces el Beacon es añadido a la lista de beaconsdel vehículo. En la línea 21 se invoca a la función“ReduceSpeed” la cual evalúa la lista de beacons en los que seencuentra el vehículo y analiza si la velocidad actual delvehículo es menor que la velocidad máxima indicada por losbeacons, de no serlo procederá a disminuir la velocidad en unfactor preestablecido, de lo contrario el vehículo permanecerácon la velocidad que tenga. En la línea 24 se simula que el[7][8][9][10][11][12][13]Sten Agerholm and Peter Gorm Larsen, Modeling and Validating SAFERin VDM-SL, In Fourth NASA Langley Formal Methods Workshop.NASA, November 1997Wolff, S. (2015). Using Executable VDM Models in an IndustrialApplication-Self-defense System for Fighter Aircraft. Technical ReportElectronics and Computer Engineering.J. Michael Spivey ,The Z Notation: A reference manua , vol. 2, 1992.Cliff B. Jones, Systematic Sodtware Development Using VDM, SecondEdition, June 8 1995Elizabeth Vidal-Duarte. “Aplicación y validación de especificacionesformales ligeras en el modelo conceptual: reduciendo la ambigüedad eincrementando la conformidad entre los requerimientos y el código”,2012.Shawn A. Bohner, Denis Graˇcanin1, Michael G. Hinchey andMohamed Eltoweissy, “Model-based evolution of collaborative agentbased system”. Journal of the Brazilian Computer Society, 2007, vol.13,n.4, pp.17-38. ISSN 0104-6500VDMTools User Manual (VDM ) ver1.1JoakimLindh. Bluetooth Low Energy Beacons Application ReportSWRA475A–January 2015–Revised October 2016Jozef Hooman and Marcel Verhoef. Format Semantics of a VDMExtension for Distributed Embedded Systems. Concurrency,Compositionality, and Correctness: Essays in Honor of Willem-Paul deRoever, pp 145.Elizabeth Vidal Duarte. “Refining light-weight formal specificationsvalidations using black box testing and code coverage analysis: anelectrocardiograph application”. 14th LACCEI International MultiConference for Engineering, Education, and Technology: “EngineeringInnovations for Global Sustainability”.M. Siekkinen, M. Hiienkari, J. K. Nurminen and J. Nieminen, ”How lowenergy is bluetooth low energy? Comparative measurements withZigBee/802.15.4,” Wireless Communications and NetworkingConference Workshops (WCNCW), 2012 IEEE, Paris, 2012, pp. 232-237Shota Noguchim, Michitoshi Niiborim, Erjing Zhou and MasaruKamada.” Student attendance management system with bluetooth lowenergy beacon and android devices”. 18th International Conference onNetwork-Based Information Systems 2015.G. Kumaresan and J. Gokulnath. “Beacon based vehicle tracking andvehicle monitoring system”. nternational Journal of Advanced Research15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
in Computer and Communication Engineering Vol. 5, Issue 3, March2016[14] Cüneyt BAYILMIŞ and Mehmet ÖZDEMİR. “A student attendancesystem based on beacon and smartphones equipped with bluetooth lowenergy technology. BİLİŞİM TEKNOLOJİLERİ DERGİSİ, CİLT: 9,SAYI: 3, EYLÜL 2016.[15] Gaurav Saraswat and Varun Garg. “Beacon controller campussurveillance”. 2016 Intl. Conference on Advances in Computing,Communications and Informatics (ICACCI), Sept. 21-24, 2016, Jaipur,India[16] Arequipa presenta la mayor tasa de accidentes de tránsito, Diario nta-mayor-tasa-accidentestransito-215418315th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnershipsfor Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States.
15th LACCEI International Multi-Conference for Engineering, Education, and Technology: “Global Partnerships for Development and Engineering Education”, 19-21 July 2017, Boca Raton Fl, United States. asistencias y, enviar enlaces a páginas w
