Please use this identifier to cite or link to this item:

TitleA dependable automated people mover system modeled and verified using timed automata : a case study
Author(s)Kunz, Guilherme
Perondi, Eduardo
Machado, José Mendes
Automated people movers
Issue dateOct-2011
PublisherAssociação Brasileira de Engenharia e Ciências Mecânicas (ABCM)
CitationGuilherme Kunz; Eduardo Perondi; Machado, José. A Dependable Automated People Mover System Modeled and Verified using Timed Automata: A Case Study, Trabalho apresentado em COBEM'2011 - 21st International Congress of Mechnical Engineering, In Proceedings of COBEM'2011 - 21st International Congress of Mechnical Engineering, Natal, 2011.
Abstract(s)Automated People Movers (APM) are systems for passenger transport with fully automated operation and high frequency service. For this study we have used the system named Aeromovel installed in Porto Alegre, Brazil. Aeromovel is a non-conventional Automatic People Mover whose operation principle is based on pneumatics. This paper proposes the use, in a complementary way, of two analysis techniques, simulation and formal verification, in order to guarantee the desired behavior for an APM propulsion system composed by a centrifugal fan and ten (on-off and proportional) pneumatic valves driven by pneumatic pistons. This approach is based on the use of timed automata and UPPAAL modelchecker. The more focused aspect is the modeling of the propulsion system associated at the distributed control system. Some simulation and formal verification results are presented, considering desired behavior properties in order to improve the system’s dependability.
TypeConference paper
AccessOpen access
Appears in Collections:DEM - Publicações em actas de encontros científicos / Papers in conference proceedings

Files in This Item:
File Description SizeFormat 
GK_cobem2011 V1.pdf180,7 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID