Analysis of a Redesigned Lift System Using UPPAAL

B. Karstens, Wan Fokkink, J. Pang

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademic


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.
Original languageEnglish
Title of host publicationProceedings 5th Conference on Formal Engineering Methods: ICFEM'03
Subtitle of host publicationLecture Notes in Computer Science 2885
Publication statusPublished - 2003

Fingerprint Dive into the research topics of 'Analysis of a Redesigned Lift System Using UPPAAL'. Together they form a unique fingerprint.

Cite this