Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino
Use this link to cite
http://hdl.handle.net/2183/23775
Except where otherwise noted, this item's license is described as Atribución-NoComercial-CompartirIgual 4.0
Collections
Metadata
Show full item recordTitle
Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destinoAlternative Title(s)
Modeling and Linear Temporal Logic Verification of a Group of Two Elevators with Destination Control SystemDate
2019Citation
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
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. [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
Keywords
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
Editor version
Rights
Atribución-NoComercial-CompartirIgual 4.0
ISBN
978-84-9749-716-9