Analyzing the Redesign of a Distributed Lift System in UPPAAL

An existing distributed lift system was analyzed using the process algebraic language µCRL [7]. Four problems were found, three of which were also found independently by the developers in the testing phase. They solved these problems in an ad hoc manner, because the causes of the problems were unclear. The analysis in [7] revealed the reasons for those problems, and proposed solutions. In this paper, we checked the developers’ solutions using Uppaal. We show that the solutions of the developers do not solve these problems completely, while a refined version of our solution proposed in [7] does.

• Type: Conference
• Year: 2003
• Where: ICFEM
• Authors: Jun Pang, Bart Karstens, Wan Fokkink
• Keywords: Ad Hoc Manner, ICFEM 2003, Problems, Process Algebraic Language