Adapting the UPPAAL Model of a Distributed Lift System

Abstract. Groote, Pang and Wouters (2001) analyzed an existing distributed lift system using the process algebraic toolset µCRL. Pang, Karstens and Fokkink (2003) analyzed a redesign of this system using the timed automata based toolset Uppaal. We adapt and extend this Uppaal model. Firstly, we refine the synchronization mechanism between lifts, to explain a new problem that was reported by the developers of the lift system, and to propose a solution for it. Secondly, we allow a lift to enter a halt state, after which the entire system should make an emergency stop, for instance because a lift meets a maximum height threshold. Using the Uppaal model checker we verified that the adapted lift system satisfies the system requirements.

• Type: Conference
• Year: 2007
• Where: FSEN
• Authors: Wan Fokkink, Allard Kakebeen, Jun Pang
• Keywords: Automata Based Toolset, FSEN 2007, Process Algebraic Toolset, Uppaal Model