A dependable automated people mover system modeled and verified using timed automata : a case study

Abstract

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.