Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino
Use este enlace para citar
http://hdl.handle.net/2183/23775
A non ser que se indique outra cousa, a licenza do ítem descríbese como Atribución-NoComercial-CompartirIgual 4.0
Coleccións
Metadatos
Mostrar o rexistro completo do ítemTítulo
Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destinoTítulo(s) alternativo(s)
Modeling and Linear Temporal Logic Verification of a Group of Two Elevators with Destination Control SystemData
2019Cita bibliográfica
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
Resumo
[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. [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
Palabras chave
Lógica temporal lineal
Verificación
Control de grupos de ascensores
Sistemas de eventos discretos
Sistemas multiagente
Linear temporal logic
Verification
Elevator group control
Discrete-event systems
Multi-agent systems
Verificación
Control de grupos de ascensores
Sistemas de eventos discretos
Sistemas multiagente
Linear temporal logic
Verification
Elevator group control
Discrete-event systems
Multi-agent systems
Versión do editor
Dereitos
Atribución-NoComercial-CompartirIgual 4.0
ISBN
978-84-9749-716-9