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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Pang, J., Karstens, B., Fokkink, W.J.: Analyzing the Redesign of a Distributed Lift System in UPPAAL. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 504–522. Springer, Heidelberg (2003)
Karstens, B.: Formal Verification of the Redesign of a Distributed Lift System using Uppaal. MSc thesis, Utrecht University (June 2003), available at http://www.phil.uu.nl/preprints/scripties/list.html
Blom, S.C.C., Fokkink, W.J., Groote, J.F., van Langevelde, I.A., Lisser, B., van de Pol, J.C.: μCRL: A Toolset for Analysing Algebraic Specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)
Groote, J.F., Pang, J., Wouters, A.G.: A Balancing Act: Analyzing a Distributed Lift System. In: Proc. FMICS 2001, pp. 1–12 (2001)
Groote, J.F., Pang, J., Wouters, A.G.: Analysis of a Distributed System for Lifting Trucks. Journal of Logic and Algebraic Programming 55(1-2), 21–56 (2003)
Larsen, K.G., Pettersson, P., Wang, Y.: UPPAAL in a Nutshell. Software Tools for Technology Transfer 1(1–2), 134–152 (1997)
Aceto, L., Burgueno, A., Larsen, K.G.: Model Checking via Reachability Testing for Timed Automata. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, pp. 263–280. Springer, Heidelberg (1998)
Aceto, L., Bouyer, P., Burgueno, A., Larsen, K.G.: The Power of Reachability Testing for Timed Automata. Theoretical Computer Science 300(1-3), 411–475 (2003)
Gmbh, R.B.: Postfach 30 02 40, D-70442 Stuttgart, Germany. CAN Specification. Version 2.0 (1991)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)
Kakebeen, A.: Extension and Formal Verification of a Distributed Lift System in UPPAAL. MSc thesis, Radbout Universiteit Nijmegen (August 2005), available at www.cs.vu.nl/~wanf/kakebeen.doc
Havelund, K., Larsen, K.G., Skou, A.: Formal Verification of a Power Controller using the Real-time Model Checker UPPAAL. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 277–298. Springer, Heidelberg (1999)
Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding Symmetry Reduction to UPPAAL. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46–59. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fokkink, W., Kakebeen, A., Pang, J. (2007). Adapting the UPPAAL Model of a Distributed Lift System. In: Arbab, F., Sirjani, M. (eds) International Symposium on Fundamentals of Software Engineering. FSEN 2007. Lecture Notes in Computer Science, vol 4767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75698-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-75698-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75697-2
Online ISBN: 978-3-540-75698-9
eBook Packages: Computer ScienceComputer Science (R0)