Abstract
We introduce the verification of hybrid systems as offered by the open-source framework called ARIADNE. The ARIADNE C++ library exploits approximation techniques based on the theory of computable analysis for implementing formal verification algorithms based on reachability analysis. We demonstrate the tool using a classical example of a controlled water tank system.
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
Notes
- 1.
ImageSets are used in the stable version of Ariadne. The development version uses a more accurate representation based on ConstrainedImageSets [7].
References
Alur R, Courcoubetis C, Henzinger TA, Ho PH (1992) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid systems, LNCS. Springer, Berlin, pp 209–229
Alur Rajeev, Dang Thao, Ivančić Franjo (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354(2):250–271
Ariadne: An open tool for hybrid system analysis. http://ariadne.parades.rm.cnr.it
Benvenuti L, Bresolin D, Collins P, Ferrari A, Geretti L, Villa T (2012) Ariadne: Dominance checking of nonlinear hybrid automata using reachability analysis. Reachability Problems., volume 7550 of LNCSSpringer, Berlin Heidelberg, pp 79–91
Benvenuti L, Bresolin D, Collins P, Ferrari A, Geretti L, Villa T (2014) Assume-guarantee verification of nonlinear hybrid systems with ARIADNE. Int J Robust Nonlinear Control 24(4):699–724
Bresolin D (2013) Improving HyLTL model checking of hybrid systems. In: Proceedings of the 4th international symposium on games, automata, logics and formal verification (GandALF2013), vol 119 of EPTCS, pp 79–92
Collins P, Bresolin D, Geretti L, Villa T (2012) Computing the evolution of hybrid systems using rigorous function calculus. In: Proceedings of the 4th IFAC conference on analysis and design of Hybrid Systems (ADHS12), pp 284–290
Frehse G (2008) PHAVer: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transf (STTT) 10:263–279
Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: Proceedings 23rd international conference on computer aided verification (CAV 2011), volume 6806 of LNCS. Springer, Berlin, pp 379–395
Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans Embed Comput Syst 6(1)
Tomlin CJ, Lygeros J, Sastry SS (2000) A game theoretic approach to controller design for hybrid systems. Proc IEEE 88(7):949–970
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Bresolin, D., Geretti, L., Villa, T., Collins, P. (2015). An Introduction to the Verification of Hybrid Systems Using Ariadne . In: van Schuppen, J., Villa, T. (eds) Coordination Control of Distributed Systems. Lecture Notes in Control and Information Sciences, vol 456. Springer, Cham. https://doi.org/10.1007/978-3-319-10407-2_39
Download citation
DOI: https://doi.org/10.1007/978-3-319-10407-2_39
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10406-5
Online ISBN: 978-3-319-10407-2
eBook Packages: EngineeringEngineering (R0)