Abstract
In this paper, we report on an application of the validation and verification tool kit Uppaal in the design and analysis of a prototype gear controller, carried out in a joint project between industry and academia. We give a detailed description of the formal model of the gear controller and its surrounding environment, and its correctness formalized according to the informal requirements delivered by our industrial partner of the project. The second contribution of this paper is a solution to the problem we met in this case study, namely how to use a tool like Uppaal, which only provides reachability analysis to verify bounded response time properties. The advantage of our solution is that we need no additional implementation work to extend the existing model-checker, but simple manual syntactical manipulation on the system description.
This work has been supported by ASTEC (Advanced Software TEChnology), NUTEK (Swedish Board for Technical Development) and TFR (Swedish Technical Research Council).
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and D. Dill. Automata for Modelling Real-Time Systems. Theoretical Computer Science, 126(2):183–236, April 1994.
Johan Bengtsson, David Griffioen, Kåre Kristoffersen, Kim G. Larsen, Predrik Larsson, Paul Pettersson, and Wang Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Rajeev Alur and Thomas A. Henzinger, editors, Proc. of 8th Int. Conf. on Computer Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 244–256. Springer-Verlag, July 1996.
Johan Bengtsson, Kim G. Larsen, Predrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. In Proc. of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in Lecture Notes in Computer Science, pages 431–434. Springer-Verlag, Mars 1996.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors, Proc. of Workshop on Verification and Control of Hybrid Systems III, Lecture Notes in Computer Science, pages 208–219. Springer-Verlag, October 1995.
Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: The Next Generation. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 56–65, December 1995.
H.E. Jensen, K.G. Larsen, and A. Skou. Modelling and Analysis of a Collision Avoidance Protocol Using SPIN and Uppaal. In Proc. of 2nd International Workshop on the SPIN Verification System, pages 1–20, August 1996.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a Nutshell. To appear in Internationa] Journal on Software Tools for Technology Transfer, 1998.
Thomas Stauner, Olaf Mller, and Max Fuchs. Using hytech to verify an automotive control system. In Proc. Hybrid and Real-Time Systems, Grenoble, March 26–28, 1997. Technische Universität München, Lecture Notes in Computer Science, Springer, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lindahl, M., Pettersson, P., Yi, W. (1998). Formal design and analysis of a gear controller. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054178
Download citation
DOI: https://doi.org/10.1007/BFb0054178
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive