Analysis of a Redesigned Lift System Using UPPAAL

B. Karstens; Wan Fokkink; J. Pang

Analysis of a Redesigned Lift System Using UPPAAL

B. Karstens, Wan Fokkink, J. Pang

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic

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 language	English
Title of host publication	Proceedings 5th Conference on Formal Engineering Methods: ICFEM'03
Subtitle of host publication	Lecture Notes in Computer Science 2885
Publisher	Springer/Verlag
Pages	504-522
Volume	2885
Publication status	Published - 2003

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

https://link.springer.com/chapter/10.1007/978-3-540-39893-6_29

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{5c35981820524e43b726c92453ef4fb5,

title = "Analysis of a Redesigned Lift System Using UPPAAL",

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{\textquoteright} 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.",

author = "B. Karstens and Wan Fokkink and J. Pang",

year = "2003",

language = "English",

volume = "2885",

pages = "504--522",

booktitle = "Proceedings 5th Conference on Formal Engineering Methods: ICFEM'03",

publisher = "Springer/Verlag",

}

TY - GEN

T1 - Analysis of a Redesigned Lift System Using UPPAAL

AU - Karstens, B.

AU - Fokkink, Wan

AU - Pang, J.

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

M3 - Conference contribution

VL - 2885

SP - 504

EP - 522

BT - Proceedings 5th Conference on Formal Engineering Methods: ICFEM'03

PB - Springer/Verlag

ER -

Analysis of a Redesigned Lift System Using UPPAAL

Abstract

UN SDGs

Access to Document

Persistent URL (handle)

Fingerprint

Cite this