Mostrar o rexistro simple do ítem
Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino
dc.contributor.author | Toscano Moreno, Manuel | |
dc.contributor.author | Arregui, Alberto | |
dc.contributor.author | Mandow, Anthony | |
dc.contributor.author | García-Cerezo, Alfonso | |
dc.date.accessioned | 2019-08-16T07:38:57Z | |
dc.date.issued | 2019 | |
dc.identifier.citation | Toscano 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.9788497497169 | es_ES |
dc.identifier.isbn | 978-84-9749-716-9 | |
dc.identifier.uri | http://hdl.handle.net/2183/23775 | |
dc.description.abstract | [Resumen] Los 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 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. | es_ES |
dc.description.abstract | [Abstract] Destination dispatch systems for group control of elevators aim to reduce the waiting and displacement time with respect to conventional control systems in mid and high rise buildings such as hotels or office blocks. In these systems, passengers are directed to cars according to their destinations. The present work addresses verification of the destination control system for an elevator group by using a software tool based on linear temporal logic (LTL). In particular, both the system model and the LTL specifications have been defined using the open source tool Spin. As a case study, the model of a group of two elevators has been implemented in a four-story building with destination preselection panels in each plant. The article offers preliminary results of simulations and verifications for a set of LTL formulas defined specifically for this system | es_ES |
dc.description.sponsorship | Ministerio de Economía y Competitividad; RTI2018-093421-B-I00. | es_ES |
dc.description.sponsorship | Ministerio de Economía y Competitividad; BES-2016-077022 | es_ES |
dc.language.iso | spa | es_ES |
dc.publisher | Universidade da Coruña, Servizo de Publicacións | es_ES |
dc.relation.uri | https://doi.org/10.17979/spudc.9788497497169.617 | es_ES |
dc.rights | Atribución-NoComercial-CompartirIgual 4.0 | es_ES |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-sa/4.0 | * |
dc.subject | Lógica temporal lineal | es_ES |
dc.subject | Verificación | es_ES |
dc.subject | Control de grupos de ascensores | es_ES |
dc.subject | Sistemas de eventos discretos | es_ES |
dc.subject | Sistemas multiagente | es_ES |
dc.subject | Linear temporal logic | es_ES |
dc.subject | Verification | es_ES |
dc.subject | Elevator group control | es_ES |
dc.subject | Discrete-event systems | es_ES |
dc.subject | Multi-agent systems | es_ES |
dc.title | Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino | es_ES |
dc.title.alternative | Modeling and Linear Temporal Logic Verification of a Group of Two Elevators with Destination Control System | es_ES |
dc.type | info:eu-repo/semantics/conferenceObject | es_ES |
dc.rights.access | info:eu-repo/semantics/embargoedAccess | es_ES |
dc.date.embargoEndDate | 2019-08-25 | es_ES |
dc.date.embargoLift | 2019-08-25 | |
UDC.startPage | 617 | es_ES |
UDC.endPage | 622 | es_ES |
UDC.conferenceTitle | XL Jornadas de Automática | es_ES |