Analysis of a Redesigned Lift System Using UPPAAL

B. Karstens, Wan Fokkink, J. Pang

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

Abstract

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
PublisherSpringer/Verlag
Pages504-522
Volume2885
Publication statusPublished - 2003

    Fingerprint

Cite this

Karstens, B., Fokkink, W., & Pang, J. (2003). Analysis of a Redesigned Lift System Using UPPAAL. In Proceedings 5th Conference on Formal Engineering Methods: ICFEM'03: Lecture Notes in Computer Science 2885 (Vol. 2885, pp. 504-522). Springer/Verlag.