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.
This research is partly supported by the Dutch Technology Foundation STW under the project CES5008: Improving the quality of embedded systems using formal design and systematic testing.
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
Aceto, L., Burgueno, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 263–280. Springer, Heidelberg (1998)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Bengtsson, J., Griffioen, W.O.D., Kristoffersen, K.J., Larsen, K.G., Larsson, F., Pettersson, P., Wang, Y.: Automated analysis of an audio control protocol using UPPAAL. Journal of Logic and Algebraic Programming 52-53, 163–181 (2002)
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Computation 60, 109–137 (1984)
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)
Gmbh, R.B.: Postfach 30 02 40, D-70442 Stuttgart, Germany. CAN Specification. Version 2.0 (1991)
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)
Groote, J.F., Ponse, A.: The syntax and semantics of μCRL. In: Algebra of Communicating Processes 1994, Workshops in Computing Series, pp. 26–62. Springer, Heidelberg (1995)
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)
Karstens, B.: Formal verification of the redesign of a distributed lift system using UPPAAL. Master thesis, Utrecht University (2003), Available at http://www.cwi.nl/~pangjun/research/liftredesign.ps
Larsen, K.G., Pettersson, P., Wang, Y.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Lindahl, M., Pettersson, P., Wang, Y.: Formal design and analysis of a gear controller. International Journal on Software Tools for Technology Transfer 3(3), 353–368 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pang, J., Karstens, B., Fokkink, W. (2003). Analyzing the Redesign of a Distributed Lift System in UPPAAL. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-39893-6_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20461-9
Online ISBN: 978-3-540-39893-6
eBook Packages: Springer Book Archive