Abstract
In this paper we describe the tool d/dt which provides automatic safety verification of hybrid systems with linear continuous dynamics with uncertain input. The verification procedure is based on a method for overapproximating reachable sets by orthogonal polyhedra. The tool also allows to synthesize a controller which switches the system between continuous modes in order to satisfy a safety specification.
Chapter PDF
Similar content being viewed by others
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. L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126, 183–235, 1994.
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.
E. Asarin, O. Bournez, T. Dang and O. Maler, Reachability Analysis of Piecewise-Linear Dynamical Systems, HSCC, 20–31 LNCS 1790, Springer, 2000.
E. Asarin, O. Bournez, T. Dang, O. Maler and A. Pnueli, Effective Synthesis of Switching Controllers for Linear Systems, Proc. of the IEEE, July, 2000.
E. Asarin, S. Bansal, B. Espiau, T. Dang and O. Maler, On Hybrid Control of Under-actuated Mechanical Systems, HSCC, 77–88 LNCS 2034, Springer, 2001.
E. Asarin, T. Dang and O. Maler, d/dt, a Tool for Reachability Analysis of Continuous and Hybrid Systems, Proc. IFAC Nonlinear Control Systems, 20–31, 2001.
C. Belta, J. Schug, T. Dang, V. Kumar, G. J. Pappas, H. Rubin and P. Dunlap, Stability and reachability analysis of a hybrid model of luminescence in the marine bacterium Vibrio Fisheri, Proc. 40th IEEE Conf. on Decision and Control, 2001.
O. Botchkarev and S. Tripakis, Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations, HSCC, 73–88 LNCS 1790, Springer, 2000.
O. Bournez, O. Maler and A. Pnueli, Orthogonal Polyhedra: Representation and Computation, HSCC, 46–60 LNCS 1569, Springer, 1999.
A. Chutinan and B. H. Krogh, Verification of Polyhedral Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations, HSCC, 76–90 LNCS 1569, Springer, 1999.
T. Dang and O. Maler, Reachability Analysis via Face Lifting, HSCC, 96–109 LNCS 1386, Springer, 1998.
T. A. Henzinger, P. W. Kopke, A. Puri and P. Varaiya, What’s decidable about hybrid automata?, J. of Computer and System Sciences 57, 94–124, 1998.
T. A. Henzinger, P.-H. Ho and H. Wong-Toi, HyTech: A Model Checker for Hybrid Systems, Software Tools for Technology Transfer 1, 110–122, 1997.
A. Kurzhanski and P. Varaiya, Ellipsoidal Techniques for Reachability Analysis, HSCC, 202–214 LNCS 1790, Springer, 2000.
K. Larsen, P. Pettersson and W. Yi, Uppaal in a nutshell, Software Tools for Technology Transfert 1–1, 1997.
O. Maler, Z. Manna and A. Pnueli, From Timed to Hybrid Systems, Real-Time: Theory in Practice, 447–484 LNCS 600, Springer, 1992.
G. Pappas, G. Lafferriere and S. Yovine, A New Class of Decidable Hybrid Systems, HSCC, 7–12 LNCS 1569, Springer, 1999.
B. I. Silva, O. Stursberg, B. H. Krogh and S. Engell, An Assessment of the Current Status of Algorithmic Approaches to the Verification of Hybrid Systems, Proc. IEEE Conf. on Decision and Control, 2867–2874, 2001.
S. Yovine, Kronos: A Verification Tool for Real-time Systems, Software Tools for Technology Transfer 1-1, 123–133, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asarin, E., Dang, T., Maler, O. (2002). The d/dt Tool for Verification of Hybrid Systems. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_30
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive