Skip navigation
  •  Inicio
  • UDC 
    • Cómo depositar
    • Políticas do RUC
    • FAQ
    • Dereitos de Autor
    • Máis información en INFOguías UDC
  • Percorrer 
    • Comunidades
    • Buscar por:
    • Data de publicación
    • Autor
    • Título
    • Materia
  • Axuda
    • español
    • Gallegan
    • English
  • Acceder
  •  Galego 
    • Español
    • Galego
    • English
  
Ver ítem 
  •   RUC
  • Publicacións UDC
  • Congresos e cursos UDC
  • Jornadas de Automática
  • Jornadas de Automática (40ª. 2019. Ferrol)
  • Ver ítem
  •   RUC
  • Publicacións UDC
  • Congresos e cursos UDC
  • Jornadas de Automática
  • Jornadas de Automática (40ª. 2019. Ferrol)
  • Ver ítem
JavaScript is disabled for your browser. Some features of this site may not work without it.

Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino

Thumbnail
Ver/abrir
2019_Toscano-Moreno_Modelado-verificacion-logica-lineal-ascensores.pdf (6.987Mb)
Use este enlace para citar
http://hdl.handle.net/2183/23775
Atribución-NoComercial-CompartirIgual 4.0
A non ser que se indique outra cousa, a licenza do ítem descríbese como Atribución-NoComercial-CompartirIgual 4.0
Coleccións
  • Jornadas de Automática (40ª. 2019. Ferrol) [114]
Metadatos
Mostrar o rexistro completo do ítem
Título
Modelado y verificación mediante lógica lineal temporal de un grupo de dos ascensores con sistema de control de destino
Título(s) alternativo(s)
Modeling and Linear Temporal Logic Verification of a Group of Two Elevators with Destination Control System
Autor(es)
Toscano Moreno, Manuel
Arregui, Alberto
Mandow, Anthony
García-Cerezo, Alfonso
Data
2019
Cita 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
 
Versión do editor
https://doi.org/10.17979/spudc.9788497497169.617
Dereitos
Atribución-NoComercial-CompartirIgual 4.0
ISBN
978-84-9749-716-9

Listar

Todo RUCComunidades e colecciónsPor data de publicaciónAutoresTítulosMateriasGrupo de InvestigaciónTitulaciónEsta colecciónPor data de publicaciónAutoresTítulosMateriasGrupo de InvestigaciónTitulación

A miña conta

AccederRexistro

Estatísticas

Ver Estatísticas de uso
Sherpa
OpenArchives
OAIster
Scholar Google
UNIVERSIDADE DA CORUÑA. Servizo de Biblioteca.    DSpace Software Copyright © 2002-2013 Duraspace - Suxestións