Advertisement

STRONG: A Trajectory-Based Verification Toolbox for Hybrid Systems

  • Yi Deng
  • Akshay Rajhans
  • A. Agung Julius
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)

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.

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Rajhans, A.: Development of robust testing toolbox for hybrid systems. Master’s thesis, School of Engineering and Applied Science, Univ. of Pennsylvania (2007)Google Scholar
  7. 7.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Yi Deng
    • 1
  • Akshay Rajhans
    • 2
  • A. Agung Julius
    • 1
  1. 1.ECSE DepartmentRensselaer Polytechnic InstituteUSA
  2. 2.ECE DepartmentCarnegie Mellon UniversityUSA

Personalised recommendations