Reliable Simulation and Monitoring of Hybrid Systems Based on Interval Analysis

(Extended Abstract)
  • Daisuke IshiiEmail author
  • Alexandre Goldsztejn
  • Naoki Yonezaki
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11267)


Hybrid systems serve as a high-level model of cyber-physical systems. Formal methods for hybrid systems have been studied energetically for around three decades and various methods for reachability analysis and approximation of continuous states/behaviors have been proposed (e.g., [1, 8]). Another line of technology, e.g., MATLAB/Simulink and Modelica, has been developed in the simulation of hybrid systems and has driven the rise of model-based development in the industry. While reachability analysis methods aim to analyze whole behaviors of a given system with carefully taking care of numerical computation errors, the latter technology focuses on efficient simulation of an approximated trajectory of a practical model.



This work was partially funded by JSPS (KAKENHI 25880008, 15K15968, and 26280024).


  1. 1.
    Alur, R., et al.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Bouissou, O., Mimram, S., Chapoutot, A.: HySon: set-based simulation of hybrid systems. In: 23rd IEEE International Symposium on Rapid System Prototyping (RSP), pp. 79–85 (2012)Google Scholar
  3. 3.
    Chen, X., Abraham, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: IEEE Real-Time Systems Symposium, pp. 183–192 (2012)Google Scholar
  4. 4.
    Collins, P., Goldsztejn, A.: The reach-and-evolve algorithm for reachability analysis of nonlinear dynamical systems. Electron. Notes Theor. Comput. Sci. 223(639), 87–102 (2008)CrossRefGoogle Scholar
  5. 5.
    Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010). Scholar
  6. 6.
    Duracz, A., Bartha, F.A., Taha, W.: Accurate rigorous simulation should be possible for good designs. In: Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), pp. 1–10 (2016)Google Scholar
  7. 7.
    Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008). Scholar
  8. 8.
    Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). Scholar
  9. 9.
    Goldsztejn, A., Ishii, D.: A parallelotope method for hybrid system simulation. Reliable Comput. 23, 163–185 (2016)MathSciNetGoogle Scholar
  10. 10.
    Goubault, E., Mullier, O., Kieffer, M.: Inner approximated reachability analysis. In: HSCC, pp. 163–172 (2014)Google Scholar
  11. 11.
    Ishii, D., Goldsztejn, A.: HySIA: tool for simulating and monitoring hybrid automata based on interval analysis. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 370–379. Springer, Cham (2017). Scholar
  12. 12.
    Ishii, D., Yonezaki, N., Goldsztejn, A.: Monitoring bounded LTL properties using interval analysis. In: 8th International Workshop on Numerical Software Verification (NSV). ENTCS 317, pp. 85–100 (2015)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Ishii, D., Yonezaki, N., Goldsztejn, A.: Monitoring temporal properties using interval analysis. In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E99-A (2016)CrossRefGoogle Scholar
  14. 14.
    Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). Scholar
  15. 15.
    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT - 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). Scholar
  16. 16.
    Mohaqeqi, M., Mousavi, M.R., Taha, W.: Conformance testing of cyber-physical systems: a comparative study. In: 14th International Workshop on Automated Verification of Critical Systems (AVOCS) (2014)Google Scholar
  17. 17.
    Ramdani, N., Meslem, N., Candau, Y.: A hybrid bounding method for computing an over-approximation for the reachable set of uncertain nonlinear systems. IEEE Trans. Autom. Control 54(10), 2352–2364 (2009)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Ramdani, N., Nedialkov, N.S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Anal. Hybrid Syst. 5(2), 149–162 (2011)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Ratschan, S.: Safety verification of non-linear hybrid systems is quasi-decidable. Formal Methods Syst. Des. 44(1), 71–90 (2014)CrossRefGoogle Scholar
  20. 20.
    Sandretto, J.A.D., Chapoutot, A.: Validated explicit and implicit runge-kutta methods. Reliable Comput. 22, 78–103 (2016)MathSciNetGoogle Scholar
  21. 21.
    Shmarov, F., Zuliani, P.: ProbReach: Verified probabilistic delta-reachability for stochastic hybrid systems. In: HSCC, pp. 134–139 (2015)Google Scholar
  22. 22.
    Wang, Q., Zuliani, P., Kong, S., Gao, S., Clarke, E.M.: SReach: A Bounded Model Checker for Stochastic Hybrid Systems. CoRR abs/1404.7206 (2015)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Daisuke Ishii
    • 1
    Email author
  • Alexandre Goldsztejn
    • 2
  • Naoki Yonezaki
    • 3
  1. 1.University of FukuiFukuiJapan
  2. 2.CNRS/LS2NNantesFrance
  3. 3.Tokyo Denki UniversityTokyoJapan

Personalised recommendations