Abstract
In this paper, we present a real time animator for dynamical systems that can be modeled as hybrid automata i.e. standard finite automata extended with differential equations. We describe its semantic foundation and its implementation in Java and C using CVODE, a software package for solving ordinary differential equations. We show how the animator is interfaced with the UPPAAL tool to demonstrate the real time behavior of dynamical systems under the control of discrete components described as timed automata.
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.
Similar content being viewed by others
References
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 125:183–235, 1994.
S. Cohen and A. Hindmarsh. Cvode, a stiff/nonstiff ode solver in c. Computers in Physics, 2(10):138–43, March–April 1996.
P. D’Argenio, J.-P. Katoen, T. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, volume 1217 of LNCS, pages 416–431. Springer-Verlag, April 1997. Enschede, The Netherlands.
K. Havelund, A. Skou, K. G. Larsen, and K. Lund. Formal modelling and analysis of an audio/video protocol: An industrial case study using uppaal. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 2–13. IEEE, December 1997. San Francisco, California, USA.
T. A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic on Computer Science (LICS 96), pages 278–292. IEEE, 1996.
K. J. Kristoffersen, K. G. Larsen, P. Pettersson, and C. Weise. Experimental batch plant-vhs case study 1 using timed automata and uppaal. Deliverable of EPRIT-LTR Project 26270 VHS (Verification of Hybird Systems), 1999.
M. Lindahl, P. Pettersson, and W. Yi. Formal design and analysis of a gear controller. In B. Steffen, editor, Proceedings of the 4th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of LNCS, pages 281–297, 1999. Gulbenkian Foundation, Lisbon, Portugal.
H. Lönn and P. Pettersson. Formal verification of a tdma protocol start-up mechanism. In Proceedings of 1997 IEEE Pacific Rim International Symposium on Fault-Tolerant Systems, pages 235–242. IEEE, December 1997. Taipei, Taiwan.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amnell, T., David, A., Yi, W. (2001). A Real-Time Animator for Hybrid Systems. In: Davidson, J., Min, S.L. (eds) Languages, Compilers, and Tools for Embedded Systems. LCTES 2000. Lecture Notes in Computer Science, vol 1985. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45245-1_9
Download citation
DOI: https://doi.org/10.1007/3-540-45245-1_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41781-1
Online ISBN: 978-3-540-45245-4
eBook Packages: Springer Book Archive