Abstract
This paper shows how HyTech, a symbolic model checker for linear hybrid systems, can be used to verify a part of an abstracted automotive control system. The system controls the height of an automobile by a pneumatic suspension system and has been proposed by BMW AG as a case study taken from a current industrial development. For a system which controls one wheel we verify safety properties, such as that the height of the car maintains within desired bounds or that the height is not changed in curves, by reachability analysis. Furthermore, a property related to stability in the sense of control theory is verified. We believe that the case study can serve as a real-life benchmark problem for the formal analysis of embedded reactive systems.
Research supported by “KorSys”, BMBF.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.
R. Alur, T.A. Henzinger, and E.D. Sontag. Hybrid Systems III. Lecture Notes in Computer Science 1066. Springer-Verlag, 1996.
T.A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In P. Wolper, editor, CAV 95: Computer-aided Verification, Lecture Notes in Computer Science 939, pages 225–238. Springer-Verlag, 1995.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to hytech. In E. Brinksma et al., editors, Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, pages 41–71. Springer-Verlag, 1995.
P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In P. Wolper, editor, CAV 95: Computer-aided Verification, Lecture Notes in Computer Science 939, pages 381–394. Springer-Verlag, 1995.
T.A. Henzinger and H. Wong-Toi. Linear phase-portrait approximations for nonlinear hybrid systems. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, LNCS 1066. Springer-Verlag, 1996.
Thomas A. Henzinger and H. Wong-Toi. Using hytech to synthesize control parameters for a steam boiler. In J.-R. Abrial et al., editors, Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165. Springer-Verlag, 1996.
Charles L. Phillips and Royce D. Harbor. Feedback Control Systems. Prentice-Hall, 1988.
Thomas Stauner. Specification and Verification of an Electronic Height Control System using Hybrid Automata. Master thesis, Munich University of Technology, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stauner, T., Müller, O., Fuchs, M. (1997). Using HyTech to verify an automotive control System. In: Maler, O. (eds) Hybrid and Real-Time Systems. HART 1997. Lecture Notes in Computer Science, vol 1201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014722
Download citation
DOI: https://doi.org/10.1007/BFb0014722
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62600-8
Online ISBN: 978-3-540-68330-8
eBook Packages: Springer Book Archive