Abstract
We present the framework of delta-complete analysis for bounded reachability problems of hybrid systems. We perform bounded reachability checking through solving delta-decision problems over the reals. The techniques take into account of robustness properties of the systems under numerical perturbations. Our implementation of the techniques scales well on several highly nonlinear hybrid system models that arise in biomedical applications.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Alur, R.: Formal verification of hybrid systems. In: EMSOFT, pp. 273–278 (2011)
Gao, S., Avigad, J., Clarke, E.M.: Delta-complete decision procedures for satisfiability over the reals. In: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), pp. 286–300 (2012)
Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 305–314 (2012)
Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013)
Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: Proceedings of the 13th International Conference on Formal Methods in Computer Aided Design, FMCAD (2013)
Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011)
Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292 (1996)
Weihrauch, K.: Computable Analysis: An Introduction (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clarke, E.M., Gao, S. (2014). Model Checking Hybrid Systems. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. ISoLA 2014. Lecture Notes in Computer Science, vol 8803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45231-8_28
Download citation
DOI: https://doi.org/10.1007/978-3-662-45231-8_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45230-1
Online ISBN: 978-3-662-45231-8
eBook Packages: Computer ScienceComputer Science (R0)