State Estimation and Property-Guided Exploration for Hybrid Systems Testing

  • Thao Dang
  • Noa Shalev
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7641)


This paper is concerned with model-based testing of hybrid systems. The first result is an algorithm for test generation which enhances the coverage of critical trajectories by using a random walk. The second result is a framework for practical testing that includes a state estimator. When the state of a system under test cannot be directly observed, it is necessary to reconstruct the trajectory of the real system in order to produce a verdict whether the system violates a property. To do so, we integrate in our tester a hybrid observer, the goal of which is to provide an estimate for the current location and the continuous state of the system under test based on the information on the input and the output of the system.


Random Walk Hybrid System Test Generation Discrete Transition System Under Test 
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.


  1. 1.
    Aichernig, B.K., Brandl, H., Wotawa, F.: Conformance testing of hybrid systems with qualitative reasoning models. Electron. Notes Theor. Comput. Sci. 253(2), 53–69 (2009)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Aziz, P.M., Sorensen, H.V., van der Spiegel, J.: An overview of sigma-delta converters. IEEE Signal Processing Magazine 13(1), 61–84 (1996)CrossRefGoogle Scholar
  4. 4.
    Bhatia, A., Frazzoli, E.: Incremental Search Methods for Reachability Analysis of Continuous and Hybrid Systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 142–156. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Biyik, E., Arcak, M.: Hybrid newton observer design using the inexact newton method and gmres. In: Proc. 2006 American Control Conf., ACC 2006, pp. 3334–3339 (2006)Google Scholar
  6. 6.
    Dang, T.: Model-based testing of hybrid systems. In: Model-Based Testing for Embedded Systems. CRC Press (2010)Google Scholar
  7. 7.
    Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods in System Design 34(2), 183–213 (2009)zbMATHCrossRefGoogle Scholar
  8. 8.
    David, A., Larsen, K.G., Li, S., Nielsen, B.: Timed testing under partial observability. In: 2nd IEEE International Conference on Software Testing, ICST 2009. IEEE Computer Society Press (2009)Google Scholar
  9. 9.
    Esposito, J., Kim, J.W., Kumar, V.: Adaptive RRTs for validating hybrid robotic control systems. In: Proceedings Workshop on Algorithmic Foundations of Robotics, Zeist, The Netherlands (July 2004)Google Scholar
  10. 10.
    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
  11. 11.
    Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods Syst. Des. 34(3) (2009)Google Scholar
  12. 12.
    LaValle, S., Kuffner, J.: Rapidly-exploring random trees: Progress and prospects, 2000. In: Workshop on the Algorithmic Foundations of Robotics (2000)Google Scholar
  13. 13.
    Luenberger, D.G.: Optimization by Vector Space Methods. Wiley, New York (1969)zbMATHGoogle Scholar
  14. 14.
    Moraal, P., Grizzle, J.W.: Observer design for nonlinear systems with discrete-time measurements. IEEE Transactions on Automatic Control 40(3) (1995)Google Scholar
  15. 15.
    Motowani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, New York (1995)Google Scholar
  16. 16.
    Nonaka, Y., Ono, H., Sadakane, K., Yamashita, M.: The hitting and cover times of metropolis walks. Theor. Comput. Sci. 411(16-18), 1889–1894 (2010)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Plaku, E., Kavraki, L., Vardi, M.: Hybrid Systems: From Verification to Falsification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 463–476. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2012

Authors and Affiliations

  • Thao Dang
    • 1
  • Noa Shalev
    • 1
  1. 1.Centre EquationVERIMAG/CNRSGièresFrance

Personalised recommendations