2026-05-31T10:14:18Zhttps://riuma.uma.es/rest/oai/request

oai:riuma.uma.es:10630/183692026-02-03T12:20:13Zcom_10630_2254col_10630_37959

00925njm 22002777a 4500 dc Toscano-Moreno, Manuel author Arregui, Alberto author Mandow, Anthony author García-Cerezo, Alfonso José author 2019 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 \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. 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 https://hdl.handle.net/10630/18369 Ascensores Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino