@inproceedings{227aee19486843bdafa5ccb692d6486b,
title = "Formal design and analysis of a gear controller",
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.",
author = "Magnus Lindahl and Paul Pettersson and Wang Yi",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1998.; 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1998, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998 ; Conference date: 28-03-1998 Through 04-04-1998",
year = "1998",
doi = "10.1007/bfb0054178",
language = "英语",
isbn = "3540643567",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "281--297",
editor = "Bernhard Steffen",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 4th International Conference, TACAS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings",
address = "德国",
}