Mostrar el registro sencillo del ítem

dc.contributor.authorToscano-Moreno, Manuel
dc.contributor.authorArregui, Alberto
dc.contributor.authorMandow, Anthony 
dc.contributor.authorGarcía-Cerezo, Alfonso José 
dc.date.accessioned2019-09-17T11:28:23Z
dc.date.available2019-09-17T11:28:23Z
dc.date.created2019
dc.date.issued2019
dc.identifier.citationToscano Moreno, M., Arregui, A., Mandow, A., García-Cerezo, A. (2019). Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino. En XL Jornadas de Automática: libro de actas, Ferrol, 4-6 de septiembre de 2019 (pp. 617-622). DOI capítulo: https://doi.org/10.17979/spudc.9788497497169.617. DOI libro: https://doi.org/10.17979/spudc.9788497497169en_US
dc.identifier.urihttps://hdl.handle.net/10630/18369
dc.description.abstractLos grupos de ascensores con sistema de preselección de destino persiguen la reducción del tiempo de espera en edificios de mediana y gran altura como hoteles o bloques de oficinas. En este tipo de sistemas, los pasajeros se dirigen al ascensor de acuerdo con el destino que hayan indicado en un panel exterior. El presente trabajo aborda la verificación del control de ascensores con preselección de destino mediante la aplicación de una herramienta software basada en lógica temporal lineal (LTL). En particular, se ha definido tanto el modelo del sistema como la especificaciones LTL mediante la herramienta de código abierto \textsc{Spin}. Como caso de estudio, se ha implementado el modelo de un grupo de dos ascensores en un edificio de cuatro plantas con paneles de preselección de destino en cada planta. El artículo ofrece resultados preliminares de simulaciones y verificaciones para un conjunto de fórmulas LTL definidas específicamente para este sistema.en_US
dc.description.sponsorshipEste trabajo ha recibido financiación del proyecto nacional RTI2018-093421-B-I00, la Universidad de Málaga (Andalucía Tech) y la ayuda BES-2016-077022 del Fondo Social Europeo FSE. Universidad de Málaga. Campus de Excelencia Internacional Andalucía Tech.en_US
dc.language.isospaen_US
dc.publisherComité Español de Automática - Universidade da Coruña Servizo de Publicaciónsen_US
dc.rightsinfo:eu-repo/semantics/openAccessen_US
dc.subjectAscensoresen_US
dc.titleModelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destinoen_US
dc.typeinfo:eu-repo/semantics/conferenceObjecten_US
dc.relation.eventtitleXL Jornadas de Automáticaen_US
dc.relation.eventplaceFerrolen_US
dc.relation.eventdate4-6 de septiembre de 2019en_US


Ficheros en el ítem

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem