Abstract
We present STRONG, a MATLAB toolbox for hybrid system verification. The toolbox addresses the problem of reachability/safety verification for bounded time. It simulates a finite number of trajectories and computes robust neighborhoods around their initial states such that any trajectory starting from these robust neighborhoods follows the same sequence of locations as the simulated trajectory does and avoids the unsafe set if the simulated trajectory does. Numerical simulation and computation of robust neighborhoods for linear dynamics scale well with the size of the problem. Moreover, the computation can be readily parallelized because the nominal trajectories can be simulated independently of each other. This paper showcases key features and functionalities of the toolbox using some examples.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Hybrid System
- Simulated Trajectory
- Rensselaer Polytechnic Institute
- Nominal Trajectory
- Coverage Assessment
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
Afshari, S.: Coverage assessment criteria for approximate bisimulation theory and introduction of computer games in hybrid systems safety/reachability design. Master’s thesis, Rensselaer Polytechnic Institute, NY (2010)
Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-taLiRo: A tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011)
Donzé, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)
Fehnker, A., Ivančić, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)
Julius, A.A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 329–342. Springer, Heidelberg (2007)
Rajhans, A.: Development of robust testing toolbox for hybrid systems. Master’s thesis, School of Engineering and Applied Science, Univ. of Pennsylvania (2007)
Stursberg, O., Fehnker, A., Han, Z., Krogh, B.H.: Verification of a cruise control system using counterexample-guided search. In: Control Engineering Practice, vol. 12, pp. 1269–1278 (October 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Deng, Y., Rajhans, A., Julius, A.A. (2013). STRONG: A Trajectory-Based Verification Toolbox for Hybrid Systems. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds) Quantitative Evaluation of Systems. QEST 2013. Lecture Notes in Computer Science, vol 8054. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40196-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-40196-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40195-4
Online ISBN: 978-3-642-40196-1
eBook Packages: Computer ScienceComputer Science (R0)