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.
Similar content being viewed by others
Author information
Authors and Affiliations
Additional information
Published online: 18 July 2001
Rights and permissions
About this article
Cite this article
Lindahl, M., Pettersson, P. & Yi, W. Formal design and analysis of a gear controller. STTT 3, 353–368 (2001). https://doi.org/10.1007/s100090100048
Issue Date:
DOI: https://doi.org/10.1007/s100090100048